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 #

source
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zeroMem' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
TopCat.PrelocalPredicate.pred (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate 0
source
theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.oneMem' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
TopCat.PrelocalPredicate.pred (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate 1
source
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
TopCat.Sheaf (Type u_2) (ProjectiveSpectrum.top ๐’œ)

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

Instances For
    source
    instance AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.commRingStructureSheafInTypeObj {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
    CommRing ((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType ๐’œ).val.obj U)
    source
    @[simp]
    theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_map_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
    โˆ€ {X Y : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (i : X โŸถ Y) (a : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType ๐’œ).val.obj X), โ†‘((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing ๐’œ).map i) a = (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType ๐’œ).val.map i a
    source
    @[simp]
    theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
    (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing ๐’œ).obj U = CommRingCat.of ((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType ๐’œ).val.obj U)
    source
    def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
    TopCat.Presheaf CommRingCat (ProjectiveSpectrum.top ๐’œ)

    The structure presheaf, valued in CommRing, constructed by dressing up the Type valued structure presheaf.

    Instances For
      source
      def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafCompForget {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
      CategoryTheory.Functor.comp (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing ๐’œ) (CategoryTheory.forget CommRingCat) โ‰… (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType ๐’œ).val

      Some glue, verifying that that structure presheaf valued in CommRing agrees with the Type valued structure presheaf.

      Instances For
        source
        def AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
        TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top ๐’œ)

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

        Instances For
          source
          @[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)
          source
          def AlgebraicGeometry.Proj.toSheafedSpace {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
          AlgebraicGeometry.SheafedSpace CommRingCat

          Proj of a graded ring as a SheafedSpace

          Instances For
            source
            @[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 : { x // x โˆˆ U }) :
            CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ)) x) (AlgebraicGeometry.stalkToFiberRingHom ๐’œ โ†‘x) = AlgebraicGeometry.openToLocalization ๐’œ U โ†‘x (_ : โ†‘x โˆˆ U)
            source
            @[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 }
            source
            @[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))) :
            โ†‘(AlgebraicGeometry.stalkToFiberRingHom ๐’œ โ†‘x) (โ†‘(TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ)) x) s) = โ†‘s x
            source
            def AlgebraicGeometry.Proj.toLocallyRingedSpace {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] :
            AlgebraicGeometry.LocallyRingedSpace

            Proj of a graded ring as a LocallyRingedSpace

            Instances For