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

source

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.

Equations

PrimeSpectrum.zariskiTopology = TopologicalSpace.ofClosed (Set.range PrimeSpectrum.zeroLocus) ⋯ ⋯ ⋯

source

theorem PrimeSpectrum.isOpen_iff {R : Type u} [CommSemiring R] (U : Set (PrimeSpectrum R)) :

IsOpen U ↔ ∃ (s : Set R), Uᶜ = PrimeSpectrum.zeroLocus s

source

theorem PrimeSpectrum.isClosed_iff_zeroLocus {R : Type u} [CommSemiring R] (Z : Set (PrimeSpectrum R)) :

IsClosed Z ↔ ∃ (s : Set R), Z = PrimeSpectrum.zeroLocus s

source

theorem PrimeSpectrum.isClosed_iff_zeroLocus_ideal {R : Type u} [CommSemiring R] (Z : Set (PrimeSpectrum R)) :

IsClosed Z ↔ ∃ (I : Ideal R), Z = PrimeSpectrum.zeroLocus ↑I

source

theorem PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal {R : Type u} [CommSemiring R] (Z : Set (PrimeSpectrum R)) :

IsClosed Z ↔ ∃ (I : Ideal R), I.IsRadical ∧ Z = PrimeSpectrum.zeroLocus ↑I

source

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

IsClosed (PrimeSpectrum.zeroLocus s)

source

theorem PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) :

PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t) = closure t

source

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

PrimeSpectrum.vanishingIdeal (closure t) = PrimeSpectrum.vanishingIdeal t

source

theorem PrimeSpectrum.closure_singleton {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) :

closure {x} = PrimeSpectrum.zeroLocus ↑x.asIdeal

source

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

IsClosed {x} ↔ x.asIdeal.IsMaximal

source

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

(PrimeSpectrum.vanishingIdeal s).IsRadical

source

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

s ⊆ t ↔ PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s

source

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

s ⊂ t ↔ PrimeSpectrum.vanishingIdeal t < PrimeSpectrum.vanishingIdeal s

source

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.

Equations

PrimeSpectrum.closedsEmbedding R = OrderEmbedding.ofMapLEIff (fun (s : (TopologicalSpace.Closeds (PrimeSpectrum R))ᵒᵈ) => PrimeSpectrum.vanishingIdeal ↑(OrderDual.ofDual s)) ⋯

Instances For

source

theorem PrimeSpectrum.t1Space_iff_isField {R : Type u} [CommSemiring R] [IsDomain R] :

T1Space (PrimeSpectrum R) ↔ IsField R

source

theorem PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical {R : Type u} [CommSemiring R] (I : Ideal R) (hI : I.IsRadical) :

IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.IsPrime

source

theorem PrimeSpectrum.isIrreducible_zeroLocus_iff {R : Type u} [CommSemiring R] (I : Ideal R) :

IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.radical.IsPrime

source

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

IsIrreducible s ↔ (PrimeSpectrum.vanishingIdeal s).IsPrime

source

theorem PrimeSpectrum.vanishingIdeal_isIrreducible {R : Type u} [CommSemiring R] :

PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s} = {P : Ideal R | P.IsPrime}

source

theorem PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible {R : Type u} [CommSemiring R] :

PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s} = {P : Ideal R | P.IsPrime}

source

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

IrreducibleSpace (PrimeSpectrum R)

Equations

⋯ = ⋯

source

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

QuasiSober (PrimeSpectrum R)

Equations

⋯ = ⋯

source

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

CompactSpace (PrimeSpectrum R)

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

Equations

⋯ = ⋯

source

theorem PrimeSpectrum.preimage_comap_zeroLocus_aux {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :

(fun (y : PrimeSpectrum S) => { asIdeal := Ideal.comap f y.asIdeal, isPrime := ⋯ }) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)

source

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

C(PrimeSpectrum S, PrimeSpectrum R)

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

Equations

PrimeSpectrum.comap f = { toFun := fun (y : PrimeSpectrum S) => { asIdeal := Ideal.comap f y.asIdeal, isPrime := ⋯ }, continuous_toFun := ⋯ }

Instances For

source

@[simp]

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

((PrimeSpectrum.comap f) y).asIdeal = Ideal.comap f y.asIdeal

source

@[simp]

theorem PrimeSpectrum.comap_id {R : Type u} [CommSemiring R] :

PrimeSpectrum.comap (RingHom.id R) = ContinuousMap.id (PrimeSpectrum R)

