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

Main definitions #

prime_spectrum R: The prime spectrum of a commutative ring R, i.e., the set of all prime ideals of R.
zero_locus s: The zero locus of a subset s of R is the subset of prime_spectrum R consisting of all prime ideals that contain s.
vanishing_ideal t: The vanishing ideal of a subset t of prime_spectrum 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).

source

@[nolint]

def prime_spectrum (R : Type u) [comm_ring 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 algebraic_geometry.structure_sheaf). It is a fundamental building block in algebraic geometry.

Equations

prime_spectrum R = {I // I.is_prime}

source

def prime_spectrum.as_ideal {R : Type u} [comm_ring R] (x : prime_spectrum R) :

ideal R

A method to view a point in the prime spectrum of a commutative ring as an ideal of that ring.

source

@[protected, instance]

def prime_spectrum.is_prime {R : Type u} [comm_ring R] (x : prime_spectrum R) :

x.as_ideal.is_prime

source

theorem prime_spectrum.punit (x : prime_spectrum punit) :

false

The prime spectrum of the zero ring is empty.

source

def prime_spectrum.prime_spectrum_prod (R : Type u) [comm_ring R] (S : Type v) [comm_ring S] :

prime_spectrum (R × S) ≃ prime_spectrum R ⊕ prime_spectrum 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

prime_spectrum.prime_spectrum_prod R S = ideal.prime_ideals_equiv R S

source

@[simp]

theorem prime_spectrum.prime_spectrum_prod_symm_inl_as_ideal {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (x : prime_spectrum R) :

(⇑((prime_spectrum.prime_spectrum_prod R S).symm) (sum.inl x)).as_ideal = x.as_ideal.prod ⊤

source

@[simp]

theorem prime_spectrum.prime_spectrum_prod_symm_inr_as_ideal {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (x : prime_spectrum S) :

(⇑((prime_spectrum.prime_spectrum_prod R S).symm) (sum.inr x)).as_ideal = ⊤.prod x.as_ideal

source

@[ext]

theorem prime_spectrum.ext {R : Type u} [comm_ring R] {x y : prime_spectrum R} :

x = y ↔ x.as_ideal = y.as_ideal

source

def prime_spectrum.zero_locus {R : Type u} [comm_ring R] (s : set R) :

set (prime_spectrum R)

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, zero_locus s is exactly the subset of prime_spectrum R where all "functions" in s vanish simultaneously.

Equations

prime_spectrum.zero_locus s = {x : prime_spectrum R | s ⊆ ↑(x.as_ideal)}

source

@[simp]

theorem prime_spectrum.mem_zero_locus {R : Type u} [comm_ring R] (x : prime_spectrum R) (s : set R) :

x ∈ prime_spectrum.zero_locus s ↔ s ⊆ ↑(x.as_ideal)

source

@[simp]

theorem prime_spectrum.zero_locus_span {R : Type u} [comm_ring R] (s : set R) :

prime_spectrum.zero_locus ↑(ideal.span s) = prime_spectrum.zero_locus s

source

def prime_spectrum.vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum 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, vanishing_ideal t is exactly the ideal of R consisting of all "functions" that vanish on all of t.

Equations

prime_spectrum.vanishing_ideal t = ⨅ (x : prime_spectrum R) (h : x ∈ t), x.as_ideal

source

theorem prime_spectrum.coe_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) :

↑(prime_spectrum.vanishing_ideal t) = {f : R | ∀ (x : prime_spectrum R), x ∈ t → f ∈ x.as_ideal}

source

theorem prime_spectrum.mem_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) (f : R) :

f ∈ prime_spectrum.vanishing_ideal t ↔ ∀ (x : prime_spectrum R), x ∈ t → f ∈ x.as_ideal

source

@[simp]

theorem prime_spectrum.vanishing_ideal_singleton {R : Type u} [comm_ring R] (x : prime_spectrum R) :

prime_spectrum.vanishing_ideal {x} = x.as_ideal

source

theorem prime_spectrum.subset_zero_locus_iff_le_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) (I : ideal R) :

t ⊆ prime_spectrum.zero_locus ↑I ↔ I ≤ prime_spectrum.vanishing_ideal t

source

theorem prime_spectrum.gc (R : Type u) [comm_ring R] :

galois_connection (λ (I : ideal R), prime_spectrum.zero_locus ↑I) (λ (t : order_dual (set (prime_spectrum R))), prime_spectrum.vanishing_ideal t)

zero_locus and vanishing_ideal form a galois connection.

source

theorem prime_spectrum.gc_set (R : Type u) [comm_ring R] :

galois_connection (λ (s : set R), prime_spectrum.zero_locus s) (λ (t : order_dual (set (prime_spectrum R))), ↑(prime_spectrum.vanishing_ideal t))

