# 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.

## References #

• [Robin Hartshorne, Algebraic Geometry][Har77]
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.IsFraction {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] {U : } (f : (x : โฅU) โ HomogeneousLocalization.AtPrime ๐ (โx).asHomogeneousIdeal.toIdeal) :

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.
Instances For
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isFractionPrelocal {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
TopCat.PrelocalPredicate fun (x : โ()) => HomogeneousLocalization.AtPrime ๐ x.asHomogeneousIdeal.toIdeal

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.
Instances For
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
TopCat.LocalPredicate fun (x : โ()) => HomogeneousLocalization.AtPrime ๐ x.asHomogeneousIdeal.toIdeal

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.

Equations
Instances For
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (U : ()แตแต) :
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (U : ()แตแต) :
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (U : ()แตแต) (a : (x : โฅU.unop) โ HomogeneousLocalization.AtPrime ๐ (โx).asHomogeneousIdeal.toIdeal) (b : (x : โฅU.unop) โ HomogeneousLocalization.AtPrime ๐ (โx).asHomogeneousIdeal.toIdeal) (ha : ) (hb : ) :
(a + b)
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (U : ()แตแต) (a : (x : โฅU.unop) โ HomogeneousLocalization.AtPrime ๐ (โx).asHomogeneousIdeal.toIdeal) (ha : ) :
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (U : ()แตแต) (a : (x : โฅU.unop) โ HomogeneousLocalization.AtPrime ๐ (โx).asHomogeneousIdeal.toIdeal) (b : (x : โฅU.unop) โ HomogeneousLocalization.AtPrime ๐ (โx).asHomogeneousIdeal.toIdeal) (ha : ) (hb : ) :
(a * b)
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.sectionsSubring {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {๐ : โ โ } [GradedAlgebra ๐] (U : ()แตแต) :
Subring ((x : โฅU.unop) โ HomogeneousLocalization.AtPrime ๐ (โx).asHomogeneousIdeal.toIdeal)

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.
Instances For
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :

The structure sheaf (valued in Type, not yet CommRing) is the subsheaf consisting of functions satisfying isLocallyFraction.

Equations
Instances For
instance AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.commRingStructureSheafInTypeObj {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ()แตแต) :
Equations
@[simp]
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_map_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :
โ {X Y : ()แตแต} (i : X โถ Y) (a : ),
@[simp]
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ()แตแต) :
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :

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.
Instances For
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafCompForget {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :

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.
Instances For
def AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :

The structure sheaf on Proj ๐, valued in CommRing.

Equations
• = { val := , cond := โฏ }
Instances For
@[simp]
theorem AlgebraicGeometry.Proj.res_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {U : ()แตแต} {V : ()แตแต} (i : V โถ U) (s : โ(.obj V)) (x : โฅU.unop) :
โ((.map i) s) x = โs ((fun (x : โฅU.unop) => โจโx, โฏโฉ) x)
theorem AlgebraicGeometry.Proj.ext {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {V : ()แตแต} (s : โ(.obj V)) (t : โ(.obj V)) (h : โs = โt) :
s = t
@[simp]
theorem AlgebraicGeometry.Proj.add_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {V : ()แตแต} (s : โ(.obj V)) (t : โ(.obj V)) (x : โฅV.unop) :
โ(s + t) x = โs x + โt x
@[simp]
theorem AlgebraicGeometry.Proj.mul_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {V : ()แตแต} (s : โ(.obj V)) (t : โ(.obj V)) (x : โฅV.unop) :
โ(s * t) x = โs x * โt x
@[simp]
theorem AlgebraicGeometry.Proj.sub_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {V : ()แตแต} (s : โ(.obj V)) (t : โ(.obj V)) (x : โฅV.unop) :
โ(s - t) x = โs x - โt x
@[simp]
theorem AlgebraicGeometry.Proj.pow_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {V : ()แตแต} (s : โ(.obj V)) (x : โฅV.unop) (n : โ) :
โ(s ^ n) x = โs x ^ n
@[simp]
theorem AlgebraicGeometry.Proj.zero_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {V : ()แตแต} (x : โฅV.unop) :
โ0 x = 0
@[simp]
theorem AlgebraicGeometry.Proj.one_apply {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] {V : ()แตแต} (x : โฅV.unop) :
โ1 x = 1
def AlgebraicGeometry.Proj.toSheafedSpace {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :

Proj of a graded ring as a SheafedSpace

Equations
• = { carrier := TopCat.of (), presheaf := , IsSheaf := โฏ }
Instances For
def AlgebraicGeometry.openToLocalization {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ) (x : โ()) (hx : x โ U) :
.obj { unop := U } โถ CommRingCat.of (HomogeneousLocalization.AtPrime ๐ x.asHomogeneousIdeal.toIdeal)

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.
Instances For
def AlgebraicGeometry.stalkToFiberRingHom {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) :
.presheaf.stalk x โถ CommRingCat.of (HomogeneousLocalization.AtPrime ๐ x.asHomogeneousIdeal.toIdeal)

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.
Instances For
@[simp]
theorem AlgebraicGeometry.germ_comp_stalkToFiberRingHom {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ) (x : โฅU) :
CategoryTheory.CategoryStruct.comp (.presheaf.germ x) () = AlgebraicGeometry.openToLocalization ๐ U โx โฏ
@[simp]
theorem AlgebraicGeometry.stalkToFiberRingHom_germ' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ) (x : โ()) (hx : x โ U) (s : โ(.obj { unop := U })) :
((.presheaf.germ โจx, hxโฉ) s) = โs โจx, hxโฉ
@[simp]
theorem AlgebraicGeometry.stalkToFiberRingHom_germ {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ) (x : โฅU) (s : โ(.obj { unop := U })) :
() ((.presheaf.germ x) s) = โs x
theorem AlgebraicGeometry.mem_basicOpen_den {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) (f : HomogeneousLocalization.NumDenSameDeg ๐ x.asHomogeneousIdeal.toIdeal.primeCompl) :
x โ ProjectiveSpectrum.basicOpen ๐ โf.den
def AlgebraicGeometry.sectionInBasicOpen {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) (f : HomogeneousLocalization.NumDenSameDeg ๐ x.asHomogeneousIdeal.toIdeal.primeCompl) :
โ(.obj { unop := ProjectiveSpectrum.basicOpen ๐ โf.den })

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.
Instances For
def AlgebraicGeometry.homogeneousLocalizationToStalk {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) (y : HomogeneousLocalization.AtPrime ๐ x.asHomogeneousIdeal.toIdeal) :
โ(.presheaf.stalk x)

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.
Instances For
theorem AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) (z : โ(.presheaf.stalk x)) :
= z
theorem AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) (z : HomogeneousLocalization.AtPrime ๐ x.asHomogeneousIdeal.toIdeal) :
= z
def AlgebraicGeometry.Proj.stalkIso' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) :
โ(.presheaf.stalk x) โ+* HomogeneousLocalization.AtPrime ๐ x.asHomogeneousIdeal.toIdeal

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.
Instances For
@[simp]
theorem AlgebraicGeometry.Proj.stalkIso'_germ' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ) (x : โ()) (hx : x โ U) (s : โ(.obj { unop := U })) :
() ((.presheaf.germ โจx, hxโฉ) s) = โs โจx, hxโฉ
@[simp]
theorem AlgebraicGeometry.Proj.stalkIso'_germ {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (U : ) (x : โฅU) (s : โ(.obj { unop := U })) :
(AlgebraicGeometry.Proj.stalkIso' ๐ โx) ((.presheaf.germ x) s) = โs x
@[simp]
theorem AlgebraicGeometry.Proj.stalkIso'_symm_mk {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] (x : โ()) (f : HomogeneousLocalization.NumDenSameDeg ๐ x.asHomogeneousIdeal.toIdeal.primeCompl) :
().symm = (.presheaf.germ โจx, โฏโฉ) ()
def AlgebraicGeometry.Proj.toLocallyRingedSpace {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (๐ : โ โ ) [GradedAlgebra ๐] :

Proj of a graded ring as a LocallyRingedSpace

Equations
• = let __src := ; { toSheafedSpace := __src, localRing := โฏ }
Instances For