source

@[simp]

theorem PrimeSpectrum.comap_comp {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {S' : Type u_1} [CommSemiring S'] (f : R →+* S) (g : S →+* S') :

PrimeSpectrum.comap (g.comp f) = (PrimeSpectrum.comap f).comp (PrimeSpectrum.comap g)

source

theorem PrimeSpectrum.comap_comp_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {S' : Type u_1} [CommSemiring S'] (f : R →+* S) (g : S →+* S') (x : PrimeSpectrum S') :

(PrimeSpectrum.comap (g.comp f)) x = (PrimeSpectrum.comap f) ((PrimeSpectrum.comap g) x)

source

@[simp]

theorem PrimeSpectrum.preimage_comap_zeroLocus {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :

⇑(PrimeSpectrum.comap f) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)

source

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

Function.Injective ⇑(PrimeSpectrum.comap f)

source

theorem PrimeSpectrum.localization_comap_inducing {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] :

Inducing ⇑(PrimeSpectrum.comap (algebraMap R S))

source

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 ⇑(PrimeSpectrum.comap (algebraMap R S))

source

theorem PrimeSpectrum.localization_comap_embedding {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] :

Embedding ⇑(PrimeSpectrum.comap (algebraMap R S))

source

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 ⇑(PrimeSpectrum.comap (algebraMap R S)) = {p : PrimeSpectrum R | Disjoint ↑M ↑p.asIdeal}

source

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

Inducing ⇑(PrimeSpectrum.comap f)

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

source

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 {(PrimeSpectrum.comap f) x}

source

theorem PrimeSpectrum.comap_singleton_isClosed_of_isIntegral {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (x : PrimeSpectrum S) (hx : IsClosed {x}) :

IsClosed {(PrimeSpectrum.comap f) x}

source

theorem PrimeSpectrum.image_comap_zeroLocus_eq_zeroLocus_comap {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (I : Ideal S) :

⇑(PrimeSpectrum.comap f) '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)

source

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

Set.range ⇑(PrimeSpectrum.comap f) = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)

source

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 ⇑(PrimeSpectrum.comap f))

source

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

ClosedEmbedding ⇑(PrimeSpectrum.comap f)

source

theorem PrimeSpectrum.primeSpectrumProd_symm_inl {R : Type u} {S : Type v} [CommRing R] [CommRing S] (x : PrimeSpectrum R) :

(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x) = (PrimeSpectrum.comap (RingHom.fst R S)) x

source

theorem PrimeSpectrum.primeSpectrumProd_symm_inr {R : Type u} {S : Type v} [CommRing R] [CommRing S] (x : PrimeSpectrum S) :

(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x) = (PrimeSpectrum.comap (RingHom.snd R S)) x

source

noncomputable def PrimeSpectrum.primeSpectrumProdHomeo {R : Type u} {S : Type v} [CommRing R] [CommRing 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.

Equations

PrimeSpectrum.primeSpectrumProdHomeo = ((PrimeSpectrum.primeSpectrumProd R S).symm.toHomeomorphOfInducing ⋯).symm

Instances For

source

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.

Equations

PrimeSpectrum.basicOpen r = { carrier := {x : PrimeSpectrum R | r ∉ x.asIdeal}, is_open' := ⋯ }

Instances For

source

@[simp]

theorem PrimeSpectrum.mem_basicOpen {R : Type u} [CommSemiring R] (f : R) (x : PrimeSpectrum R) :

x ∈ PrimeSpectrum.basicOpen f ↔ f ∉ x.asIdeal

source

theorem PrimeSpectrum.isOpen_basicOpen {R : Type u} [CommSemiring R] {a : R} :

IsOpen ↑(PrimeSpectrum.basicOpen a)

source

@[simp]

theorem PrimeSpectrum.basicOpen_eq_zeroLocus_compl {R : Type u} [CommSemiring R] (r : R) :

↑(PrimeSpectrum.basicOpen r) = (PrimeSpectrum.zeroLocus {r})ᶜ

source

@[simp]

theorem PrimeSpectrum.basicOpen_one {R : Type u} [CommSemiring R] :

PrimeSpectrum.basicOpen 1 = ⊤

source

@[simp]

theorem PrimeSpectrum.basicOpen_zero {R : Type u} [CommSemiring R] :

PrimeSpectrum.basicOpen 0 = ⊥

source

theorem PrimeSpectrum.basicOpen_le_basicOpen_iff {R : Type u} [CommSemiring R] (f : R) (g : R) :

PrimeSpectrum.basicOpen f ≤ PrimeSpectrum.basicOpen g ↔ f ∈ (Ideal.span {g}).radical

source

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

PrimeSpectrum.basicOpen (f * g) = PrimeSpectrum.basicOpen f ⊓ PrimeSpectrum.basicOpen g

source

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

PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen f

source

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

PrimeSpectrum.basicOpen (f * g) ≤ PrimeSpectrum.basicOpen g

source

@[simp]

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

PrimeSpectrum.basicOpen (f ^ n) = PrimeSpectrum.basicOpen f

source

theorem PrimeSpectrum.isTopologicalBasis_basic_opens {R : Type u} [CommSemiring R] :

TopologicalSpace.IsTopologicalBasis (Set.range fun (r : R) => ↑(PrimeSpectrum.basicOpen r))

source

theorem PrimeSpectrum.isBasis_basic_opens {R : Type u} [CommSemiring R] :

TopologicalSpace.Opens.IsBasis (Set.range PrimeSpectrum.basicOpen)

source

@[simp]

theorem PrimeSpectrum.basicOpen_eq_bot_iff {R : Type u} [CommSemiring R] (f : R) :

PrimeSpectrum.basicOpen f = ⊥ ↔ IsNilpotent f

source

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 ⇑(PrimeSpectrum.comap (algebraMap R S)) = ↑(PrimeSpectrum.basicOpen r)

source

theorem PrimeSpectrum.localization_away_openEmbedding {R : Type u} [CommSemiring R] (S : Type v) [CommSemiring S] [Algebra R S] (r : R) [IsLocalization.Away r S] :

OpenEmbedding ⇑(PrimeSpectrum.comap (algebraMap R S))

source

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

IsCompact ↑(PrimeSpectrum.basicOpen f)

source

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

(TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) (PrimeSpectrum.basicOpen x) = PrimeSpectrum.basicOpen (f x)

source

theorem PrimeSpectrum.iSup_basicOpen_eq_top_iff {R : Type u} [CommSemiring R] {ι : Type u_1} {f : ι → R} :

⨆ (i : ι), PrimeSpectrum.basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤

source

theorem PrimeSpectrum.iSup_basicOpen_eq_top_iff' {R : Type u} [CommSemiring R] {s : Set R} :

⨆ i ∈ s, PrimeSpectrum.basicOpen i = ⊤ ↔ Ideal.span s = ⊤

The specialization order #

We endow PrimeSpectrum R with a partial order, where x ≤ y if and only if y ∈ closure {x}. This instance was defined in RingTheory/PrimeSpectrum/Basic.

source

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

x ≤ y ↔ y ∈ closure {x}

source

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

x ≤ y ↔ x ⤳ y

source

@[simp]

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

PrimeSpectrum.nhdsOrderEmbedding x = nhds x

source

def PrimeSpectrum.nhdsOrderEmbedding {R : Type u} [CommSemiring R] :

PrimeSpectrum R ↪o Filter (PrimeSpectrum R)

nhds as an order embedding.

Equations

PrimeSpectrum.nhdsOrderEmbedding = OrderEmbedding.ofMapLEIff nhds ⋯

Instances For

source

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

T0Space (PrimeSpectrum R)

Equations

⋯ = ⋯

source

def PrimeSpectrum.localizationMapOfSpecializes {R : Type u} [CommSemiring R] {x : PrimeSpectrum R} {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.

Equations

PrimeSpectrum.localizationMapOfSpecializes h = IsLocalization.lift ⋯

Instances For

source

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.

Equations

PrimeSpectrum.pointsEquivIrreducibleCloseds R = let __spread.0 := irreducibleSetEquivPoints.symm.trans OrderDual.toDual; { toEquiv := __spread.0, map_rel_iff' := ⋯ }

Instances For

source

def PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal {R : Type u} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] (h : I ∈ minimalPrimes R) :

Unique (PrimeSpectrum (Localization.AtPrime I))

Localizations at minimal primes have single-point prime spectra.

Equations

PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal h = { default := { asIdeal := LocalRing.maximalIdeal (Localization I.primeCompl), isPrime := ⋯ }, uniq := ⋯ }

Instances For

source

def minimalPrimes.equivIrreducibleComponents (R : Type u) [CommSemiring R] :

↑(minimalPrimes R) ≃o (↑(irreducibleComponents (PrimeSpectrum R)))ᵒᵈ

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