The structure sheaf on projective_spectrum ๐
. #
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 structure sheaf (valued in Type
, not yet CommRing
) is the subsheaf consisting of
functions satisfying isLocallyFraction
.
Instances For
The structure presheaf, valued in CommRing
, constructed by dressing up the Type
valued
structure presheaf.
Instances For
Some glue, verifying that that structure presheaf valued in CommRing
agrees with the Type
valued structure presheaf.
Instances For
The structure sheaf on Proj
๐, valued in CommRing
.
Instances For
Proj
of a graded ring as a SheafedSpace
Instances For
Proj
of a graded ring as a LocallyRingedSpace