# The Zariski topology on the prime spectrum of a commutative (semi)ring #

## Conventions #

We denote subsets of (semi)rings with s, s', etc... whereas we denote subsets of prime spectra with t, t', etc...

## Inspiration/contributors #

The contents of this file draw inspiration from https://github.com/ramonfmir/lean-scheme which has contributions from Ramon Fernandez Mir, Kevin Buzzard, Kenny Lau, and Chris Hughes (on an earlier repository).

instance PrimeSpectrum.zariskiTopology {R : Type u} [] :

The Zariski topology on the prime spectrum of a commutative (semi)ring is defined via the closed sets of the topology: they are exactly those sets that are the zero locus of a subset of the ring.

Equations
theorem PrimeSpectrum.isOpen_iff {R : Type u} [] (U : Set ()) :
∃ (s : Set R),
theorem PrimeSpectrum.isClosed_iff_zeroLocus {R : Type u} [] (Z : Set ()) :
∃ (s : Set R),
theorem PrimeSpectrum.isClosed_iff_zeroLocus_ideal {R : Type u} [] (Z : Set ()) :
∃ (I : ),
theorem PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal {R : Type u} [] (Z : Set ()) :
theorem PrimeSpectrum.isClosed_zeroLocus {R : Type u} [] (s : Set R) :
theorem PrimeSpectrum.closure_singleton {R : Type u} [] (x : ) :
theorem PrimeSpectrum.isClosed_singleton_iff_isMaximal {R : Type u} [] (x : ) :
IsClosed {x} x.asIdeal.IsMaximal
theorem PrimeSpectrum.isRadical_vanishingIdeal {R : Type u} [] (s : Set ()) :
theorem PrimeSpectrum.vanishingIdeal_anti_mono_iff {R : Type u} [] {s : Set ()} {t : Set ()} (ht : ) :
theorem PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff {R : Type u} [] {s : Set ()} {t : Set ()} (hs : ) (ht : ) :

The antitone order embedding of closed subsets of Spec R into ideals of R.

Equations
Instances For
theorem PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical {R : Type u} [] (I : ) (hI : I.IsRadical) :
I.IsPrime
theorem PrimeSpectrum.isIrreducible_zeroLocus_iff {R : Type u} [] (I : ) :
theorem PrimeSpectrum.vanishingIdeal_isIrreducible {R : Type u} [] :
PrimeSpectrum.vanishingIdeal '' {s : Set () | } = {P : | P.IsPrime}
theorem PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible {R : Type u} [] :
PrimeSpectrum.vanishingIdeal '' {s : Set () | } = {P : | P.IsPrime}
instance PrimeSpectrum.irreducibleSpace {R : Type u} [] [] :
Equations
• =
instance PrimeSpectrum.quasiSober {R : Type u} [] :
Equations
• =
instance PrimeSpectrum.compactSpace {R : Type u} [] :

The prime spectrum of a commutative (semi)ring is a compact topological space.

Equations
• =
theorem PrimeSpectrum.preimage_comap_zeroLocus_aux {R : Type u} {S : Type v} [] [] (f : R →+* S) (s : Set R) :
(fun (y : ) => { asIdeal := Ideal.comap f y.asIdeal, isPrime := }) ⁻¹' = PrimeSpectrum.zeroLocus (f '' s)
def PrimeSpectrum.comap {R : Type u} {S : Type v} [] [] (f : R →+* S) :

The function between prime spectra of commutative (semi)rings induced by a ring homomorphism. This function is continuous.

