18.1. Prime spectrum
Let R and S be commutative rings.
variable {R S : Type} [CommRing R] [CommRing S]
The basic building block of algebraic geometry is the prime spectrum of a ring,
which is the type PrimeSpectrum.
#check PrimeSpectrum R
To provide a term of type PrimeSpectrum R, we need to provide an ideal of R
with a proof that p is a prime ideal.
example (p : Ideal R) [p.IsPrime] : PrimeSpectrum R :=
⟨p, (inferInstance : p.IsPrime)⟩
It is endowed with a structure of topological space: the Zariski topology.
example : TopologicalSpace (PrimeSpectrum R) :=
inferInstance
A ring homomorphism induces a function on prime spectra:
example (f : R →+* S) : PrimeSpectrum S → PrimeSpectrum R :=
PrimeSpectrum.comap f
We can construct sets in the prime spectrum with the familiar constructions. For example,
this is the set \mathrm{V}(s) \cap \mathrm{D}(f):
example (s : Set R) (f : R) : Set (PrimeSpectrum R) :=
PrimeSpectrum.zeroLocus s ∩ PrimeSpectrum.basicOpen f