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 ringR
, i.e., the set of all prime ideals ofR
.zeroLocus s
: The zero locus of a subsets
ofR
is the subset ofPrimeSpectrum R
consisting of all prime ideals that contains
.vanishingIdeal t
: The vanishing ideal of a subsett
ofPrimeSpectrum 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).
- asIdeal : Ideal R
- IsPrime : Ideal.IsPrime s.asIdeal
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.
The map from the direct sum of prime spectra to the prime spectrum of a direct product.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- PrimeSpectrum.zeroLocus s = {x | s ⊆ ↑x.asIdeal}
Instances For
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
.
Equations
- PrimeSpectrum.vanishingIdeal t = ⨅ (x : PrimeSpectrum R) (_ : x ∈ t), x.asIdeal
Instances For
zeroLocus
and vanishingIdeal
form a galois connection.
zeroLocus
and vanishingIdeal
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
- One or more equations did not get rendered due to their size.
The antitone order embedding of closed subsets of Spec R
into ideals of R
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The prime spectrum of a commutative ring is a compact topological space.
The function between prime spectra of commutative rings induced by a ring homomorphism. This function is continuous.
Equations
- PrimeSpectrum.comap f = ContinuousMap.mk fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }
Instances For
The comap of a surjective ring homomorphism is a closed embedding between the prime spectra.
basicOpen r
is the open subset containing all prime ideals not containing r
.
Equations
- PrimeSpectrum.basicOpen r = { carrier := {x | ¬r ∈ x.asIdeal}, is_open' := (_ : ∃ y, PrimeSpectrum.zeroLocus y = {x | ¬r ∈ x.asIdeal}ᶜ) }
Instances For
The specialization order #
We endow PrimeSpectrum R
with a partial order, where x ≤ y
if and only if y ∈ closure {x}
.
Equations
- PrimeSpectrum.instPartialOrderPrimeSpectrum = PartialOrder.lift PrimeSpectrum.asIdeal (_ : ∀ (x y : PrimeSpectrum R), x.asIdeal = y.asIdeal → x = y)
nhds
as an order embedding.
Equations
- PrimeSpectrum.nhdsOrderEmbedding = OrderEmbedding.ofMapLEIff nhds (_ : ∀ (a b : PrimeSpectrum R), a ⤳ b ↔ a ≤ b)
Instances For
Equations
- PrimeSpectrum.instOrderBotPrimeSpectrumToLEToPreorderInstPartialOrderPrimeSpectrum = OrderBot.mk (_ : ∀ (I : PrimeSpectrum R), ⊥ ≤ I.asIdeal)
Equations
- PrimeSpectrum.instUniquePrimeSpectrumToCommRingToEuclideanDomain = { toInhabited := { default := ⊥ }, uniq := (_ : ∀ (x : PrimeSpectrum R), x = default) }
If x
specializes to y
, then there is a natural map from the localization of y
to the
localization of x
.
Equations
- PrimeSpectrum.localizationMapOfSpecializes h = IsLocalization.lift (_ : ∀ (y : { x // x ∈ Ideal.primeCompl y.asIdeal }), IsUnit (↑(algebraMap R (Localization.AtPrime x.asIdeal)) ↑y))
Instances For
The closed point in the prime spectrum of a local ring.
Equations
- LocalRing.closedPoint R = { asIdeal := LocalRing.maximalIdeal R, IsPrime := (_ : Ideal.IsPrime (LocalRing.maximalIdeal R)) }