Zariski Topology

We formalize in the Mizar system [3], [4] basic definitions of commutative ring theory such as prime spectrum, nilradical, Jacobson radical, local ring, and semi-local ring [5], [6], then formalize proofs of some related theorems along with the first chapter of [1].

The article introduces the so-called Zariski topology. The set of all prime ideals of a commutative ring A is called the prime spectrum of A denoted by Spectrum A. A new functor Spec generates Zariski topology to make Spectrum A a topological space. A different role is given to Spec as a map from a ring morphism of commutative rings to that of topological spaces by the following manner: for a ring homomorphism h : A → B, we defined (Spec h) : Spec B → Spec A by (Spec h)(𝔭) = h⁻¹(𝔭) where 𝔭 2 Spec B.