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 ringR
, i.e., the set of all prime ideals ofR
.zero_locus s
: The zero locus of a subsets
ofR
is the subset ofprime_spectrum R
consisting of all prime ideals that contains
.vanishing_ideal t
: The vanishing ideal of a subsett
ofprime_spectrum R
is 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).
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}
A method to view a point in the prime spectrum of a commutative ring as an ideal of that ring.
The prime spectrum of the zero ring is empty.
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)}
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
zero_locus
and vanishing_ideal
form a galois connection.
zero_locus
and vanishing_ideal
form a galois connection.
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
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, _⟩
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}, _⟩
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
Equations
- prime_spectrum.partial_order = subtype.partial_order (λ (I : ideal R), I.is_prime)