The structure sheaf on
projective_spectrum 𝒜. #
Ris a commutative semiring;
Ais a commutative ring and an
𝒜 : ℕ → Submodule R Ais the grading of
Uis opposite object of some open subset of
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 with
U ↦ sectionsSubring Uand natural restriction map.
Then we establish that
Proj 𝒜 is a
AlgebraicGeometry.Proj.stalkIso': for any
x : ProjectiveSpectrum 𝒜, the stalk of
xis isomorphic to
HomogeneousLocalization 𝒜 x.
Projas a locally ringed space.
- [Robin Hartshorne, Algebraic Geometry][Har77]
The structure sheaf (valued in
Type, not yet
CommRing) is the subsheaf consisting of
The structure presheaf, valued in
CommRing, constructed by dressing up the
Some glue, verifying that that structure presheaf valued in
CommRing agrees with the
valued structure presheaf.