# Documentation

Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic

# Prime spectrum of a commutative ring #

The prime spectrum of a commutative ring is the type of all prime ideals. It is naturally endowed with a topology: the Zariski topology.

(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 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 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_iff {R : Type u} :
∀ {inst : } (x y : ), x = y x.asIdeal = y.asIdeal
theorem PrimeSpectrum.ext {R : Type u} :
∀ {inst : } (x y : ), x.asIdeal = y.asIdealx = y
structure PrimeSpectrum (R : Type u) [] :

The prime spectrum of a commutative 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.

Instances For

The prime spectrum of the zero ring is empty.

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.

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.

Instances For
@[simp]
theorem PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal {R : Type u} {S : Type v} [] [] (x : ) :
(().symm ()).asIdeal = Ideal.prod x.asIdeal
@[simp]
theorem PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal {R : Type u} {S : Type v} [] [] (x : ) :
(().symm ()).asIdeal = Ideal.prod x.asIdeal
def PrimeSpectrum.zeroLocus {R : Type u} [] (s : Set R) :
Set ()

The zero locus of a set s of elements of a commutative 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.

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.

Instances For
theorem PrimeSpectrum.coe_vanishingIdeal {R : Type u} [] (t : Set ()) :
= {f | ∀ (x : ), x tf x.asIdeal}
theorem PrimeSpectrum.mem_vanishingIdeal {R : Type u} [] (t : Set ()) (f : R) :
∀ (x : ), x tf x.asIdeal
@[simp]
theorem PrimeSpectrum.vanishingIdeal_singleton {R : Type u} [] (x : ) :
= x.asIdeal
theorem PrimeSpectrum.gc (R : Type u) [] :
GaloisConnection (fun I => ) fun t =>

zeroLocus and vanishingIdeal form a galois connection.

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

zeroLocus and vanishingIdeal form a galois connection.

@[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_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_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_bUnion {R : Type u} [] (s : Set (Set R)) :
PrimeSpectrum.zeroLocus (⋃ (s' : Set R) (_ : s' s), s') = ⋂ (s' : Set R) (_ : 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 : 0 < n) :
@[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 () ¬f I.asIdeal
instance PrimeSpectrum.zariskiTopology {R : Type u} [] :

The Zariski topology on the prime spectrum of a commutative 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} [] (U : Set ()) :
s,
theorem PrimeSpectrum.isClosed_iff_zeroLocus {R : Type u} [] (Z : Set ()) :
s,
theorem PrimeSpectrum.isClosed_iff_zeroLocus_ideal {R : Type u} [] (Z : Set ()) :
I,
theorem PrimeSpectrum.isClosed_zeroLocus {R : Type u} [] (s : Set R) :
theorem PrimeSpectrum.closure_singleton {R : Type u} [] (x : ) :
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.

Instances For
instance PrimeSpectrum.quasiSober {R : Type u} [] :
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 := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹' = PrimeSpectrum.zeroLocus (f '' s)
def PrimeSpectrum.comap {R : Type u} {S : Type v} [] [] (f : R →+* S) :

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

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} [CommRing S'] (f : R →+* S) (g : S →+* S') :
theorem PrimeSpectrum.comap_comp_apply {R : Type u} {S : Type v} [] [] {S' : Type u_1} [CommRing S'] (f : R →+* S) (g : S →+* S') (x : ) :
↑() 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.comap_singleton_isClosed_of_surjective {R : Type u} {S : Type v} [] [] (f : R →+* S) (hf : ) (x : ) (hx : IsClosed {x}) :
IsClosed {↑() x}
theorem PrimeSpectrum.comap_singleton_isClosed_of_isIntegral {R : Type u} {S : Type v} [] [] (f : R →+* S) (hf : ) (x : ) (hx : IsClosed {x}) :
IsClosed {↑() x}
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}

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

theorem PrimeSpectrum.comap_inducing_of_surjective {R : Type u} (S : Type v) [] [] (f : R →+* S) (hf : ) :
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 : ) :
def PrimeSpectrum.basicOpen {R : Type u} [] (r : R) :

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

Instances For
@[simp]
theorem PrimeSpectrum.mem_basicOpen {R : Type u} [] (f : R) (x : ) :
¬f x.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) :
theorem PrimeSpectrum.isCompact_basicOpen {R : Type u} [] (f : R) :
@[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) [] :
instance PrimeSpectrum.compactSpace {R : Type u} [] :

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

## The specialization order #

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

@[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} [] (a : ) :
PrimeSpectrum.nhdsOrderEmbedding a = nhds a

nhds as an order embedding.

Instances For
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.

Instances For
def LocalRing.closedPoint (R : Type u) [] [] :

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

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 {R : Type u} [] [] (x : ) :