zero_locus and vanishing_ideal form a galois connection.

source

theorem prime_spectrum.subset_zero_locus_iff_subset_vanishing_ideal (R : Type u) [comm_ring R] (t : set (prime_spectrum R)) (s : set R) :

t ⊆ prime_spectrum.zero_locus s ↔ s ⊆ ↑(prime_spectrum.vanishing_ideal t)

source

theorem prime_spectrum.subset_vanishing_ideal_zero_locus {R : Type u} [comm_ring R] (s : set R) :

s ⊆ ↑(prime_spectrum.vanishing_ideal (prime_spectrum.zero_locus s))

source

theorem prime_spectrum.le_vanishing_ideal_zero_locus {R : Type u} [comm_ring R] (I : ideal R) :

I ≤ prime_spectrum.vanishing_ideal (prime_spectrum.zero_locus ↑I)

source

@[simp]

theorem prime_spectrum.vanishing_ideal_zero_locus_eq_radical {R : Type u} [comm_ring R] (I : ideal R) :

prime_spectrum.vanishing_ideal (prime_spectrum.zero_locus ↑I) = I.radical

source

@[simp]

theorem prime_spectrum.zero_locus_radical {R : Type u} [comm_ring R] (I : ideal R) :

prime_spectrum.zero_locus ↑(I.radical) = prime_spectrum.zero_locus ↑I

source

theorem prime_spectrum.subset_zero_locus_vanishing_ideal {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) :

t ⊆ prime_spectrum.zero_locus ↑(prime_spectrum.vanishing_ideal t)

source

theorem prime_spectrum.zero_locus_anti_mono {R : Type u} [comm_ring R] {s t : set R} (h : s ⊆ t) :

prime_spectrum.zero_locus t ⊆ prime_spectrum.zero_locus s

source

theorem prime_spectrum.zero_locus_anti_mono_ideal {R : Type u} [comm_ring R] {s t : ideal R} (h : s ≤ t) :

prime_spectrum.zero_locus ↑t ⊆ prime_spectrum.zero_locus ↑s

source

theorem prime_spectrum.vanishing_ideal_anti_mono {R : Type u} [comm_ring R] {s t : set (prime_spectrum R)} (h : s ⊆ t) :

prime_spectrum.vanishing_ideal t ≤ prime_spectrum.vanishing_ideal s

source

