Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

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 #

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.

Then we establish that Proj ๐’œ is a LocallyRingedSpace:

References #

def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.IsFraction {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] {U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)} (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.

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.

Equations
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) (a b : (x : โ†ฅ(Opposite.unop U)) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal) (ha : (isLocallyFraction ๐’œ).pred a) (hb : (isLocallyFraction ๐’œ).pred b) :
(isLocallyFraction ๐’œ).pred (a + b)
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) (a : (x : โ†ฅ(Opposite.unop U)) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal) (ha : (isLocallyFraction ๐’œ).pred a) :
(isLocallyFraction ๐’œ).pred (-a)
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) (a b : (x : โ†ฅ(Opposite.unop U)) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal) (ha : (isLocallyFraction ๐’œ).pred a) (hb : (isLocallyFraction ๐’œ).pred b) :
(isLocallyFraction ๐’œ).pred (a * b)

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 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
@[simp]
theorem AlgebraicGeometry.Proj.res_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {U V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (i : V โŸถ U) (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj V)) (x : โ†ฅ(Opposite.unop U)) :
theorem AlgebraicGeometry.Proj.ext {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj V)) (h : โ†‘s = โ†‘t) :
s = t
@[simp]
theorem AlgebraicGeometry.Proj.add_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj V)) (x : โ†ฅ(Opposite.unop V)) :
โ†‘(s + t) x = โ†‘s x + โ†‘t x
@[simp]
theorem AlgebraicGeometry.Proj.mul_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj V)) (x : โ†ฅ(Opposite.unop V)) :
โ†‘(s * t) x = โ†‘s x * โ†‘t x
@[simp]
theorem AlgebraicGeometry.Proj.sub_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj V)) (x : โ†ฅ(Opposite.unop V)) :
โ†‘(s - t) x = โ†‘s x - โ†‘t x
@[simp]
theorem AlgebraicGeometry.Proj.pow_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj V)) (x : โ†ฅ(Opposite.unop V)) (n : โ„•) :
โ†‘(s ^ n) x = โ†‘s x ^ n
@[simp]
theorem AlgebraicGeometry.Proj.zero_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (x : โ†ฅ(Opposite.unop V)) :
โ†‘0 x = 0
@[simp]
theorem AlgebraicGeometry.Proj.one_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (x : โ†ฅ(Opposite.unop V)) :
โ†‘1 x = 1
def AlgebraicGeometry.Proj.toSheafedSpace {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

Proj of a graded ring as a SheafedSpace

Equations

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.
@[simp]
theorem AlgebraicGeometry.germ_comp_stalkToFiberRingHom {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) :
@[simp]
theorem AlgebraicGeometry.stalkToFiberRingHom_germ {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj (Opposite.op U))) :
theorem AlgebraicGeometry.mem_basicOpen_den {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (f : HomogeneousLocalization.NumDenSameDeg ๐’œ x.asHomogeneousIdeal.toIdeal.primeCompl) :

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.
def AlgebraicGeometry.homogeneousLocalizationToStalk {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (y : HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal) :

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.
@[simp]
theorem AlgebraicGeometry.Proj.stalkIso'_germ {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj (Opposite.op U))) :
(stalkIso' ๐’œ x) ((CategoryTheory.ConcreteCategory.hom ((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.germ U x hx)) s) = โ†‘s โŸจx, hxโŸฉ
def AlgebraicGeometry.Proj.toLocallyRingedSpace {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :

Proj of a graded ring as a LocallyRingedSpace

Equations