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).

Main definitions

• PrimeSpectrum.zariskiTopology: the Zariski topology on the prime spectrum, whose closed sets are zero loci (zeroLocus).

• PrimeSpectrum.basicOpen: the complement of the zero locus of a single element. The basicOpens form a topological basis of the Zariski topology: PrimeSpectrum.isTopologicalBasis_basic_opens.

• PrimeSpectrum.comap: the continuous map between prime spectra induced by a ring homomorphism.

• IsLocalRing.closedPoint: the maximal ideal of a local ring is the unique closed point in its prime spectrum.

Main results

• PrimeSpectrum.instSpectralSpace: every prime spectrum is a spectral space, i.e. it is quasi-compact, sober (in particular T0), quasi-separated, and its compact open subsets form a topological basis.

• PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero: the prime spectrum of a commutative semiring is discrete iff it is finite and the semiring has zero Krull dimension or is trivial.

• PrimeSpectrum.localization_comap_range, PrimeSpectrum.localization_comap_isEmbedding: localization at a submonoid of a commutative semiring induces an embedding between the prime spectra, with range consisting of prime ideals disjoint from the submonoid.

• PrimeSpectrum.localization_away_comap_range: for localization away from an element, the range of the embedding is the basicOpen associated to the element.

• PrimeSpectrum.comap_isEmbedding_of_surjective: a surjective ring homomorphism between commutative semirings induces an embedding between the prime spectra.

• PrimeSpectrum.isClosedEmbedding_comap_of_surjective: a surjective ring homomorphism between commutative rings induces a closed embedding between the prime spectra.

• PrimeSpectrum.primeSpectrumProdHomeo: the prime spectrum of a product semiring is homeomorphic to the disjoint union of the prime spectra.

• PrimeSpectrum.stableUnderSpecialization_range_iff: the range of PrimeSpectrum.comap _ is closed iff it is stable under specialization.

• PrimeSpectrum.denseRange_comap_iff_minimalPrimes, PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical: the range of comap f is dense iff it contains all minimal primes, iff the kernel of f is contained in the nilradical.

• PrimeSpectrum.isClosedMap_comap_of_isIntegral: comap f is a closed map if f is integral.

• PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom: f : R →+* S is integral if comap (Polynomial.mapRingHom f : R[X] →+* S[X]) is a closed map.

In the prime spectrum of a commutative semiring:

• PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal, PrimeSpectrum.isRadical_vanishingIdeal, PrimeSpectrum.zeroLocus_eq_iff, PrimeSpectrum.vanishingIdeal_anti_mono_iff: closed subsets correspond to radical ideals.

• PrimeSpectrum.isClosed_singleton_iff_isMaximal: closed points correspond to maximal ideals.

• PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime: irreducible closed subsets correspond to prime ideals.

• minimalPrimes.equivIrreducibleComponents: irreducible components correspond to minimal primes.

• PrimeSpectrum.mulZeroAddOneEquivClopens: clopen subsets correspond to pairs of elements that add up to 1 and multiply to 0 in the semiring.

• PrimeSpectrum.isIdempotentElemEquivClopens: (if the semiring is a ring) clopen subsets correspond to idempotents in the ring.

@[implicit_reducible]

instance PrimeSpectrum.zariskiTopology {R : Type u} [CommSemiring R] : TopologicalSpace (PrimeSpectrum R)

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.

theorem PrimeSpectrum.isOpen_iff {R : Type u} [CommSemiring R] (U : Set (PrimeSpectrum R)) : IsOpen U ↔ ∃ (s : Set R), Uᶜ = zeroLocus s

theorem PrimeSpectrum.isClosed_iff_zeroLocus {R : Type u} [CommSemiring R] (Z : Set (PrimeSpectrum R)) : IsClosed Z ↔ ∃ (s : Set R), Z = zeroLocus s

theorem PrimeSpectrum.isClosed_iff_zeroLocus_ideal {R : Type u} [CommSemiring R] (Z : Set (PrimeSpectrum R)) : IsClosed Z ↔ ∃ (I : Ideal R), Z = zeroLocus ↑I

theorem PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal {R : Type u} [CommSemiring R] (Z : Set (PrimeSpectrum R)) : IsClosed Z ↔ ∃ (I : Ideal R), I.IsRadical ∧ Z = zeroLocus ↑I

theorem PrimeSpectrum.isClosed_zeroLocus {R : Type u} [CommSemiring R] (s : Set R) : IsClosed (zeroLocus s)

theorem PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) : zeroLocus ↑(vanishingIdeal t) = closure t

