Prime spectrum of a commutative (semi)ring

For the Zariski topology, see Mathlib.RingTheory.Spectrum.Prime.Topology.

(It is also naturally endowed with a sheaf of rings, which is constructed in AlgebraicGeometry.StructureSheaf.)

Main definitions

• zeroLocus s: The zero locus of a subset s of R is the subset of PrimeSpectrum R consisting of all prime ideals that contain s.
• vanishingIdeal t: The vanishing ideal of a subset t of PrimeSpectrum R is the intersection of points in t (viewed as prime ideals).

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

References

• M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra
• P. Samuel, Algebraic Theory of Numbers

instance PrimeSpectrum.instNonemptyOfNontrivial {R : Type u} [CommSemiring R] [Nontrivial R] : Nonempty (PrimeSpectrum R)

instance PrimeSpectrum.instIsEmptyOfSubsingleton {R : Type u} [CommSemiring R] [Subsingleton R] : IsEmpty (PrimeSpectrum R)

The prime spectrum of the zero ring is empty.

def PrimeSpectrum.equivSubtype (R : Type u) [CommSemiring R] : PrimeSpectrum R ≃ { I : Ideal R // I.IsPrime }

The prime spectrum is in bijection with the set of prime ideals.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PrimeSpectrum.equivSubtype_symm_apply_asIdeal (R : Type u) [CommSemiring R] (I : { I : Ideal R // I.IsPrime }) : ((equivSubtype R).symm I).asIdeal = ↑I

@[simp]

theorem PrimeSpectrum.equivSubtype_apply_coe (R : Type u) [CommSemiring R] (I : PrimeSpectrum R) : ↑((equivSubtype R) I) = I.asIdeal

theorem PrimeSpectrum.range_asIdeal (R : Type u) [CommSemiring R] : Set.range asIdeal = {J : Ideal R | J.IsPrime}

def PrimeSpectrum.primeSpectrumProdOfSum (R : Type u) (S : Type v) [CommSemiring R] [CommSemiring S] : PrimeSpectrum R ⊕ PrimeSpectrum S → PrimeSpectrum (R × S)

The map from the direct sum of prime spectra to the prime spectrum of a direct product.

Equations

• PrimeSpectrum.primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := isPrime }) = { asIdeal := I.prod ⊤, isPrime := ⋯ }
• PrimeSpectrum.primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := isPrime }) = { asIdeal := ⊤.prod J, isPrime := ⋯ }

noncomputable def PrimeSpectrum.primeSpectrumProd (R : Type u) (S : Type v) [CommSemiring R] [CommSemiring S] : PrimeSpectrum (R × S) ≃ PrimeSpectrum R ⊕ PrimeSpectrum S

The prime spectrum of R × S is in bijection with the disjoint unions of the prime spectrum of R and the prime spectrum of S.

Equations

• PrimeSpectrum.primeSpectrumProd R S = (Equiv.ofBijective (PrimeSpectrum.primeSpectrumProdOfSum R S) ⋯).symm

@[simp]

theorem PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (x : PrimeSpectrum R) : ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = x.asIdeal.prod ⊤

@[simp]

theorem PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (x : PrimeSpectrum S) : ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = ⊤.prod x.asIdeal

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

The zero locus of a set s of elements of a commutative (semi)ring R is the set of all prime ideals of the ring that contain the set s.

An element f of R can be thought of as a dependent function on the prime spectrum of R. At a point x (a prime ideal) the function (i.e., element) f takes values in the quotient ring R modulo the prime ideal x. In this manner, zeroLocus s is exactly the subset of PrimeSpectrum R where all "functions" in s vanish simultaneously.

Equations

• PrimeSpectrum.zeroLocus s = {x : PrimeSpectrum R | s ⊆ ↑x.asIdeal}

@[simp]

theorem PrimeSpectrum.mem_zeroLocus {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) (s : Set R) : x ∈ zeroLocus s ↔ s ⊆ ↑x.asIdeal

@[simp]

