Prime spectrum of a commutative ring #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 ringR, i.e., the set of all prime ideals ofR.zero_locus s: The zero locus of a subsetsofRis the subset ofprime_spectrum Rconsisting of all prime ideals that contains.vanishing_ideal t: The vanishing ideal of a subsettofprime_spectrum Ris the intersection of points int(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).
@[ext]
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.
Instances for prime_spectrum
- prime_spectrum.has_sizeof_inst
- prime_spectrum.nonempty
- prime_spectrum.zariski_topology
- prime_spectrum.irreducible_space
- prime_spectrum.quasi_sober
- prime_spectrum.compact_space
- prime_spectrum.partial_order
- prime_spectrum.t0_space
- prime_spectrum.order_bot
- prime_spectrum.unique
- prime_spectrum.topological_space.noetherian_space
theorem
prime_spectrum.ext
{R : Type u}
{_inst_1 : comm_ring R}
(x y : prime_spectrum R)
(h : x.as_ideal = y.as_ideal) :
x = y
@[protected, instance]
The prime spectrum of the zero ring is empty.
@[simp]
def
prime_spectrum.prime_spectrum_prod_of_sum
(R : Type u)
(S : Type v)
[comm_ring R]
[comm_ring S] :
prime_spectrum R ⊕ prime_spectrum S → prime_spectrum (R × S)
The map from the direct sum of prime spectra to the prime spectrum of a direct product.
noncomputable
def
prime_spectrum.prime_spectrum_prod
(R : Type u)
(S : Type v)
[comm_ring R]
[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
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)}
@[simp]
theorem
prime_spectrum.mem_zero_locus
{R : Type u}
[comm_ring R]
(x : prime_spectrum R)
(s : set R) :
@[simp]
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
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}
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
@[simp]
theorem
prime_spectrum.vanishing_ideal_singleton
{R : Type u}
[comm_ring R]
(x : prime_spectrum R) :
theorem
prime_spectrum.subset_zero_locus_iff_le_vanishing_ideal
{R : Type u}
[comm_ring R]
(t : set (prime_spectrum R))
(I : ideal R) :
theorem
prime_spectrum.gc
(R : Type u)
[comm_ring R] :
galois_connection (λ (I : ideal R), prime_spectrum.zero_locus ↑I) (λ (t : (set (prime_spectrum R))ᵒᵈ), prime_spectrum.vanishing_ideal t)
zero_locus and vanishing_ideal form a galois connection.
theorem
prime_spectrum.gc_set
(R : Type u)
[comm_ring R] :
galois_connection (λ (s : set R), prime_spectrum.zero_locus s) (λ (t : (set (prime_spectrum R))ᵒᵈ), ↑(prime_spectrum.vanishing_ideal t))
zero_locus and vanishing_ideal form a galois connection.
theorem
prime_spectrum.subset_zero_locus_iff_subset_vanishing_ideal
(R : Type u)
[comm_ring R]
(t : set (prime_spectrum R))
(s : set R) :
@[simp]
theorem
prime_spectrum.vanishing_ideal_zero_locus_eq_radical
{R : Type u}
[comm_ring R]
(I : ideal R) :
@[simp]
theorem
prime_spectrum.subset_zero_locus_vanishing_ideal
{R : Type u}
[comm_ring R]
(t : set (prime_spectrum R)) :
theorem
prime_spectrum.zero_locus_anti_mono_ideal
{R : Type u}
[comm_ring R]
{s t : ideal R}
(h : s ≤ t) :
theorem
prime_spectrum.vanishing_ideal_anti_mono
{R : Type u}
[comm_ring R]
{s t : set (prime_spectrum R)}
(h : s ⊆ t) :
theorem
prime_spectrum.zero_locus_subset_zero_locus_iff
{R : Type u}
[comm_ring R]
(I J : ideal R) :
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
@[simp]
@[simp]
@[simp]
theorem
prime_spectrum.zero_locus_empty_of_one_mem
{R : Type u}
[comm_ring R]
{s : set R}
(h : 1 ∈ s) :
@[simp]
@[simp]
theorem
prime_spectrum.vanishing_ideal_eq_top_iff
{R : Type u}
[comm_ring R]
{s : set (prime_spectrum R)} :
theorem
prime_spectrum.vanishing_ideal_union
{R : Type u}
[comm_ring R]
(t t' : set (prime_spectrum R)) :
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)
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)
@[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}
theorem
prime_spectrum.sup_vanishing_ideal_le
{R : Type u}
[comm_ring R]
(t t' : set (prime_spectrum R)) :
theorem
prime_spectrum.mem_compl_zero_locus_iff_not_mem
{R : Type u}
[comm_ring R]
{f : R}
{I : prime_spectrum R} :
@[protected, instance]
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
theorem
prime_spectrum.is_closed_iff_zero_locus
{R : Type u}
[comm_ring R]
(Z : set (prime_spectrum R)) :
theorem
prime_spectrum.is_closed_iff_zero_locus_ideal
{R : Type u}
[comm_ring R]
(Z : set (prime_spectrum R)) :
theorem
prime_spectrum.is_closed_iff_zero_locus_radical_ideal
{R : Type u}
[comm_ring R]
(Z : set (prime_spectrum R)) :
is_closed Z ↔ ∃ (I : ideal R), I.is_radical ∧ Z = prime_spectrum.zero_locus ↑I
theorem
prime_spectrum.is_closed_singleton_iff_is_maximal
{R : Type u}
[comm_ring R]
(x : prime_spectrum R) :
is_closed {x} ↔ x.as_ideal.is_maximal
theorem
prime_spectrum.zero_locus_vanishing_ideal_eq_closure
{R : Type u}
[comm_ring R]
(t : set (prime_spectrum R)) :
theorem
prime_spectrum.vanishing_ideal_closure
{R : Type u}
[comm_ring R]
(t : set (prime_spectrum R)) :
theorem
prime_spectrum.closure_singleton
{R : Type u}
[comm_ring R]
(x : prime_spectrum R) :
closure {x} = prime_spectrum.zero_locus ↑(x.as_ideal)
theorem
prime_spectrum.is_radical_vanishing_ideal
{R : Type u}
[comm_ring R]
(s : set (prime_spectrum R)) :
theorem
prime_spectrum.vanishing_ideal_anti_mono_iff
{R : Type u}
[comm_ring R]
{s t : set (prime_spectrum R)}
(ht : is_closed t) :
theorem
prime_spectrum.vanishing_ideal_strict_anti_mono_iff
{R : Type u}
[comm_ring R]
{s t : set (prime_spectrum R)}
(hs : is_closed s)
(ht : is_closed t) :
The antitone order embedding of closed subsets of Spec R into ideals of R.
Equations
theorem
prime_spectrum.t1_space_iff_is_field
{R : Type u}
[comm_ring R]
[is_domain R] :
t1_space (prime_spectrum R) ↔ is_field R
theorem
prime_spectrum.is_irreducible_zero_locus_iff_of_radical
{R : Type u}
[comm_ring R]
(I : ideal R)
(hI : I.is_radical) :
theorem
prime_spectrum.is_irreducible_iff_vanishing_ideal_is_prime
{R : Type u}
[comm_ring R]
{s : set (prime_spectrum R)} :
@[protected, instance]
@[protected, instance]
theorem
prime_spectrum.preimage_comap_zero_locus_aux
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(s : set R) :
(λ (y : prime_spectrum S), {as_ideal := ideal.comap f y.as_ideal, is_prime := _}) ⁻¹' prime_spectrum.zero_locus s = prime_spectrum.zero_locus (⇑f '' s)
The function between prime spectra of commutative rings induced by a ring homomorphism. This function is continuous.
Equations
- prime_spectrum.comap f = {to_fun := λ (y : prime_spectrum S), {as_ideal := ideal.comap f y.as_ideal, is_prime := _}, continuous_to_fun := _}
@[simp]
theorem
prime_spectrum.comap_as_ideal
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(y : prime_spectrum S) :
(⇑(prime_spectrum.comap f) y).as_ideal = ideal.comap f y.as_ideal
@[simp]
@[simp]
theorem
prime_spectrum.comap_comp
{R : Type u}
{S : Type v}
[comm_ring R]
[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).comp (prime_spectrum.comap g)
theorem
prime_spectrum.comap_comp_apply
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
{S' : Type u_1}
[comm_ring S']
(f : R →+* S)
(g : S →+* S')
(x : prime_spectrum S') :
⇑(prime_spectrum.comap (g.comp f)) x = ⇑(prime_spectrum.comap f) (⇑(prime_spectrum.comap g) x)
theorem
prime_spectrum.comap_injective_of_surjective
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f) :
theorem
prime_spectrum.comap_singleton_is_closed_of_surjective
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f)
(x : prime_spectrum S)
(hx : is_closed {x}) :
is_closed {⇑(prime_spectrum.comap f) x}
theorem
prime_spectrum.comap_singleton_is_closed_of_is_integral
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : f.is_integral)
(x : prime_spectrum S)
(hx : is_closed {x}) :
is_closed {⇑(prime_spectrum.comap f) x}
theorem
prime_spectrum.localization_comap_inducing
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
[algebra R S]
(M : submonoid R)
[is_localization M S] :
inducing ⇑(prime_spectrum.comap (algebra_map R S))
theorem
prime_spectrum.localization_comap_injective
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
[algebra R S]
(M : submonoid R)
[is_localization M S] :
theorem
prime_spectrum.localization_comap_embedding
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
[algebra R S]
(M : submonoid R)
[is_localization M S] :
theorem
prime_spectrum.localization_comap_range
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
[algebra R S]
(M : submonoid R)
[is_localization M S] :
set.range ⇑(prime_spectrum.comap (algebra_map R S)) = {p : prime_spectrum R | disjoint ↑M ↑(p.as_ideal)}
The comap of a surjective ring homomorphism is a closed embedding between the prime spectra.
theorem
prime_spectrum.comap_inducing_of_surjective
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f) :
theorem
prime_spectrum.image_comap_zero_locus_eq_zero_locus_comap
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f)
(I : ideal S) :
theorem
prime_spectrum.range_comap_of_surjective
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f) :
theorem
prime_spectrum.is_closed_range_comap_of_surjective
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f) :
theorem
prime_spectrum.closed_embedding_comap_of_surjective
{R : Type u}
(S : Type v)
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f) :
basic_open r is the open subset containing all prime ideals not containing r.
Equations
- prime_spectrum.basic_open r = {carrier := {x : prime_spectrum R | r ∉ x.as_ideal}, is_open' := _}
@[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
@[simp]
@[simp]
@[simp]
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
@[simp]
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)))
@[simp]
theorem
prime_spectrum.localization_away_comap_range
{R : Type u}
[comm_ring R]
(S : Type v)
[comm_ring S]
[algebra R S]
(r : R)
[is_localization.away r S] :
theorem
prime_spectrum.localization_away_open_embedding
{R : Type u}
[comm_ring R]
(S : Type v)
[comm_ring S]
[algebra R S]
(r : R)
[is_localization.away r S] :
@[protected, instance]
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}.
@[protected, instance]
@[simp]
@[simp]
def
prime_spectrum.nhds_order_embedding
{R : Type u}
[comm_ring R] :
prime_spectrum R ↪o filter (prime_spectrum R)
nhds as an order embedding.
Equations
- prime_spectrum.nhds_order_embedding = order_embedding.of_map_le_iff nhds prime_spectrum.nhds_order_embedding._proof_1
@[simp]
theorem
prime_spectrum.nhds_order_embedding_apply
{R : Type u}
[comm_ring R]
(a : prime_spectrum R) :
@[protected, instance]
@[protected, instance]
Equations
- prime_spectrum.unique = {to_inhabited := {default := ⊥}, uniq := _}
noncomputable
def
prime_spectrum.localization_map_of_specializes
{R : Type u}
[comm_ring R]
{x y : prime_spectrum R}
(h : x ⤳ y) :
If x specializes to y, then there is a natural map from the localization of y to the
localization of x.
The closed point in the prime spectrum of a local ring.
Equations
- local_ring.closed_point R = {as_ideal := local_ring.maximal_ideal R _inst_3, is_prime := _}
theorem
local_ring.is_local_ring_hom_iff_comap_closed_point
{R : Type u}
[comm_ring R]
[local_ring R]
{S : Type v}
[comm_ring S]
[local_ring S]
(f : R →+* S) :
@[simp]
theorem
local_ring.comap_closed_point
{R : Type u}
[comm_ring R]
[local_ring R]
{S : Type v}
[comm_ring S]
[local_ring S]
(f : R →+* S)
[is_local_ring_hom f] :
theorem
local_ring.specializes_closed_point
{R : Type u}
[comm_ring R]
[local_ring R]
(x : prime_spectrum R) :
theorem
local_ring.closed_point_mem_iff
{R : Type u}
[comm_ring R]
[local_ring R]
(U : topological_space.opens (prime_spectrum R)) :
local_ring.closed_point R ∈ U ↔ U = ⊤
@[simp]
theorem
prime_spectrum.comap_residue
{R : Type u}
[comm_ring R]
[local_ring R]
(x : prime_spectrum (local_ring.residue_field R)) :