theorem PrimeSpectrum.vanishingIdeal_closure {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) : vanishingIdeal (closure t) = vanishingIdeal t

theorem PrimeSpectrum.closure_singleton {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) : closure {x} = zeroLocus ↑x.asIdeal

theorem PrimeSpectrum.isClosed_singleton_iff_isMaximal {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) : IsClosed {x} ↔ x.asIdeal.IsMaximal

theorem PrimeSpectrum.isRadical_vanishingIdeal {R : Type u} [CommSemiring R] (s : Set (PrimeSpectrum R)) : (vanishingIdeal s).IsRadical

theorem PrimeSpectrum.zeroLocus_eq_iff {R : Type u} [CommSemiring R] {I J : Ideal R} : zeroLocus ↑I = zeroLocus ↑J ↔ I.radical = J.radical

theorem PrimeSpectrum.vanishingIdeal_anti_mono_iff {R : Type u} [CommSemiring R] {s t : Set (PrimeSpectrum R)} (ht : IsClosed t) : s ⊆ t ↔ vanishingIdeal t ≤ vanishingIdeal s

theorem PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff {R : Type u} [CommSemiring R] {s t : Set (PrimeSpectrum R)} (hs : IsClosed s) (ht : IsClosed t) : s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s

def PrimeSpectrum.closedsEmbedding (R : Type u_1) [CommSemiring R] : (TopologicalSpace.Closeds (PrimeSpectrum R))ᵒᵈ ↪o Ideal R

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

theorem PrimeSpectrum.t1Space_iff_isField {R : Type u} [CommSemiring R] [IsDomain R] : T1Space (PrimeSpectrum R) ↔ IsField R

theorem PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical {R : Type u} [CommSemiring R] (I : Ideal R) (hI : I.IsRadical) : IsIrreducible (zeroLocus ↑I) ↔ I.IsPrime

theorem PrimeSpectrum.isIrreducible_zeroLocus_iff {R : Type u} [CommSemiring R] (I : Ideal R) : IsIrreducible (zeroLocus ↑I) ↔ I.radical.IsPrime

theorem PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : IsIrreducible s ↔ (vanishingIdeal s).IsPrime

theorem PrimeSpectrum.vanishingIdeal_isIrreducible {R : Type u} [CommSemiring R] : vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s} = {P : Ideal R | P.IsPrime}

theorem PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible {R : Type u} [CommSemiring R] : vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s} = {P : Ideal R | P.IsPrime}

theorem PrimeSpectrum.irreducibleSpace_iff_isPrime_nilradical {R : Type u} [CommSemiring R] : IrreducibleSpace (PrimeSpectrum R) ↔ (nilradical R).IsPrime

instance PrimeSpectrum.irreducibleSpace {R : Type u} [CommSemiring R] [IsDomain R] : IrreducibleSpace (PrimeSpectrum R)

instance PrimeSpectrum.quasiSober {R : Type u} [CommSemiring R] : QuasiSober (PrimeSpectrum R)

instance PrimeSpectrum.instQuasiSoberElemZeroLocus {R : Type u} [CommSemiring R] (I : Set R) : QuasiSober ↑(zeroLocus I)

instance PrimeSpectrum.compactSpace {R : Type u} [CommSemiring R] : CompactSpace (PrimeSpectrum R)

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

theorem PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero {R : Type u} [CommSemiring R] : DiscreteTopology (PrimeSpectrum R) ↔ Finite (PrimeSpectrum R) ∧ Ring.KrullDimLE 0 R

The prime spectrum of a commutative semiring has discrete Zariski topology iff it is finite and the semiring has Krull dimension zero or is trivial.

theorem PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical {R : Type u} [CommSemiring R] : DiscreteTopology (PrimeSpectrum R) ↔ Finite ↑{I : Ideal R | I.IsMaximal} ∧ sInf {I : Ideal R | I.IsMaximal} ≤ nilradical R

The prime spectrum of a semiring has discrete Zariski topology iff there are only finitely many maximal ideals and their intersection is contained in the nilradical.

theorem PrimeSpectrum.discreteTopology_of_toLocalization_surjective {R : Type u} [CommSemiring R] (surj : Function.Surjective ⇑(toPiLocalization R)) : DiscreteTopology (PrimeSpectrum R)

theorem PrimeSpectrum.continuous_comap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) : Continuous (comap f)

@[deprecated "RingHom.specComap and PrimeSpectrum.comap were unified,so this lemma is now a no-op." (since := "2025-12-10")]