Equations
• = { toFun := fun (y : ) => { asIdeal := Ideal.comap f y.asIdeal, isPrime := }, continuous_toFun := }
Instances For
@[simp]
theorem PrimeSpectrum.comap_asIdeal {R : Type u} {S : Type v} [] [] (f : R →+* S) (y : ) :
( y).asIdeal = Ideal.comap f y.asIdeal
@[simp]
theorem PrimeSpectrum.comap_id {R : Type u} [] :
@[simp]
theorem PrimeSpectrum.comap_comp {R : Type u} {S : Type v} [] [] {S' : Type u_1} [] (f : R →+* S) (g : S →+* S') :
PrimeSpectrum.comap (g.comp f) = .comp
theorem PrimeSpectrum.comap_comp_apply {R : Type u} {S : Type v} [] [] {S' : Type u_1} [] (f : R →+* S) (g : S →+* S') (x : ) :
(PrimeSpectrum.comap (g.comp f)) x = ( x)
@[simp]
theorem PrimeSpectrum.preimage_comap_zeroLocus {R : Type u} {S : Type v} [] [] (f : R →+* S) (s : Set R) :
theorem PrimeSpectrum.comap_injective_of_surjective {R : Type u} {S : Type v} [] [] (f : R →+* S) (hf : ) :
theorem PrimeSpectrum.localization_comap_inducing {R : Type u} (S : Type v) [] [] [Algebra R S] (M : ) [] :
Inducing ()
theorem PrimeSpectrum.localization_comap_injective {R : Type u} (S : Type v) [] [] [Algebra R S] (M : ) [] :
theorem PrimeSpectrum.localization_comap_embedding {R : Type u} (S : Type v) [] [] [Algebra R S] (M : ) [] :
Embedding ()
theorem PrimeSpectrum.localization_comap_range {R : Type u} (S : Type v) [] [] [Algebra R S] (M : ) [] :
Set.range () = {p : | Disjoint M p.asIdeal}
theorem PrimeSpectrum.comap_inducing_of_surjective {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : ) :

The comap of a surjective ring homomorphism is a closed embedding between the prime spectra.

theorem PrimeSpectrum.comap_singleton_isClosed_of_surjective {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : ) (x : ) (hx : IsClosed {x}) :
theorem PrimeSpectrum.comap_singleton_isClosed_of_isIntegral {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : f.IsIntegral) (x : ) (hx : IsClosed {x}) :
theorem PrimeSpectrum.image_comap_zeroLocus_eq_zeroLocus_comap {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : ) (I : ) :
theorem PrimeSpectrum.range_comap_of_surjective {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : ) :
theorem PrimeSpectrum.isClosed_range_comap_of_surjective {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : ) :
theorem PrimeSpectrum.closedEmbedding_comap_of_surjective {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : ) :
theorem PrimeSpectrum.primeSpectrumProd_symm_inl {R : Type u} {S : Type v} [] [] (x : ) :
.symm () = () x
theorem PrimeSpectrum.primeSpectrumProd_symm_inr {R : Type u} {S : Type v} [] [] (x : ) :
.symm () = () x
noncomputable def PrimeSpectrum.primeSpectrumProdHomeo {R : Type u} {S : Type v} [] [] :

The prime spectrum of R × S is homeomorphic to the disjoint union of PrimeSpectrum R and PrimeSpectrum S.

Equations
• PrimeSpectrum.primeSpectrumProdHomeo = (.symm.toHomeomorphOfInducing ).symm
Instances For
def PrimeSpectrum.basicOpen {R : Type u} [] (r : R) :

basicOpen r is the open subset containing all prime ideals not containing r.

