# Prime spectrum of a commutative (semi)ring as a type #

The prime spectrum of a commutative (semi)ring is the type of all prime ideals.

For the Zariski topology, see AlgebraicGeometry.PrimeSpectrum.Basic.

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

## Main definitions #

• PrimeSpectrum R: The prime spectrum of a commutative (semi)ring R, i.e., the set of all prime ideals of R.
• 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).

theorem PrimeSpectrum.ext {R : Type u} :
∀ {inst : } {x y : }, x.asIdeal = y.asIdealx = y
theorem PrimeSpectrum.ext_iff {R : Type u} :
∀ {inst : } {x y : }, x = y x.asIdeal = y.asIdeal
structure PrimeSpectrum (R : Type u) [] :

The prime spectrum of a commutative (semi)ring R is the type of all prime ideals of R.

It is naturally endowed with a topology (the Zariski topology), and a sheaf of commutative rings (see AlgebraicGeometry.StructureSheaf). It is a fundamental building block in algebraic geometry.

• asIdeal :
• isPrime : self.asIdeal.IsPrime
Instances For
theorem PrimeSpectrum.isPrime {R : Type u} [] (self : ) :
self.asIdeal.IsPrime
@[deprecated PrimeSpectrum.isPrime]
theorem PrimeSpectrum.IsPrime {R : Type u} [] (self : ) :
self.asIdeal.IsPrime

Alias of PrimeSpectrum.isPrime.

Equations
• =

The prime spectrum of the zero ring is empty.

