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 #

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 #

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

      The structure sheaf on Proj ๐’œ, valued in CommRing.

      Instances For
        @[simp]
        theorem AlgebraicGeometry.res_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (V : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (i : V โŸถ U) (s : โ†‘((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj (Opposite.op U))) (x : { x // x โˆˆ V }) :
        โ†‘(โ†‘((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.map i.op) s) x = โ†‘s ((fun x => { val := โ†‘x, property := (_ : โ†‘x โˆˆ โ†‘U) }) x)

        Proj of a graded ring as a SheafedSpace

        Instances For
          @[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 : โ†‘((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj (Opposite.op U))) :
          โ†‘(AlgebraicGeometry.stalkToFiberRingHom ๐’œ x) (โ†‘(TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ)) { val := x, property := hx }) s) = โ†‘s { val := x, property := hx }
          @[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 : { x // x โˆˆ U }) (s : โ†‘((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.obj (Opposite.op U))) :

          Proj of a graded ring as a LocallyRingedSpace

          Instances For