Equations
• = { carrier := {x : | rx.asIdeal}, is_open' := }
Instances For
@[simp]
theorem PrimeSpectrum.mem_basicOpen {R : Type u} [] (f : R) (x : ) :
fx.asIdeal
theorem PrimeSpectrum.isOpen_basicOpen {R : Type u} [] {a : R} :
@[simp]
@[simp]
theorem PrimeSpectrum.basicOpen_one {R : Type u} [] :
@[simp]
theorem PrimeSpectrum.basicOpen_zero {R : Type u} [] :
theorem PrimeSpectrum.basicOpen_le_basicOpen_iff {R : Type u} [] (f : R) (g : R) :
theorem PrimeSpectrum.basicOpen_mul {R : Type u} [] (f : R) (g : R) :
theorem PrimeSpectrum.basicOpen_mul_le_left {R : Type u} [] (f : R) (g : R) :
theorem PrimeSpectrum.basicOpen_mul_le_right {R : Type u} [] (f : R) (g : R) :
@[simp]
theorem PrimeSpectrum.basicOpen_pow {R : Type u} [] (f : R) (n : ) (hn : 0 < n) :
@[simp]
theorem PrimeSpectrum.basicOpen_eq_bot_iff {R : Type u} [] (f : R) :
theorem PrimeSpectrum.localization_away_comap_range {R : Type u} [] (S : Type v) [] [Algebra R S] (r : R) [] :
Set.range () =
theorem PrimeSpectrum.localization_away_openEmbedding {R : Type u} [] (S : Type v) [] [Algebra R S] (r : R) [] :
theorem PrimeSpectrum.isCompact_basicOpen {R : Type u} [] (f : R) :
theorem PrimeSpectrum.comap_basicOpen {R : Type u} {S : Type v} [] [] (f : R →+* S) (x : R) :

## The specialization order #

We endow PrimeSpectrum R with a partial order, where x ≤ y if and only if y ∈ closure {x}.

instance PrimeSpectrum.instPartialOrder {R : Type u} [] :
Equations
@[simp]
theorem PrimeSpectrum.asIdeal_le_asIdeal {R : Type u} [] (x : ) (y : ) :
x.asIdeal y.asIdeal x y
@[simp]
theorem PrimeSpectrum.asIdeal_lt_asIdeal {R : Type u} [] (x : ) (y : ) :
x.asIdeal < y.asIdeal x < y
theorem PrimeSpectrum.le_iff_mem_closure {R : Type u} [] (x : ) (y : ) :
x y y closure {x}
theorem PrimeSpectrum.le_iff_specializes {R : Type u} [] (x : ) (y : ) :
x y x y
@[simp]
theorem PrimeSpectrum.nhdsOrderEmbedding_apply {R : Type u} [] (x : ) :
PrimeSpectrum.nhdsOrderEmbedding x = nhds x

nhds as an order embedding.

Equations
• PrimeSpectrum.nhdsOrderEmbedding =
Instances For
instance PrimeSpectrum.instT0Space {R : Type u} [] :
Equations
• =
Equations
• PrimeSpectrum.instOrderBotOfIsDomain =
instance PrimeSpectrum.instUnique {R : Type u_1} [] :
Equations
• PrimeSpectrum.instUnique = { default := , uniq := }
def PrimeSpectrum.localizationMapOfSpecializes {R : Type u} [] {x : } {y : } (h : x y) :

If x specializes to y, then there is a natural map from the localization of y to the localization of x.

Equations
Instances For

Zero loci of prime ideals are closed irreducible sets in the Zariski topology and any closed irreducible set is a zero locus of some prime ideal.

Equations
• = let __spread.0 := irreducibleSetEquivPoints.symm.trans OrderDual.toDual; { toEquiv := __spread.0, map_rel_iff' := }
Instances For
def PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal {R : Type u} [] {I : } [hI : I.IsPrime] (h : ) :

Localizations at minimal primes have single-point prime spectra.

Equations
Instances For

Stacks: Lemma 00ES (3) Zero loci of minimal prime ideals of R are irreducible components in Spec R and any irreducible component is a zero locus of some minimal prime ideal.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem PrimeSpectrum.vanishingIdeal_irreducibleComponents (R : Type u) [] :
PrimeSpectrum.vanishingIdeal '' =
theorem PrimeSpectrum.zeroLocus_minimalPrimes (R : Type u) [] :
PrimeSpectrum.zeroLocus SetLike.coe '' =
def LocalRing.closedPoint (R : Type u) [] [] :

The closed point in the prime spectrum of a local ring.

Equations
• = { asIdeal := , isPrime := }
Instances For
theorem LocalRing.isLocalRingHom_iff_comap_closedPoint {R : Type u} [] [] {S : Type v} [] [] (f : R →+* S) :
@[simp]
theorem LocalRing.comap_closedPoint {R : Type u} [] [] {S : Type v} [] [] (f : R →+* S) [] :
theorem LocalRing.specializes_closedPoint {R : Type u} [] [] (x : ) :
theorem LocalRing.closedPoint_mem_iff {R : Type u} [] [] (U : ) :
U =
@[simp]
theorem LocalRing.PrimeSpectrum.comap_residue (T : Type u) [] [] (x : ) :