Equations
• =
def PrimeSpectrum.primeSpectrumProdOfSum (R : Type u) (S : Type v) [] [] :
PrimeSpectrum (R × S)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def PrimeSpectrum.primeSpectrumProd (R : Type u) (S : Type v) [] [] :

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
Instances For
@[simp]
theorem PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal {R : Type u} {S : Type v} [] [] (x : ) :
(.symm (Sum.inl x)).asIdeal = x.asIdeal.prod
@[simp]
theorem PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal {R : Type u} {S : Type v} [] [] (x : ) :
(.symm (Sum.inr x)).asIdeal = .prod x.asIdeal
def PrimeSpectrum.zeroLocus {R : Type u} [] (s : Set 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
• = {x : | s x.asIdeal}
Instances For
@[simp]
theorem PrimeSpectrum.mem_zeroLocus {R : Type u} [] (x : ) (s : Set R) :
s x.asIdeal
@[simp]
theorem PrimeSpectrum.zeroLocus_span {R : Type u} [] (s : Set R) :
def PrimeSpectrum.vanishingIdeal {R : Type u} [] (t : Set ) :

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
• = xt, x.asIdeal
Instances For
theorem PrimeSpectrum.coe_vanishingIdeal {R : Type u} [] (t : Set ) :
= {f : R | xt, f x.asIdeal}
theorem PrimeSpectrum.mem_vanishingIdeal {R : Type u} [] (t : Set ) (f : R) :
xt, f x.asIdeal
@[simp]
theorem PrimeSpectrum.vanishingIdeal_singleton {R : Type u} [] (x : ) :
= x.asIdeal
theorem PrimeSpectrum.gc (R : Type u) [] :
GaloisConnection (fun (I : ) => ) fun (t : (Set )ᵒᵈ) =>

zeroLocus and vanishingIdeal form a galois connection.

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

zeroLocus and vanishingIdeal form a galois connection.

@[simp]
theorem PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical {R : Type u} [] (I : ) :
@[simp]
theorem PrimeSpectrum.zeroLocus_radical {R : Type u} [] (I : ) :
theorem PrimeSpectrum.zeroLocus_anti_mono {R : Type u} [] {s : Set R} {t : Set R} (h : s t) :
theorem PrimeSpectrum.zeroLocus_anti_mono_ideal {R : Type u} [] {s : } {t : } (h : s t) :
theorem PrimeSpectrum.vanishingIdeal_anti_mono {R : Type u} [] {s : Set } {t : Set } (h : s t) :
theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_iff {R : Type u} [] (I : ) (J : ) :
theorem PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff {R : Type u} [] (f : R) (g : R) :
theorem PrimeSpectrum.zeroLocus_bot {R : Type u} [] :
= Set.univ
@[simp]
theorem PrimeSpectrum.zeroLocus_singleton_zero {R : Type u} [] :
= Set.univ
@[simp]
theorem PrimeSpectrum.zeroLocus_empty {R : Type u} [] :
= Set.univ
@[simp]
theorem PrimeSpectrum.zeroLocus_empty_of_one_mem {R : Type u} [] {s : Set R} (h : 1 s) :
theorem PrimeSpectrum.zeroLocus_eq_top_iff {R : Type u} [] (s : Set R) :
theorem PrimeSpectrum.zeroLocus_sup {R : Type u} [] (I : ) (J : ) :
theorem PrimeSpectrum.zeroLocus_union {R : Type u} [] (s : Set R) (s' : Set R) :
theorem PrimeSpectrum.vanishingIdeal_union {R : Type u} [] (t : Set ) (t' : Set ) :
theorem PrimeSpectrum.zeroLocus_iSup {R : Type u} [] {ι : Sort u_1} (I : ι) :
PrimeSpectrum.zeroLocus (⨆ (i : ι), I i) = ⋂ (i : ι), PrimeSpectrum.zeroLocus (I i)
theorem PrimeSpectrum.zeroLocus_iUnion {R : Type u} [] {ι : Sort u_1} (s : ιSet R) :
PrimeSpectrum.zeroLocus (⋃ (i : ι), s i) = ⋂ (i : ι),
theorem PrimeSpectrum.zeroLocus_iUnion₂ {R : Type u} [] {ι : Sort u_1} {κ : ιSort u_2} (s : (i : ι) → κ iSet R) :
PrimeSpectrum.zeroLocus (⋃ (i : ι), ⋃ (j : κ i), s i j) = ⋂ (i : ι), ⋂ (j : κ i), PrimeSpectrum.zeroLocus (s i j)
theorem PrimeSpectrum.zeroLocus_bUnion {R : Type u} [] (s : Set (Set R)) :
PrimeSpectrum.zeroLocus (⋃ s's, s') = s's,
theorem PrimeSpectrum.vanishingIdeal_iUnion {R : Type u} [] {ι : Sort u_1} (t : ιSet ) :
PrimeSpectrum.vanishingIdeal (⋃ (i : ι), t i) = ⨅ (i : ι),
theorem PrimeSpectrum.zeroLocus_inf {R : Type u} [] (I : ) (J : ) :
theorem PrimeSpectrum.union_zeroLocus {R : Type u} [] (s : Set R) (s' : Set R) :
theorem PrimeSpectrum.zeroLocus_mul {R : Type u} [] (I : ) (J : ) :
theorem PrimeSpectrum.zeroLocus_singleton_mul {R : Type u} [] (f : R) (g : R) :
@[simp]
theorem PrimeSpectrum.zeroLocus_pow {R : Type u} [] (I : ) {n : } (hn : n 0) :
@[simp]
theorem PrimeSpectrum.zeroLocus_singleton_pow {R : Type u} [] (f : R) (n : ) (hn : 0 < n) :
theorem PrimeSpectrum.sup_vanishingIdeal_le {R : Type u} [] (t : Set ) (t' : Set ) :
theorem PrimeSpectrum.mem_compl_zeroLocus_iff_not_mem {R : Type u} [] {f : R} {I : } :
I fI.asIdeal

## 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 AlgebraicGeometry/PrimeSpectrum/Basic.

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
Equations
• PrimeSpectrum.instOrderBotOfIsDomain =
instance PrimeSpectrum.instUnique {R : Type u_1} [] :
Equations
• PrimeSpectrum.instUnique = { default := , uniq := }
theorem PrimeSpectrum.exists_primeSpectrum_prod_le (R : Type u) [] [] (I : ) :
∃ (Z : ), (Multiset.map PrimeSpectrum.asIdeal Z).prod I

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

theorem PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain {A : Type u} [] [] [] (h_fA : ¬) {I : } (h_nzI : I ) :
∃ (Z : ), (Multiset.map PrimeSpectrum.asIdeal Z).prod I (Multiset.map PrimeSpectrum.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 ([samuel, § 3.3, Lemma 3])