theorem PrimeSpectrum.comap_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : PrimeSpectrum S) : comap f x = comap f x

theorem PrimeSpectrum.localization_comap_injective {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Function.Injective (comap (algebraMap R S))

@[deprecated PrimeSpectrum.localization_comap_injective (since := "2025-12-10")]

theorem PrimeSpectrum.localization_specComap_injective {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Function.Injective (comap (algebraMap R S))

Alias of PrimeSpectrum.localization_comap_injective.

theorem PrimeSpectrum.localization_comap_range {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Set.range (comap (algebraMap R S)) = {p : PrimeSpectrum R | Disjoint ↑M ↑p.asIdeal}

@[deprecated PrimeSpectrum.localization_comap_range (since := "2025-12-10")]

theorem PrimeSpectrum.localization_specComap_range {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Set.range (comap (algebraMap R S)) = {p : PrimeSpectrum R | Disjoint ↑M ↑p.asIdeal}

Alias of PrimeSpectrum.localization_comap_range.

theorem PrimeSpectrum.localization_comap_isInducing {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Topology.IsInducing (comap (algebraMap R S))

theorem PrimeSpectrum.localization_comap_isEmbedding {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Topology.IsEmbedding (comap (algebraMap R S))

theorem PrimeSpectrum.comap_isInducing_of_surjective {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) : Topology.IsInducing (comap f)

theorem PrimeSpectrum.isEmbedding_comap_of_surjective {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) : Topology.IsEmbedding (comap f)

The embedding has closed range if the domain (and therefore the codomain) is a ring, see PrimeSpectrum.isClosedEmbedding_comap_of_surjective. On the other hand, comap (Nat.castRingHom (ZMod 2)) does not have closed range.

def PrimeSpectrum.homeomorphOfRingEquiv {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : PrimeSpectrum R ≃ₜ PrimeSpectrum S

Homeomorphism between prime spectra induced by an isomorphism of semirings.

theorem PrimeSpectrum.isHomeomorph_comap_of_bijective {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {f : R →+* S} (hf : Function.Bijective ⇑f) : IsHomeomorph (comap f)

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) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (x : PrimeSpectrum S) (hx : IsClosed {x}) : IsClosed {comap f x}

theorem PrimeSpectrum.comap_quotientMk_bijective_of_le_nilradical {R : Type u} [CommRing R] {I : Ideal R} (hle : I ≤ nilradical R) : Function.Bijective (comap (Ideal.Quotient.mk I))

theorem PrimeSpectrum.isClosed_range_comap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) : IsClosed (Set.range (comap f))

theorem PrimeSpectrum.isClosedEmbedding_comap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) : Topology.IsClosedEmbedding (comap f)

theorem PrimeSpectrum.primeSpectrumProd_symm_inl {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (x : PrimeSpectrum R) : (primeSpectrumProd R S).symm (Sum.inl x) = comap (RingHom.fst R S) x

theorem PrimeSpectrum.primeSpectrumProd_symm_inr {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (x : PrimeSpectrum S) : (primeSpectrumProd R S).symm (Sum.inr x) = comap (RingHom.snd R S) x

theorem PrimeSpectrum.range_comap_fst {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] : Set.range (comap (RingHom.fst R S)) = zeroLocus ↑(RingHom.ker (RingHom.fst R S))

theorem PrimeSpectrum.range_comap_snd {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] : Set.range (comap (RingHom.snd R S)) = zeroLocus ↑(RingHom.ker (RingHom.snd R S))

theorem PrimeSpectrum.isClosedEmbedding_comap_fst {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] : Topology.IsClosedEmbedding (comap (RingHom.fst R S))

theorem PrimeSpectrum.isClosedEmbedding_comap_snd {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] : Topology.IsClosedEmbedding (comap (RingHom.snd R S))

noncomputable def PrimeSpectrum.primeSpectrumProdHomeo {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] : PrimeSpectrum (R × S) ≃ₜ PrimeSpectrum R ⊕ PrimeSpectrum S

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

def PrimeSpectrum.basicOpen {R : Type u} [CommSemiring R] (r : R) : TopologicalSpace.Opens (PrimeSpectrum R)

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

@[simp]

theorem PrimeSpectrum.mem_basicOpen {R : Type u} [CommSemiring R] (f : R) (x : PrimeSpectrum R) : x ∈ basicOpen f ↔ f ∉ x.asIdeal

theorem PrimeSpectrum.isOpen_basicOpen {R : Type u} [CommSemiring R] {a : R} : IsOpen ↑(basicOpen a)

@[simp]

theorem PrimeSpectrum.basicOpen_eq_zeroLocus_compl {R : Type u} [CommSemiring R] (r : R) : ↑(basicOpen r) = (zeroLocus {r})ᶜ

@[simp]

theorem PrimeSpectrum.basicOpen_one {R : Type u} [CommSemiring R] : basicOpen 1 = ⊤

@[simp]

theorem PrimeSpectrum.basicOpen_zero {R : Type u} [CommSemiring R] : basicOpen 0 = ⊥

theorem PrimeSpectrum.basicOpen_le_basicOpen_iff {R : Type u} [CommSemiring R] (f g : R) : basicOpen f ≤ basicOpen g ↔ f ∈ (Ideal.span {g}).radical

theorem PrimeSpectrum.basicOpen_le_basicOpen_iff_algebraMap_isUnit {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {f g : R} [Algebra R S] [IsLocalization.Away f S] : basicOpen f ≤ basicOpen g ↔ IsUnit ((algebraMap R S) g)

theorem PrimeSpectrum.basicOpen_mul {R : Type u} [CommSemiring R] (f g : R) : basicOpen (f * g) = basicOpen f ⊓ basicOpen g

theorem PrimeSpectrum.basicOpen_mul_le_left {R : Type u} [CommSemiring R] (f g : R) : basicOpen (f * g) ≤ basicOpen f

theorem PrimeSpectrum.basicOpen_mul_le_right {R : Type u} [CommSemiring R] (f g : R) : basicOpen (f * g) ≤ basicOpen g

@[simp]

theorem PrimeSpectrum.basicOpen_pow {R : Type u} [CommSemiring R] (f : R) (n : ℕ) (hn : 0 < n) : basicOpen (f ^ n) = basicOpen f

theorem PrimeSpectrum.le_basicOpen_pow {R : Type u} [CommSemiring R] (r : R) (n : ℕ) : basicOpen r ≤ basicOpen (r ^ n)

theorem PrimeSpectrum.isTopologicalBasis_basic_opens {R : Type u} [CommSemiring R] : TopologicalSpace.IsTopologicalBasis (Set.range fun (r : R) => ↑(basicOpen r))

theorem PrimeSpectrum.eq_biUnion_of_isOpen {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} (hs : IsOpen s) : s = ⋃ (r : R), ⋃ (_ : ↑(basicOpen r) ⊆ s), ↑(basicOpen r)

theorem PrimeSpectrum.isBasis_basic_opens {R : Type u} [CommSemiring R] : TopologicalSpace.Opens.IsBasis (Set.range basicOpen)

@[simp]

theorem PrimeSpectrum.basicOpen_eq_bot_iff {R : Type u} [CommSemiring R] (f : R) : basicOpen f = ⊥ ↔ IsNilpotent f

theorem PrimeSpectrum.localization_away_comap_range {R : Type u} [CommSemiring R] (S : Type v) [CommSemiring S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Set.range (comap (algebraMap R S)) = ↑(basicOpen r)

theorem PrimeSpectrum.localization_away_isOpenEmbedding {R : Type u} [CommSemiring R] (S : Type v) [CommSemiring S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Topology.IsOpenEmbedding (comap (algebraMap R S))

theorem PrimeSpectrum.isCompact_basicOpen {R : Type u} [CommSemiring R] (f : R) : IsCompact ↑(basicOpen f)

theorem PrimeSpectrum.comap_basicOpen {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : R) : (TopologicalSpace.Opens.comap { toFun := comap f, continuous_toFun := ⋯ }) (basicOpen x) = basicOpen (f x)

theorem PrimeSpectrum.iSup_basicOpen_eq_top_iff {R : Type u} [CommSemiring R] {ι : Type u_1} {f : ι → R} : ⨆ (i : ι), basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤

theorem PrimeSpectrum.iSup_basicOpen_eq_top_iff' {R : Type u} [CommSemiring R] {s : Set R} : ⨆ i ∈ s, basicOpen i = ⊤ ↔ Ideal.span s = ⊤

theorem PrimeSpectrum.isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] {f : R} {p : PrimeSpectrum R} (h : (basicOpen f).carrier = {p}) : IsLocalization.Away f S ↔ IsLocalization.AtPrime S p.asIdeal

theorem PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk {R : Type u_1} [CommRing R] (c : R) : (Set.range (comap (algebraMap (Polynomial R) (Polynomial (Localization.Away c)))))ᶜ = Set.range (comap (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

instance PrimeSpectrum.instQuasiSeparatedSpace {R : Type u} [CommSemiring R] : QuasiSeparatedSpace (PrimeSpectrum R)

theorem PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology (R : Type u) [CommSemiring R] [DiscreteTopology (PrimeSpectrum R)] : Function.Surjective ⇑(toPiLocalization R)

theorem PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology (R : Type u) [CommSemiring R] [DiscreteTopology (PrimeSpectrum R)] : Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R)

noncomputable def MaximalSpectrum.toPiLocalizationEquiv (R : Type u) [CommSemiring R] [DiscreteTopology (PrimeSpectrum R)] : R ≃+* PiLocalization R

If the prime spectrum of a commutative semiring R has discrete Zariski topology, then R is canonically isomorphic to the product of its localizations at the (finitely many) maximal ideals.

theorem PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective {R : Type u_1} [CommSemiring R] : DiscreteTopology (PrimeSpectrum R) ↔ Function.Surjective ⇑(toPiLocalization R)

theorem PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective {R : Type u_1} [CommSemiring R] : DiscreteTopology (PrimeSpectrum R) ↔ Function.Bijective ⇑(toPiLocalization R)

theorem PrimeSpectrum.toPiLocalization_bijective {R : Type u_1} [CommRing R] [DiscreteTopology (PrimeSpectrum R)] : Function.Bijective ⇑(toPiLocalization R)

The specialization order

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

theorem PrimeSpectrum.le_iff_mem_closure {R : Type u} [CommSemiring R] (x y : PrimeSpectrum R) : x ≤ y ↔ y ∈ closure {x}

theorem PrimeSpectrum.le_iff_specializes {R : Type u} [CommSemiring R] (x y : PrimeSpectrum R) : x ≤ y ↔ x ⤳ y

def PrimeSpectrum.nhdsOrderEmbedding {R : Type u} [CommSemiring R] : PrimeSpectrum R ↪o Filter (PrimeSpectrum R)

nhds as an order embedding.

@[simp]

theorem PrimeSpectrum.nhdsOrderEmbedding_apply {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) : nhdsOrderEmbedding x = nhds x

instance PrimeSpectrum.instT0Space {R : Type u} [CommSemiring R] : T0Space (PrimeSpectrum R)

instance PrimeSpectrum.instPrespectralSpace {R : Type u} [CommSemiring R] : PrespectralSpace (PrimeSpectrum R)

instance PrimeSpectrum.instSpectralSpace {R : Type u} [CommSemiring R] : SpectralSpace (PrimeSpectrum R)

noncomputable def PrimeSpectrum.localizationMapOfSpecializes {R : Type u} [CommSemiring R] {x y : PrimeSpectrum R} (h : x ⤳ y) : Localization.AtPrime y.asIdeal →+* Localization.AtPrime x.asIdeal

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

theorem PrimeSpectrum.isClosed_image_of_stableUnderSpecialization {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (Z : Set (PrimeSpectrum S)) (hZ : IsClosed Z) (hf : StableUnderSpecialization (comap f '' Z)) : IsClosed (comap f '' Z)

theorem PrimeSpectrum.isClosed_range_of_stableUnderSpecialization {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : StableUnderSpecialization (Set.range (comap f))) : IsClosed (Set.range (comap f))

Stacks Tag 00HY

theorem PrimeSpectrum.stableUnderSpecialization_range_iff {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {f : R →+* S} : StableUnderSpecialization (Set.range (comap f)) ↔ IsClosed (Set.range (comap f))

Stacks Tag 00HY

theorem PrimeSpectrum.stableUnderSpecialization_image_iff {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (Z : Set (PrimeSpectrum S)) (hZ : IsClosed Z) : StableUnderSpecialization (comap f '' Z) ↔ IsClosed (comap f '' Z)

theorem PrimeSpectrum.isQuotientMap_of_specializingMap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {f : R →+* S} (h₁ : Function.Surjective (comap f)) (h₂ : SpecializingMap (comap f)) : Topology.IsQuotientMap (comap f)

If f : Spec S → Spec R is specializing and surjective, the topology on Spec R is the quotient topology induced by f.

theorem PrimeSpectrum.isQuotientMap_of_generalizingMap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {f : R →+* S} (h₁ : Function.Surjective (comap f)) (h₂ : GeneralizingMap (comap f)) : Topology.IsQuotientMap (comap f)

If f : Spec S → Spec R is generalizing and surjective, the topology on Spec R is the quotient topology induced by f.

theorem PrimeSpectrum.vanishingIdeal_range_comap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) : vanishingIdeal (Set.range (comap f)) = (RingHom.ker f).radical

theorem PrimeSpectrum.closure_range_comap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) : closure (Set.range (comap f)) = zeroLocus ↑(RingHom.ker f)

theorem PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) : DenseRange (comap f) ↔ RingHom.ker f ≤ nilradical R

theorem PrimeSpectrum.denseRange_comap_iff_minimalPrimes {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) : DenseRange (comap f) ↔ ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)

Stacks Tag 00FL

noncomputable def PrimeSpectrum.pointsEquivIrreducibleCloseds (R : Type u) [CommSemiring R] : PrimeSpectrum R ≃o (TopologicalSpace.IrreducibleCloseds (PrimeSpectrum R))ᵒᵈ

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.

noncomputable def PrimeSpectrum.zeroLocusEquivIrreducibleCloseds {R : Type u} [CommSemiring R] (I : Set R) : ↑(zeroLocus I) ≃o (TopologicalSpace.IrreducibleCloseds ↑(zeroLocus I))ᵒᵈ

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.

theorem PrimeSpectrum.stableUnderSpecialization_singleton {R : Type u} [CommSemiring R] {x : PrimeSpectrum R} : StableUnderSpecialization {x} ↔ x.asIdeal.IsMaximal

theorem PrimeSpectrum.stableUnderGeneralization_singleton {R : Type u} [CommSemiring R] {x : PrimeSpectrum R} : StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R

theorem PrimeSpectrum.isCompact_isOpen_iff {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : IsCompact s ∧ IsOpen s ↔ ∃ (t : Finset R), (zeroLocus ↑t)ᶜ = s

theorem PrimeSpectrum.isCompact_isOpen_iff_ideal {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : IsCompact s ∧ IsOpen s ↔ ∃ (I : Ideal R), I.FG ∧ (zeroLocus ↑I)ᶜ = s

theorem PrimeSpectrum.basicOpen_eq_zeroLocus_of_mul_add {R : Type u} [CommSemiring R] (e f : R) (mul : e * f = 0) (add : e + f = 1) : ↑(basicOpen e) = zeroLocus {f}

theorem PrimeSpectrum.zeroLocus_eq_basicOpen_of_mul_add {R : Type u} [CommSemiring R] (e f : R) (mul : e * f = 0) (add : e + f = 1) : zeroLocus {e} = ↑(basicOpen f)

theorem PrimeSpectrum.isClopen_basicOpen_of_mul_add {R : Type u} [CommSemiring R] (e f : R) (mul : e * f = 0) (add : e + f = 1) : IsClopen ↑(basicOpen e)

theorem PrimeSpectrum.basicOpen_injOn_isIdempotentElem {R : Type u} [CommSemiring R] : Set.InjOn basicOpen {e : R | IsIdempotentElem e}

theorem PrimeSpectrum.exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} (hs : IsClopen s) : ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

theorem PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} (hs : IsClopen s) : ∃ (e : R), IsIdempotentElem e ∧ s = ↑(basicOpen e)

theorem PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} (hs : IsClopen s) : ∃! e : R, IsIdempotentElem e ∧ s = ↑(basicOpen e)

Stacks Tag 00EE

theorem PrimeSpectrum.isClopen_iff_mul_add {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : IsClopen s ↔ ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e)

theorem PrimeSpectrum.isClopen_iff_mul_add_zeroLocus {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : IsClopen s ↔ ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

noncomputable def PrimeSpectrum.mulZeroAddOneEquivClopens {R : Type u} [CommSemiring R] : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 } ≃o TopologicalSpace.Clopens (PrimeSpectrum R)

Clopen subsets in the prime spectrum of a commutative semiring are in order-preserving bijection with pairs of elements with product 0 and sum 1. (By definition, (e₁, f₁) ≤ (e₂, f₂) iff e₁ * e₂ = e₁.) Both elements in such pairs must be idempotents, but there may exists idempotents that do not form such pairs (does not have a "complement"). For example, in the semiring {0, 0.5, 1} with ⊔ as + and ⊓ as *, 0.5 has no complement.

theorem PrimeSpectrum.isRetrocompact_zeroLocus_compl {R : Type u} [CommSemiring R] {s : Set R} (hs : s.Finite) : IsRetrocompact (zeroLocus s)ᶜ

theorem PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg {R : Type u} [CommSemiring R] {I : Ideal R} (hI : I.FG) : IsRetrocompact (zeroLocus ↑I)ᶜ

theorem PrimeSpectrum.isRetrocompact_basicOpen {R : Type u} [CommSemiring R] {f : R} : IsRetrocompact ↑(basicOpen f)

theorem PrimeSpectrum.isConstructible_basicOpen {R : Type u} [CommSemiring R] {f : R} : Topology.IsConstructible ↑(basicOpen f)

theorem PrimeSpectrum.isClosedMap_comap_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) : IsClosedMap (comap f)

theorem PrimeSpectrum.isClosed_comap_singleton_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (x : PrimeSpectrum S) (hx : IsClosed {x}) : IsClosed {comap f x}

theorem PrimeSpectrum.closure_image_comap_zeroLocus {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (I : Ideal S) : closure (comap f '' zeroLocus ↑I) = zeroLocus ↑(Ideal.comap f I)

theorem PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (h : IsClosedMap (comap (Polynomial.mapRingHom f))) : f.IsIntegral

theorem RingHom.IsIntegral.comap_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsIntegral) (hinj : Function.Injective ⇑f) : Function.Surjective (PrimeSpectrum.comap f)

@[deprecated RingHom.IsIntegral.comap_surjective (since := "2025-12-10")]

theorem RingHom.IsIntegral.specComap_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.IsIntegral) (hinj : Function.Injective ⇑f) : Function.Surjective (PrimeSpectrum.comap f)

Alias of RingHom.IsIntegral.comap_surjective.

noncomputable def Ideal.minimalPrimes.equivIrreducibleComponents {R : Type u} [CommSemiring R] (I : Ideal R) : ↑I.minimalPrimes ≃o (↑(irreducibleComponents ↑(PrimeSpectrum.zeroLocus ↑I)))ᵒᵈ

Zero loci of minimal prime ideals over I are irreducible components in zeroLocus I and any irreducible component is a zero locus of some minimal prime ideal.

noncomputable def minimalPrimes.equivIrreducibleComponents (R : Type u) [CommSemiring R] : ↑(minimalPrimes R) ≃o (↑(irreducibleComponents (PrimeSpectrum R)))ᵒᵈ

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.

theorem PrimeSpectrum.vanishingIdeal_irreducibleComponents (R : Type u) [CommSemiring R] : vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) = minimalPrimes R

theorem PrimeSpectrum.zeroLocus_minimalPrimes (R : Type u) [CommSemiring R] : zeroLocus ∘ SetLike.coe '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R)

theorem PrimeSpectrum.vanishingIdeal_mem_minimalPrimes {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : vanishingIdeal s ∈ minimalPrimes R ↔ closure s ∈ irreducibleComponents (PrimeSpectrum R)

theorem PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents {R : Type u} [CommSemiring R] {I : Ideal R} : zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R

def IsLocalRing.closedPoint (R : Type u) [CommSemiring R] [IsLocalRing R] : PrimeSpectrum R

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

@[implicit_reducible]

instance IsLocalRing.instOrderTopPrimeSpectrum (R : Type u) [CommSemiring R] [IsLocalRing R] : OrderTop (PrimeSpectrum R)

@[implicit_reducible]

instance IsLocalRing.instBoundedOrderPrimeSpectrumOfIsDomain (R : Type u) [CommSemiring R] [IsLocalRing R] [IsDomain R] : BoundedOrder (PrimeSpectrum R)

@[simp]

theorem IsLocalRing.PrimeSpectrum.asIdeal_top (R : Type u) [CommSemiring R] [IsLocalRing R] : ⊤.asIdeal = maximalIdeal R

theorem IsLocalRing.isLocalHom_iff_comap_closedPoint {R : Type u} [CommSemiring R] [IsLocalRing R] {S : Type v} [CommSemiring S] [IsLocalRing S] (f : R →+* S) : IsLocalHom f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

@[simp]

theorem IsLocalRing.comap_closedPoint {R : Type u} [CommSemiring R] [IsLocalRing R] {S : Type v} [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] : PrimeSpectrum.comap f (closedPoint S) = closedPoint R

theorem IsLocalRing.specializes_closedPoint {R : Type u} [CommSemiring R] [IsLocalRing R] (x : PrimeSpectrum R) : x ⤳ closedPoint R

theorem IsLocalRing.closedPoint_mem_iff {R : Type u} [CommSemiring R] [IsLocalRing R] (U : TopologicalSpace.Opens (PrimeSpectrum R)) : closedPoint R ∈ U ↔ U = ⊤

theorem IsLocalRing.closed_point_mem_iff {R : Type u} [CommSemiring R] [IsLocalRing R] {U : TopologicalSpace.Opens (PrimeSpectrum R)} : closedPoint R ∈ U ↔ U = ⊤

@[simp]

theorem IsLocalRing.PrimeSpectrum.comap_residue (T : Type u) [CommRing T] [IsLocalRing T] (x : PrimeSpectrum (ResidueField T)) : PrimeSpectrum.comap (residue T) x = closedPoint T

theorem IsLocalRing.isClosed_singleton_closedPoint (R : Type u) [CommSemiring R] [IsLocalRing R] : IsClosed {closedPoint R}

theorem IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top {R : Type u} [CommSemiring R] [IsLocalRing R] [IsDomain R] [Ring.KrullDimLE 1 R] (x : PrimeSpectrum R) : x = ⊥ ∨ x = ⊤

theorem PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim (R : Type u) [CommSemiring R] : topologicalKrullDim (PrimeSpectrum R) = ringKrullDim R

theorem PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem {R : Type u} [CommRing R] (e : R) (he : IsIdempotentElem e) : ↑(basicOpen e) = zeroLocus {1 - e}

Stacks Tag 00EC

theorem PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem {R : Type u} [CommRing R] (e : R) (he : IsIdempotentElem e) : zeroLocus {e} = ↑(basicOpen (1 - e))

Stacks Tag 00EC

theorem PrimeSpectrum.isClopen_iff {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} : IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = ↑(basicOpen e)

theorem PrimeSpectrum.isClopen_iff_zeroLocus {R : Type u} [CommRing R] {s : Set (PrimeSpectrum R)} : IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = zeroLocus {e}

noncomputable def PrimeSpectrum.isIdempotentElemEquivClopens {R : Type u} [CommRing R] : { e : R // IsIdempotentElem e } ≃o TopologicalSpace.Clopens (PrimeSpectrum R)

Clopen subsets in the prime spectrum of a commutative ring are in 1-1 correspondence with idempotent elements in the ring.

theorem PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm {R : Type u} [CommRing R] (s : TopologicalSpace.Clopens (PrimeSpectrum R)) : basicOpen ↑(isIdempotentElemEquivClopens.symm s) = s.toOpens

theorem PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply {R : Type u} [CommRing R] (e : { e : R // IsIdempotentElem e }) : ↑(isIdempotentElemEquivClopens e) = ↑(basicOpen ↑e)

theorem PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens {R : Type u} [CommRing R] (e : { e : R // IsIdempotentElem e }) : (isIdempotentElemEquivClopens e).toOpens = basicOpen ↑e

theorem PrimeSpectrum.isIdempotentElemEquivClopens_mul {R : Type u} [CommRing R] (e₁ e₂ : ↑{e : R | IsIdempotentElem e}) : isIdempotentElemEquivClopens ⟨↑e₁ * ↑e₂, ⋯⟩ = isIdempotentElemEquivClopens e₁ ⊓ isIdempotentElemEquivClopens e₂

theorem PrimeSpectrum.isIdempotentElemEquivClopens_one_sub {R : Type u} [CommRing R] (e : ↑{e : R | IsIdempotentElem e}) : isIdempotentElemEquivClopens ⟨1 - ↑e, ⋯⟩ = (isIdempotentElemEquivClopens e)ᶜ

theorem PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf {R : Type u} [CommRing R] (s₁ s₂ : TopologicalSpace.Clopens (PrimeSpectrum R)) : isIdempotentElemEquivClopens.symm (s₁ ⊓ s₂) = ⟨↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂), ⋯⟩

theorem PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl {R : Type u} [CommRing R] (s : TopologicalSpace.Clopens (PrimeSpectrum R)) : isIdempotentElemEquivClopens.symm sᶜ = ⟨1 - ↑(isIdempotentElemEquivClopens.symm s), ⋯⟩

theorem PrimeSpectrum.isIdempotentElemEquivClopens_symm_top {R : Type u} [CommRing R] : isIdempotentElemEquivClopens.symm ⊤ = ⟨1, ⋯⟩

theorem PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot {R : Type u} [CommRing R] : isIdempotentElemEquivClopens.symm ⊥ = ⟨0, ⋯⟩

theorem PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup {R : Type u} [CommRing R] (s₁ s₂ : TopologicalSpace.Clopens (PrimeSpectrum R)) : isIdempotentElemEquivClopens.symm (s₁ ⊔ s₂) = ⟨↑(isIdempotentElemEquivClopens.symm s₁) + ↑(isIdempotentElemEquivClopens.symm s₂) - ↑(isIdempotentElemEquivClopens.symm s₁) * ↑(isIdempotentElemEquivClopens.symm s₂), ⋯⟩