The structure sheaf on ProjectiveSpectrum ๐
. #
In Mathlib.AlgebraicGeometry.Topology
, we have given a topology on ProjectiveSpectrum ๐
; in
this file we will construct a sheaf on ProjectiveSpectrum ๐
.
Notation #
R
is a commutative semiring;A
is a commutative ring and anR
-algebra;๐ : โ โ Submodule R A
is the grading ofA
;U
is opposite object of some open subset ofProjectiveSpectrum.top
.
Main definitions and results #
We define the structure sheaf as the subsheaf of all dependent function
f : ฮ x : U, HomogeneousLocalization ๐ x
such that f
is locally expressible as ratio of two
elements of the same grading, i.e. โ y โ U, โ (V โ U) (i : โ) (a b โ ๐ i), โ z โ V, f z = a / b
.
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction
: the predicate that a dependent function is locally expressible as a ratio of two elements of the same grading.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.sectionsSubring
: the dependent functions satisfying the above local property forms a subring of all dependent functionsฮ x : U, HomogeneousLocalization ๐ x
.AlgebraicGeometry.Proj.StructureSheaf
: the sheaf withU โฆ sectionsSubring U
and natural restriction map.
Then we establish that Proj ๐
is a LocallyRingedSpace
:
AlgebraicGeometry.Proj.stalkIso'
: for anyx : ProjectiveSpectrum ๐
, the stalk ofProj.StructureSheaf
atx
is isomorphic toHomogeneousLocalization ๐ x
.AlgebraicGeometry.Proj.toLocallyRingedSpace
:Proj
as a locally ringed space.
References #
- [Robin Hartshorne, Algebraic Geometry][Har77]
The predicate saying that a dependent function on an open U
is realised as a fixed fraction
r / s
of same grading in each of the stalks (which are localizations at various prime ideals).
Equations
- One or more equations did not get rendered due to their size.
The predicate IsFraction
is "prelocal", in the sense that if it holds on U
it holds on any open
subset V
of U
.
Equations
- One or more equations did not get rendered due to their size.
We will define the structure sheaf as the subsheaf of all dependent functions in
ฮ x : U, HomogeneousLocalization ๐ x
consisting of those functions which can locally be expressed
as a ratio of A
of same grading.
The functions satisfying isLocallyFraction
form a subring of all dependent functions
ฮ x : U, HomogeneousLocalization ๐ x
.
Equations
- One or more equations did not get rendered due to their size.
The structure sheaf (valued in Type
, not yet CommRing
) is the subsheaf consisting of
functions satisfying isLocallyFraction
.
The structure presheaf, valued in CommRing
, constructed by dressing up the Type
valued
structure presheaf.
Equations
- One or more equations did not get rendered due to their size.
Some glue, verifying that the structure presheaf valued in CommRing
agrees with the Type
valued structure presheaf.
Equations
- One or more equations did not get rendered due to their size.
The structure sheaf on Proj
๐, valued in CommRing
.
Equations
- AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐ = { val := AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing ๐, cond := โฏ }
Proj
of a graded ring as a SheafedSpace
Equations
- AlgebraicGeometry.Proj.toSheafedSpace ๐ = { carrier := TopCat.of (ProjectiveSpectrum ๐), presheaf := (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐).val, IsSheaf := โฏ }
The ring homomorphism that takes a section of the structure sheaf of Proj
on the open set U
,
implemented as a subtype of dependent functions to localizations at homogeneous prime ideals, and
evaluates the section on the point corresponding to a given homogeneous prime ideal.
Equations
- One or more equations did not get rendered due to their size.
The ring homomorphism from the stalk of the structure sheaf of Proj
at a point corresponding
to a homogeneous prime ideal x
to the homogeneous localization at x
,
formed by gluing the openToLocalization
maps.
Equations
- One or more equations did not get rendered due to their size.
Given a point x
corresponding to a homogeneous prime ideal, there is a (dependent) function
such that, for any f
in the homogeneous localization at x
, it returns the obvious section in the
basic open set D(f.den)
.
Equations
- One or more equations did not get rendered due to their size.
Given any point x
and f
in the homogeneous localization at x
, there is an element in the
stalk at x
obtained by sectionInBasicOpen
. This is the inverse of stalkToFiberRingHom
.
Equations
- One or more equations did not get rendered due to their size.
Using homogeneousLocalizationToStalk
, we construct a ring isomorphism between stalk at x
and homogeneous localization at x
for any point x
in Proj
.
Equations
- One or more equations did not get rendered due to their size.
Proj
of a graded ring as a LocallyRingedSpace
Equations
- AlgebraicGeometry.Proj.toLocallyRingedSpace ๐ = { toSheafedSpace := AlgebraicGeometry.Proj.toSheafedSpace ๐, isLocalRing := โฏ }