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
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 ๐’œ (HomogeneousIdeal.toIdeal (โ†‘x).asHomogeneousIdeal)) :
Prop

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

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

      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
        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 ๐’œ))แต’แต–) :
        (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred 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 ๐’œ))แต’แต–) :
        (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred 1
        source
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.addMem' {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 : โ†ฅU.unop) โ†’ HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal (โ†‘x).asHomogeneousIdeal)) (b : (x : โ†ฅU.unop) โ†’ HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal (โ†‘x).asHomogeneousIdeal)) (ha : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred a) (hb : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred b) :
        (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred (a + b)
        source
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.negMem' {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 : โ†ฅU.unop) โ†’ HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal (โ†‘x).asHomogeneousIdeal)) (ha : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred a) :
        (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred (-a)
        source
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mulMem' {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 : โ†ฅU.unop) โ†’ HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal (โ†‘x).asHomogeneousIdeal)) (b : (x : โ†ฅU.unop) โ†’ HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal (โ†‘x).asHomogeneousIdeal)) (ha : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred a) (hb : (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred b) :
        (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ๐’œ).toPrelocalPredicate.pred (a * b)
        source
        def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.sectionsSubring {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {๐’œ : โ„• โ†’ Submodule R A} [GradedAlgebra ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
        Subring ((x : โ†ฅU.unop) โ†’ HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal (โ†‘x).asHomogeneousIdeal))

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

          Equations
          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.toPrefunctor.obj U)
            Equations
            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 ๐’œ).toPrefunctor.obj U = CommRingCat.of ((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType ๐’œ).val.toPrefunctor.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.toPrefunctor.obj X), ((AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing ๐’œ).toPrefunctor.map i) a = (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType ๐’œ).val.toPrefunctor.map i a
            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.

            Equations
            • One or more equations did not get rendered due to their size.
            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.

              Equations
              • One or more equations did not get rendered due to their size.
              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.

                Equations
                • One or more equations did not get rendered due to their size.
                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.toPrefunctor.obj (Opposite.op U))) (x : โ†ฅV) :
                  โ†‘(((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.toPrefunctor.map i.op) s) x = โ†‘s ((fun (x : โ†ฅV) => { 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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def AlgebraicGeometry.openToLocalization {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) :
                    (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.toPrefunctor.obj (Opposite.op U) โŸถ CommRingCat.of (HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal))

                    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
                      source
                      def AlgebraicGeometry.stalkToFiberRingHom {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                      TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ)) x โŸถ CommRingCat.of (HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal))

                      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
                        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 : โ†ฅ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.toPrefunctor.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 : โ†ฅU) (s : โ†‘((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.toPrefunctor.obj (Opposite.op U))) :
                        (AlgebraicGeometry.stalkToFiberRingHom ๐’œ โ†‘x) ((TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ)) x) s) = โ†‘s x
                        source
                        theorem AlgebraicGeometry.HomogeneousLocalization.mem_basicOpen {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (f : HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) :
                        x โˆˆ ProjectiveSpectrum.basicOpen ๐’œ (HomogeneousLocalization.den f)
                        source
                        def AlgebraicGeometry.sectionInBasicOpen {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (f : HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)) :
                        โ†‘((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ).val.toPrefunctor.obj (Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ (HomogeneousLocalization.den f))))

                        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
                          source
                          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 ๐’œ)) :
                          HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal) โ†’ โ†‘(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ)) 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
                            source
                            def AlgebraicGeometry.Proj.stalkIso' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (๐’œ : โ„• โ†’ Submodule R A) [GradedAlgebra ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                            โ†‘(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ๐’œ)) x) โ‰ƒ+* โ†‘(CommRingCat.of (HomogeneousLocalization.AtPrime ๐’œ (HomogeneousIdeal.toIdeal x.asHomogeneousIdeal)))

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For