theorem prime_spectrum.zero_locus_subset_zero_locus_iff {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus ↑I ⊆ prime_spectrum.zero_locus ↑J ↔ J ≤ I.radical

source

theorem prime_spectrum.zero_locus_subset_zero_locus_singleton_iff {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.zero_locus {f} ⊆ prime_spectrum.zero_locus {g} ↔ g ∈ (ideal.span {f}).radical

source

theorem prime_spectrum.zero_locus_bot {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus ↑⊥ = set.univ

source

@[simp]

theorem prime_spectrum.zero_locus_singleton_zero {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus {0} = set.univ

source

@[simp]

theorem prime_spectrum.zero_locus_empty {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus ∅ = set.univ

source

@[simp]

theorem prime_spectrum.vanishing_ideal_univ {R : Type u} [comm_ring R] :

prime_spectrum.vanishing_ideal ∅ = ⊤

source

theorem prime_spectrum.zero_locus_empty_of_one_mem {R : Type u} [comm_ring R] {s : set R} (h : 1 ∈ s) :

prime_spectrum.zero_locus s = ∅

source

@[simp]

theorem prime_spectrum.zero_locus_singleton_one {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus {1} = ∅

source

theorem prime_spectrum.zero_locus_empty_iff_eq_top {R : Type u} [comm_ring R] {I : ideal R} :

prime_spectrum.zero_locus ↑I = ∅ ↔ I = ⊤

source

@[simp]

theorem prime_spectrum.zero_locus_univ {R : Type u} [comm_ring R] :

prime_spectrum.zero_locus set.univ = ∅

source

theorem prime_spectrum.zero_locus_sup {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus ↑(I ⊔ J) = prime_spectrum.zero_locus ↑I ∩ prime_spectrum.zero_locus ↑J

source

theorem prime_spectrum.zero_locus_union {R : Type u} [comm_ring R] (s s' : set R) :

prime_spectrum.zero_locus (s ∪ s') = prime_spectrum.zero_locus s ∩ prime_spectrum.zero_locus s'

source

theorem prime_spectrum.vanishing_ideal_union {R : Type u} [comm_ring R] (t t' : set (prime_spectrum R)) :

prime_spectrum.vanishing_ideal (t ∪ t') = prime_spectrum.vanishing_ideal t ⊓ prime_spectrum.vanishing_ideal t'

source

theorem prime_spectrum.zero_locus_supr {R : Type u} [comm_ring R] {ι : Sort u_1} (I : ι → ideal R) :

prime_spectrum.zero_locus (↑⨆ (i : ι), I i) = ⋂ (i : ι), prime_spectrum.zero_locus ↑(I i)

source

theorem prime_spectrum.zero_locus_Union {R : Type u} [comm_ring R] {ι : Sort u_1} (s : ι → set R) :

prime_spectrum.zero_locus (⋃ (i : ι), s i) = ⋂ (i : ι), prime_spectrum.zero_locus (s i)

source

theorem prime_spectrum.zero_locus_bUnion {R : Type u} [comm_ring R] (s : set (set R)) :

prime_spectrum.zero_locus (⋃ (s' : set R) (H : s' ∈ s), s') = ⋂ (s' : set R) (H : s' ∈ s), prime_spectrum.zero_locus s'

source

theorem prime_spectrum.vanishing_ideal_Union {R : Type u} [comm_ring R] {ι : Sort u_1} (t : ι → set (prime_spectrum R)) :

prime_spectrum.vanishing_ideal (⋃ (i : ι), t i) = ⨅ (i : ι), prime_spectrum.vanishing_ideal (t i)

source

theorem prime_spectrum.zero_locus_inf {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus ↑(I ⊓ J) = prime_spectrum.zero_locus ↑I ∪ prime_spectrum.zero_locus ↑J

source

theorem prime_spectrum.union_zero_locus {R : Type u} [comm_ring R] (s s' : set R) :

prime_spectrum.zero_locus s ∪ prime_spectrum.zero_locus s' = prime_spectrum.zero_locus ↑(ideal.span s ⊓ ideal.span s')

source

theorem prime_spectrum.zero_locus_mul {R : Type u} [comm_ring R] (I J : ideal R) :

prime_spectrum.zero_locus (↑I * J) = prime_spectrum.zero_locus ↑I ∪ prime_spectrum.zero_locus ↑J

source

theorem prime_spectrum.zero_locus_singleton_mul {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.zero_locus {f * g} = prime_spectrum.zero_locus {f} ∪ prime_spectrum.zero_locus {g}

source

@[simp]

theorem prime_spectrum.zero_locus_pow {R : Type u} [comm_ring R] (I : ideal R) {n : ℕ} (hn : 0 < n) :

prime_spectrum.zero_locus ↑(I ^ n) = prime_spectrum.zero_locus ↑I

source

@[simp]

theorem prime_spectrum.zero_locus_singleton_pow {R : Type u} [comm_ring R] (f : R) (n : ℕ) (hn : 0 < n) :

prime_spectrum.zero_locus {f ^ n} = prime_spectrum.zero_locus {f}

source

theorem prime_spectrum.sup_vanishing_ideal_le {R : Type u} [comm_ring R] (t t' : set (prime_spectrum R)) :

prime_spectrum.vanishing_ideal t ⊔ prime_spectrum.vanishing_ideal t' ≤ prime_spectrum.vanishing_ideal (t ∩ t')

source

theorem prime_spectrum.mem_compl_zero_locus_iff_not_mem {R : Type u} [comm_ring R] {f : R} {I : prime_spectrum R} :

I ∈ (prime_spectrum.zero_locus {f})ᶜ ↔ f ∉ I.as_ideal

source

@[protected, instance]

def prime_spectrum.zariski_topology {R : Type u} [comm_ring R] :

topological_space (prime_spectrum R)

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.

Equations

prime_spectrum.zariski_topology = topological_space.of_closed (set.range prime_spectrum.zero_locus) prime_spectrum.zariski_topology._proof_1 prime_spectrum.zariski_topology._proof_2 prime_spectrum.zariski_topology._proof_3

source

theorem prime_spectrum.is_open_iff {R : Type u} [comm_ring R] (U : set (prime_spectrum R)) :

is_open U ↔ ∃ (s : set R), Uᶜ = prime_spectrum.zero_locus s

source

theorem prime_spectrum.is_closed_iff_zero_locus {R : Type u} [comm_ring R] (Z : set (prime_spectrum R)) :

is_closed Z ↔ ∃ (s : set R), Z = prime_spectrum.zero_locus s

source

theorem prime_spectrum.is_closed_zero_locus {R : Type u} [comm_ring R] (s : set R) :

is_closed (prime_spectrum.zero_locus s)

source

theorem prime_spectrum.zero_locus_vanishing_ideal_eq_closure {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) :

prime_spectrum.zero_locus ↑(prime_spectrum.vanishing_ideal t) = closure t

source

theorem prime_spectrum.vanishing_ideal_closure {R : Type u} [comm_ring R] (t : set (prime_spectrum R)) :

prime_spectrum.vanishing_ideal (closure t) = prime_spectrum.vanishing_ideal t

source

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

prime_spectrum S → prime_spectrum R

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

Equations

prime_spectrum.comap f = λ (y : prime_spectrum S), ⟨ideal.comap f y.as_ideal, _⟩

source

@[simp]

theorem prime_spectrum.comap_as_ideal {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (y : prime_spectrum S) :

(prime_spectrum.comap f y).as_ideal = ideal.comap f y.as_ideal

source

@[simp]

theorem prime_spectrum.comap_id {R : Type u} [comm_ring R] :

prime_spectrum.comap (ring_hom.id R) = id

source

@[simp]

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

prime_spectrum.comap (g.comp f) = prime_spectrum.comap f ∘ prime_spectrum.comap g

source

@[simp]

theorem prime_spectrum.preimage_comap_zero_locus {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (s : set R) :

prime_spectrum.comap f ⁻¹' prime_spectrum.zero_locus s = prime_spectrum.zero_locus (⇑f '' s)

source

theorem prime_spectrum.comap_continuous {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) :

continuous (prime_spectrum.comap f)

source

def prime_spectrum.basic_open {R : Type u} [comm_ring R] (r : R) :

topological_space.opens (prime_spectrum R)

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

Equations

prime_spectrum.basic_open r = ⟨{x : prime_spectrum R | r ∉ x.as_ideal}, _⟩

source

@[simp]

theorem prime_spectrum.mem_basic_open {R : Type u} [comm_ring R] (f : R) (x : prime_spectrum R) :

x ∈ prime_spectrum.basic_open f ↔ f ∉ x.as_ideal

source

theorem prime_spectrum.is_open_basic_open {R : Type u} [comm_ring R] {a : R} :

is_open ↑(prime_spectrum.basic_open a)

source

@[simp]

theorem prime_spectrum.basic_open_eq_zero_locus_compl {R : Type u} [comm_ring R] (r : R) :

↑(prime_spectrum.basic_open r) = (prime_spectrum.zero_locus {r})ᶜ

source

@[simp]

theorem prime_spectrum.basic_open_one {R : Type u} [comm_ring R] :

prime_spectrum.basic_open 1 = ⊤

source

@[simp]

theorem prime_spectrum.basic_open_zero {R : Type u} [comm_ring R] :

prime_spectrum.basic_open 0 = ⊥

source

theorem prime_spectrum.basic_open_le_basic_open_iff {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open f ≤ prime_spectrum.basic_open g ↔ f ∈ (ideal.span {g}).radical

source

theorem prime_spectrum.basic_open_mul {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open (f * g) = prime_spectrum.basic_open f ⊓ prime_spectrum.basic_open g

source

theorem prime_spectrum.basic_open_mul_le_left {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open (f * g) ≤ prime_spectrum.basic_open f

source

theorem prime_spectrum.basic_open_mul_le_right {R : Type u} [comm_ring R] (f g : R) :

prime_spectrum.basic_open (f * g) ≤ prime_spectrum.basic_open g

source

@[simp]

theorem prime_spectrum.basic_open_pow {R : Type u} [comm_ring R] (f : R) (n : ℕ) (hn : 0 < n) :

prime_spectrum.basic_open (f ^ n) = prime_spectrum.basic_open f

source

theorem prime_spectrum.is_topological_basis_basic_opens {R : Type u} [comm_ring R] :

topological_space.is_topological_basis (set.range (λ (r : R), ↑(prime_spectrum.basic_open r)))

source

theorem prime_spectrum.is_compact_basic_open {R : Type u} [comm_ring R] (f : R) :

is_compact ↑(prime_spectrum.basic_open f)

source

@[protected, instance]

def prime_spectrum.compact_space {R : Type u} [comm_ring R] :

compact_space (prime_spectrum R)

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

The specialization order #

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

TODO: maybe define sober topological spaces, and generalise this instance to those

source

@[protected, instance]

def prime_spectrum.partial_order {R : Type u} [comm_ring R] :

partial_order (prime_spectrum R)

Equations

prime_spectrum.partial_order = subtype.partial_order (λ (I : ideal R), I.is_prime)

source

@[simp]

theorem prime_spectrum.as_ideal_le_as_ideal {R : Type u} [comm_ring R] (x y : prime_spectrum R) :

x.as_ideal ≤ y.as_ideal ↔ x ≤ y

source

@[simp]

theorem prime_spectrum.as_ideal_lt_as_ideal {R : Type u} [comm_ring R] (x y : prime_spectrum R) :

x.as_ideal < y.as_ideal ↔ x < y

source

theorem prime_spectrum.le_iff_mem_closure {R : Type u} [comm_ring R] (x y : prime_spectrum R) :

x ≤ y ↔ y ∈ closure {x}