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, but that sheaf is not constructed in this file. It should be contributed to mathlib in future work.)
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).
The prime spectrum of a commutative ring R
is the type of all prime ideal of R.
It is naturally endowed with a topology (the Zariski topology), and a sheaf of commutative rings (not yet in mathlib). 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.
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, _⟩
The prime spectrum of a commutative ring is a compact topological space.