# Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

# 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 an R-algebra;
• 𝒜 : ℕ → Submodule R A is the grading of A;
• U is opposite object of some open subset of ProjectiveSpectrum.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 with U ↦ sectionsSubring U and natural restriction map.

Then we establish that Proj 𝒜 is a LocallyRingedSpace:

• AlgebraicGeometry.Proj.stalkIso': for any x : ProjectiveSpectrum 𝒜, the stalk of Proj.StructureSheaf at x is isomorphic to HomogeneousLocalization 𝒜 x.
• AlgebraicGeometry.Proj.toLocallyRingedSpace: Proj as a locally ringed space.
• [Robin Hartshorne, Algebraic Geometry][Har77]