theorem PrimeSpectrum.zeroLocus_span {R : Type u} [CommSemiring R] (s : Set R) : zeroLocus ↑(Ideal.span s) = zeroLocus s

def PrimeSpectrum.vanishingIdeal {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) : Ideal R

The vanishing ideal of a set t of points of the prime spectrum of a commutative ring R is the intersection of all the prime ideals in the set t.

An element f of R can be thought of as a dependent function on the prime spectrum of R. At a point x (a prime ideal) the function (i.e., element) f takes values in the quotient ring R modulo the prime ideal x. In this manner, vanishingIdeal t is exactly the ideal of R consisting of all "functions" that vanish on all of t.

Equations

• PrimeSpectrum.vanishingIdeal t = ⨅ x ∈ t, x.asIdeal

theorem PrimeSpectrum.coe_vanishingIdeal {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) : ↑(vanishingIdeal t) = {f : R | ∀ x ∈ t, f ∈ x.asIdeal}

theorem PrimeSpectrum.mem_vanishingIdeal {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) (f : R) : f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal

@[simp]

theorem PrimeSpectrum.vanishingIdeal_singleton {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) : vanishingIdeal {x} = x.asIdeal

theorem PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) (I : Ideal R) : t ⊆ zeroLocus ↑I ↔ I ≤ vanishingIdeal t

theorem PrimeSpectrum.gc (R : Type u) [CommSemiring R] : GaloisConnection (fun (I : Ideal R) => zeroLocus ↑I) fun (t : (Set (PrimeSpectrum R))ᵒᵈ) => vanishingIdeal t

zeroLocus and vanishingIdeal form a galois connection.

theorem PrimeSpectrum.gc_set (R : Type u) [CommSemiring R] : GaloisConnection (fun (s : Set R) => zeroLocus s) fun (t : (Set (PrimeSpectrum R))ᵒᵈ) => ↑(vanishingIdeal t)

zeroLocus and vanishingIdeal form a galois connection.

theorem PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal (R : Type u) [CommSemiring R] (t : Set (PrimeSpectrum R)) (s : Set R) : t ⊆ zeroLocus s ↔ s ⊆ ↑(vanishingIdeal t)

theorem PrimeSpectrum.subset_vanishingIdeal_zeroLocus {R : Type u} [CommSemiring R] (s : Set R) : s ⊆ ↑(vanishingIdeal (zeroLocus s))

theorem PrimeSpectrum.le_vanishingIdeal_zeroLocus {R : Type u} [CommSemiring R] (I : Ideal R) : I ≤ vanishingIdeal (zeroLocus ↑I)

@[simp]

theorem PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical {R : Type u} [CommSemiring R] (I : Ideal R) : vanishingIdeal (zeroLocus ↑I) = I.radical

theorem PrimeSpectrum.nilradical_eq_iInf {R : Type u} [CommSemiring R] : nilradical R = iInf asIdeal

@[simp]

theorem PrimeSpectrum.zeroLocus_radical {R : Type u} [CommSemiring R] (I : Ideal R) : zeroLocus ↑I.radical = zeroLocus ↑I

theorem PrimeSpectrum.subset_zeroLocus_vanishingIdeal {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) : t ⊆ zeroLocus ↑(vanishingIdeal t)

theorem PrimeSpectrum.zeroLocus_anti_mono {R : Type u} [CommSemiring R] {s t : Set R} (h : s ⊆ t) : zeroLocus t ⊆ zeroLocus s

theorem PrimeSpectrum.zeroLocus_anti_mono_ideal {R : Type u} [CommSemiring R] {s t : Ideal R} (h : s ≤ t) : zeroLocus ↑t ⊆ zeroLocus ↑s

theorem PrimeSpectrum.vanishingIdeal_anti_mono {R : Type u} [CommSemiring R] {s t : Set (PrimeSpectrum R)} (h : s ⊆ t) : vanishingIdeal t ≤ vanishingIdeal s

theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_iff {R : Type u} [CommSemiring R] (I J : Ideal R) : zeroLocus ↑I ⊆ zeroLocus ↑J ↔ J ≤ I.radical

theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff {R : Type u} [CommSemiring R] (f g : R) : zeroLocus {f} ⊆ zeroLocus {g} ↔ g ∈ (Ideal.span {f}).radical

theorem PrimeSpectrum.zeroLocus_bot {R : Type u} [CommSemiring R] : zeroLocus ↑⊥ = Set.univ

@[simp]

theorem PrimeSpectrum.zeroLocus_singleton_zero {R : Type u} [CommSemiring R] : zeroLocus {0} = Set.univ

@[simp]

theorem PrimeSpectrum.zeroLocus_empty {R : Type u} [CommSemiring R] : zeroLocus ∅ = Set.univ

@[simp]

theorem PrimeSpectrum.vanishingIdeal_empty {R : Type u} [CommSemiring R] : vanishingIdeal ∅ = ⊤

theorem PrimeSpectrum.zeroLocus_empty_of_one_mem {R : Type u} [CommSemiring R] {s : Set R} (h : 1 ∈ s) : zeroLocus s = ∅

@[simp]

theorem PrimeSpectrum.zeroLocus_singleton_one {R : Type u} [CommSemiring R] : zeroLocus {1} = ∅

theorem PrimeSpectrum.zeroLocus_empty_iff_eq_top {R : Type u} [CommSemiring R] {I : Ideal R} : zeroLocus ↑I = ∅ ↔ I = ⊤

@[simp]

theorem PrimeSpectrum.zeroLocus_univ {R : Type u} [CommSemiring R] : zeroLocus Set.univ = ∅

theorem PrimeSpectrum.vanishingIdeal_eq_top_iff {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} : vanishingIdeal s = ⊤ ↔ s = ∅

theorem PrimeSpectrum.zeroLocus_eq_top_iff {R : Type u} [CommSemiring R] (s : Set R) : zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical R)

theorem PrimeSpectrum.zeroLocus_sup {R : Type u} [CommSemiring R] (I J : Ideal R) : zeroLocus ↑(I ⊔ J) = zeroLocus ↑I ∩ zeroLocus ↑J

theorem PrimeSpectrum.zeroLocus_union {R : Type u} [CommSemiring R] (s s' : Set R) : zeroLocus (s ∪ s') = zeroLocus s ∩ zeroLocus s'

