@MISC{TOPZARI1.MIZ,
  AUTHOR = {Watase, Yasushige},
  TITLE = {{Z}ariski {T}opology},
  SECTION1 = {Preliminaries: Some Properties on Ideals}, 
  SECTION2 = {Spectrum of Prime Ideals (spec) and Maximal Ideal (m-spec)},
  SECTION3 = {Local & Semi-Local Ring},
  SECTION4 = {Nilradical & Jacobson Radical},
  SECTION5 = {Construction of Zariski Topology of the Prime Spectrum of A (Spec A)},
  SECTION6 = {Continous Map Spec B -> Spec A associated with a ring homomorphism},
  DAY = {16},
  MONTH = {October},
  YEAR = {2018},
  ADDRESS1 = {Suginami-ku Matsunoki 3-21-6 Tokyo\\Japan},
  SUMMARY = {We formalize in the Mizar System \cite{Mizar-State-2015}, 
   basic definitions of commutative ring theory such as prime spectrum, 
   nilradical, Jacobson radical and local ring, and semi-local ring, then 
   formalize proofs of some relating theorems along with the first chapter 
   of \cite{AM}. \par
   We denote $\mathrm{Spec} \ A$ for the set of all prime ideals of a 
   commutative ring $A$ and introduce the so-called Zariski topology 
   in order to make $\mathrm{Spec} \ A$ a topological space. We formalize 
   a topological space defined by the topology and provide a formal proof 
   of the fact that $\mathrm{Spec} \ A$ is $\mathrm{T_0}$ space.  
   Finally we formalize a continuous map associated with a ring 
   homomorphism $h:A \longrightarrow B$.  Namely, $h$ induces a continuous 
   map ${}^{a}h:\mathrm{Spec} \ B \longrightarrow \mathrm{Spec} \ A$ (${}^{a}h$ 
   which is defined by ${}^{a}h(\mathfrak{P}) = h^{-1}(\mathfrak{P}),$ 
    where $\mathfrak{P}$ is a prime ideal of $B$.},  
  MSC2010 = {14A05,16D25},
  KEYWORDS = {Prime Spectra; Local Ring; Semi-Local Ring; Nilradical; Jacobson Radical; Zariski Topology }}

@BOOK{AM,
 AUTHOR={M.F.ATIYAH and I.G.MACDONALD},
 TITLE={Introduction to Commutative Algebra},
 PUBLISHER={Addison-Wesley Publishing Company, Inc.},
 YEAR=1969}

@BOOK{IITAKA,
 AUTHOR={Shigeru.IITAKA},
 TITLE={Algebraic Geometory},
 PUBLISHER={Springer-Verlag New York, Inc.},
 YEAR=1982}

@BOOK{IITAKA2,
 AUTHOR={Shigeru.IITAKA},
 TITLE={Ring Theory in Japanese},
 PUBLISHER={Kyoritsu Shuppan Co., Ltd.},
 YEAR=2013}
