Projective spectrum of a graded ring #
The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal. It is naturally endowed with a topology: the Zariski topology.
Notation #
R
is a commutative semiring;A
is a commutative ring and anR
-algebra;π : β β submodule R A
is the grading ofA
;
Main definitions #
projective_spectrum π
: The projective spectrum of a graded ringA
, or equivalently, the set of all homogeneous ideals ofA
that is both prime and relevant i.e. not containing irrelevant ideal. Henceforth, we call elements of projective spectrum relevant homogeneous prime ideals.projective_spectrum.zero_locus π s
: The zero locus of a subsets
ofA
is the subset ofprojective_spectrum π
consisting of all relevant homogeneous prime ideals that contains
.projective_spectrum.vanishing_ideal t
: The vanishing ideal of a subsett
ofprojective_spectrum π
is the intersection of points int
(viewed as relevant homogeneous prime ideals).projective_spectrum.Top
: the topological space ofprojective_spectrum π
endowed with the Zariski topology.
- as_homogeneous_ideal : homogeneous_ideal π
- is_prime : self.as_homogeneous_ideal.to_ideal.is_prime
- not_irrelevant_le : Β¬homogeneous_ideal.irrelevant π β€ self.as_homogeneous_ideal
The projective spectrum of a graded commutative ring is the subtype of all homogenous ideals that are prime and do not contain the irrelevant ideal.
Instances for projective_spectrum
- projective_spectrum.has_sizeof_inst
- projective_spectrum.zariski_topology
- projective_spectrum.partial_order
The zero locus of a set s
of elements of a commutative ring A
is the set of all relevant
homogeneous prime ideals of the ring that contain the set s
.
An element f
of A
can be thought of as a dependent function on the projective spectrum of π
.
At a point x
(a homogeneous prime ideal) the function (i.e., element) f
takes values in the
quotient ring A
modulo the prime ideal x
. In this manner, zero_locus s
is exactly the subset
of projective_spectrum π
where all "functions" in s
vanish simultaneously.
Equations
- projective_spectrum.zero_locus π s = {x : projective_spectrum π | s β β(x.as_homogeneous_ideal)}
The vanishing ideal of a set t
of points of the projective spectrum of a commutative ring R
is the intersection of all the relevant homogeneous prime ideals in the set t
.
An element f
of A
can be thought of as a dependent function on the projective spectrum of π
.
At a point x
(a homogeneous prime ideal) the function (i.e., element) f
takes values in the
quotient ring A
modulo the prime ideal x
. In this manner, vanishing_ideal t
is exactly the
ideal of A
consisting of all "functions" that vanish on all of t
.
Equations
- projective_spectrum.vanishing_ideal t = β¨ (x : projective_spectrum π) (h : x β t), x.as_homogeneous_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
The underlying topology of Proj
is the projective spectrum of graded ring A
.
Equations
- projective_spectrum.Top π = Top.of (projective_spectrum π)
basic_open r
is the open subset containing all prime ideals not containing r
.
Equations
- projective_spectrum.basic_open π r = {carrier := {x : projective_spectrum π | r β x.as_homogeneous_ideal}, is_open' := _}
The specialization order #
We endow projective_spectrum π
with a partial order,
where x β€ y
if and only if y β closure {x}
.