theorem PrimeSpectrum.vanishingIdeal_union {R : Type u} [CommSemiring R] (t t' : Set (PrimeSpectrum R)) : vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'

theorem PrimeSpectrum.zeroLocus_iSup {R : Type u} [CommSemiring R] {ι : Sort u_1} (I : ι → Ideal R) : zeroLocus ↑(⨆ (i : ι), I i) = ⋂ (i : ι), zeroLocus ↑(I i)

theorem PrimeSpectrum.zeroLocus_iUnion {R : Type u} [CommSemiring R] {ι : Sort u_1} (s : ι → Set R) : zeroLocus (⋃ (i : ι), s i) = ⋂ (i : ι), zeroLocus (s i)

theorem PrimeSpectrum.zeroLocus_iUnion₂ {R : Type u} [CommSemiring R] {ι : Sort u_1} {κ : ι → Sort u_2} (s : (i : ι) → κ i → Set R) : zeroLocus (⋃ (i : ι), ⋃ (j : κ i), s i j) = ⋂ (i : ι), ⋂ (j : κ i), zeroLocus (s i j)

theorem PrimeSpectrum.zeroLocus_bUnion {R : Type u} [CommSemiring R] (s : Set (Set R)) : zeroLocus (⋃ s' ∈ s, s') = ⋂ s' ∈ s, zeroLocus s'

theorem PrimeSpectrum.vanishingIdeal_iUnion {R : Type u} [CommSemiring R] {ι : Sort u_1} (t : ι → Set (PrimeSpectrum R)) : vanishingIdeal (⋃ (i : ι), t i) = ⨅ (i : ι), vanishingIdeal (t i)

theorem PrimeSpectrum.zeroLocus_inf {R : Type u} [CommSemiring R] (I J : Ideal R) : zeroLocus ↑(I ⊓ J) = zeroLocus ↑I ∪ zeroLocus ↑J

theorem PrimeSpectrum.union_zeroLocus {R : Type u} [CommSemiring R] (s s' : Set R) : zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')

theorem PrimeSpectrum.zeroLocus_mul {R : Type u} [CommSemiring R] (I J : Ideal R) : zeroLocus ↑(I * J) = zeroLocus ↑I ∪ zeroLocus ↑J

theorem PrimeSpectrum.zeroLocus_singleton_mul {R : Type u} [CommSemiring R] (f g : R) : zeroLocus {f * g} = zeroLocus {f} ∪ zeroLocus {g}

@[simp]

theorem PrimeSpectrum.zeroLocus_pow {R : Type u} [CommSemiring R] (I : Ideal R) {n : ℕ} (hn : n ≠ 0) : zeroLocus ↑(I ^ n) = zeroLocus ↑I

@[simp]

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

theorem PrimeSpectrum.sup_vanishingIdeal_le {R : Type u} [CommSemiring R] (t t' : Set (PrimeSpectrum R)) : vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

theorem PrimeSpectrum.mem_compl_zeroLocus_iff_not_mem {R : Type u} [CommSemiring R] {f : R} {I : PrimeSpectrum R} : I ∈ (zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal

@[simp]

theorem PrimeSpectrum.zeroLocus_insert_zero {R : Type u} [CommSemiring R] (s : Set R) : zeroLocus (insert 0 s) = zeroLocus s

@[simp]

theorem PrimeSpectrum.zeroLocus_diff_singleton_zero {R : Type u} [CommSemiring R] (s : Set R) : zeroLocus (s \ {0}) = zeroLocus s

theorem PrimeSpectrum.zeroLocus_smul_of_isUnit {R : Type u} [CommSemiring R] {r : R} (hr : IsUnit r) (s : Set R) : zeroLocus (r • s) = zeroLocus s

The specialization order

We endow PrimeSpectrum R with a partial order induced from the ideal lattice. This is exactly the specialization order. See the corresponding section at Mathlib.RingTheory.Spectrum.Prime.Topology.

instance PrimeSpectrum.instPartialOrder {R : Type u} [CommSemiring R] : PartialOrder (PrimeSpectrum R)

Equations

• PrimeSpectrum.instPartialOrder = PartialOrder.lift PrimeSpectrum.asIdeal ⋯

@[simp]

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

@[simp]

theorem PrimeSpectrum.asIdeal_lt_asIdeal {R : Type u} [CommSemiring R] (x y : PrimeSpectrum R) : x.asIdeal < y.asIdeal ↔ x < y

instance PrimeSpectrum.instOrderBotOfIsDomain {R : Type u} [CommSemiring R] [IsDomain R] : OrderBot (PrimeSpectrum R)

Equations

• PrimeSpectrum.instOrderBotOfIsDomain = OrderBot.mk ⋯

instance PrimeSpectrum.instUnique {R : Type u_1} [Field R] : Unique (PrimeSpectrum R)

Equations

• PrimeSpectrum.instUnique = { default := ⊥, uniq := ⋯ }

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

Also see PrimeSpectrum.isClosed_singleton_iff_isMaximal

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

theorem PrimeSpectrum.exists_primeSpectrum_prod_le (R : Type u) [CommRing R] [IsNoetherianRing R] (I : Ideal R) : ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map asIdeal Z).prod ≤ I

In a noetherian ring, every ideal contains a product of prime ideals ([samuel1967, § 3.3, Lemma 3]).

theorem PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A] (h_fA : ¬IsField A) {I : Ideal A} (h_nzI : I ≠ ⊥) : ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as product or prime ideals ([samuel1967, § 3.3, Lemma 3])