Documentation

DerivedAlgGeo.AlgebraicGeometry.ProjectiveSpectrum.Modules.AssociatedSheaf

The sheaf associated to a graded module on Proj #

For an โ„•-graded ring A = โจ i, ๐’œ i and a compatibly graded A-module M = โจ i, ๐“œ i, this file constructs the sheaf usually denoted Mฬƒ on Proj ๐’œ. Its fiber at a homogeneous prime is the degree-zero homogeneous localization from AlgebraicGeometry.Proj.Modules.GradedLocalization, and its sections are the dependent functions which are locally represented by one homogeneous module fraction.

The construction deliberately mirrors Mathlib's ProjectiveSpectrum.StructureSheaf: the underlying topological space, restrictions, structure-sheaf scalars, and stalk evaluation maps are the existing Mathlib ones.

Local homogeneous module fractions #

source
@[reducible, inline]
abbrev AlgebraicGeometry.Proj.Fiber {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (x : ProjectiveSpectrum ๐’œ) :
Submodule (HomogeneousLocalization ๐’œ x.asHomogeneousIdeal.toIdeal.primeCompl) (LocalizedModule x.asHomogeneousIdeal.toIdeal.primeCompl M)

The degree-zero homogeneous localization of M at a point of Proj ๐’œ.

Equations
Instances For
    source
    def AlgebraicGeometry.Proj.IsFraction {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)} (f : (x : โ†ฅU) โ†’ โ†ฅ(Fiber ๐’œ ๐“œ โ†‘x)) :
    Prop

    A dependent module section is a single homogeneous fraction on an open set.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def AlgebraicGeometry.Proj.isFractionPrelocal {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] :
      TopCat.PrelocalPredicate fun (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) => โ†ฅ(Fiber ๐’œ ๐“œ x)

      The fixed-fraction predicate is preserved by restriction.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def AlgebraicGeometry.Proj.isLocallyFraction {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] :
        TopCat.LocalPredicate fun (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) => โ†ฅ(Fiber ๐’œ ๐“œ x)

        The local predicate defining Mฬƒ: locally, a section is one homogeneous fraction.

        Equations
        Instances For
          source
          theorem AlgebraicGeometry.Proj.Sections.zero_mem' {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] {๐’œ : โ„• โ†’ ฯƒA} {๐“œ : โ„• โ†’ ฯƒM} [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) :
          (isLocallyFraction ๐’œ ๐“œ).pred 0
          source
          theorem AlgebraicGeometry.Proj.Sections.add_mem' {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] {๐’œ : โ„• โ†’ ฯƒA} {๐“œ : โ„• โ†’ ฯƒM} [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (a b : (x : โ†ฅU) โ†’ โ†ฅ(Fiber ๐’œ ๐“œ โ†‘x)) (ha : (isLocallyFraction ๐’œ ๐“œ).pred a) (hb : (isLocallyFraction ๐’œ ๐“œ).pred b) :
          (isLocallyFraction ๐’œ ๐“œ).pred (a + b)
          source
          theorem AlgebraicGeometry.Proj.Sections.neg_mem' {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] {๐’œ : โ„• โ†’ ฯƒA} {๐“œ : โ„• โ†’ ฯƒM} [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (a : (x : โ†ฅU) โ†’ โ†ฅ(Fiber ๐’œ ๐“œ โ†‘x)) (ha : (isLocallyFraction ๐’œ ๐“œ).pred a) :
          (isLocallyFraction ๐’œ ๐“œ).pred (-a)

          Module-valued sheaf #

          source
          def AlgebraicGeometry.Proj.sectionsAddSubgroup {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) :
          AddSubgroup ((x : โ†ฅU) โ†’ โ†ฅ(Fiber ๐’œ ๐“œ โ†‘x))

          The locally fractional sections form an additive subgroup.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            noncomputable instance AlgebraicGeometry.Proj.sectionFiberModule {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†ฅU) :
            Module โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj (Opposite.op U)) โ†ฅ(Fiber ๐’œ ๐“œ โ†‘x)

            Evaluation of a structure-sheaf section makes every fiber a module over the ring of sections on the ambient open.

            Equations
            source
            def AlgebraicGeometry.Proj.sectionsSubmodule {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) :
            Submodule (โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj (Opposite.op U))) ((x : โ†ฅU) โ†’ โ†ฅ(Fiber ๐’œ ๐“œ โ†‘x))

            The locally fractional sections form a module over Mathlib's structure-sheaf sections.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def AlgebraicGeometry.Proj.associatedSheafInType {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] :
              TopCat.Sheaf (Type u) (ProjectiveSpectrum.top ๐’œ)

              The Type-valued sheaf underlying the associated graded-module sheaf.

              Equations
              Instances For
                source
                @[implicit_reducible]
                noncomputable instance AlgebraicGeometry.Proj.instAddCommGroupObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyAssociatedSheafInType {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
                AddCommGroup ((associatedSheafInType ๐’œ ๐“œ).obj.obj U)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                @[implicit_reducible]
                noncomputable instance AlgebraicGeometry.Proj.instModuleCarrierObjOppositeOpensCarrierTopCommRingCatObjFunctorIsSheafGrothendieckTopologyStructureSheafTypeAssociatedSheafInType {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
                Module (โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj U)) ((associatedSheafInType ๐’œ ๐“œ).obj.obj U)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                noncomputable def AlgebraicGeometry.Proj.associatedPresheafInAddCommGrp {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] :
                TopCat.Presheaf AddCommGrpCat (ProjectiveSpectrum.top ๐’œ)

                The additive presheaf underlying Mฬƒ.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def AlgebraicGeometry.Proj.associatedPresheaf {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] :
                  PresheafOfModules ((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.comp (CategoryTheory.forgetโ‚‚ CommRingCat RingCat))

                  The presheaf of modules over Mathlib's structure presheaf.

                  Equations
                  Instances For
                    source
                    noncomputable def AlgebraicGeometry.Proj.associatedPresheafCompForget {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] :
                    CategoryTheory.Functor.comp (associatedPresheafInAddCommGrp ๐’œ ๐“œ) (CategoryTheory.forget AddCommGrpCat) โ‰… (associatedSheafInType ๐’œ ๐“œ).obj

                    Forgetting the additive structure recovers the locally-fractional Type-valued sheaf.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def AlgebraicGeometry.Proj.associatedSheaf {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] :
                      (Proj ๐’œ).Modules

                      The sheaf Mฬƒ of modules on Proj ๐’œ associated to the graded module M.

                      Equations
                      Instances For

                        Restrictions and stalks #

                        source
                        @[simp]
                        theorem AlgebraicGeometry.Proj.associatedPresheaf_res_apply {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {U V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (i : V โŸถ U) (s : (associatedSheafInType ๐’œ ๐“œ).obj.obj V) (x : โ†ฅ(Opposite.unop U)) :
                        โ†‘((CategoryTheory.ConcreteCategory.hom ((associatedSheafInType ๐’œ ๐“œ).obj.map i)) s) x = โ†‘s (i.unop x)
                        source
                        theorem AlgebraicGeometry.Proj.section_ext {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} {s t : (associatedSheafInType ๐’œ ๐“œ).obj.obj U} (h : โ†‘s = โ†‘t) :
                        s = t
                        source
                        theorem AlgebraicGeometry.Proj.section_ext_iff {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] {๐’œ : โ„• โ†’ ฯƒA} {๐“œ : โ„• โ†’ ฯƒM} [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} {s t : (associatedSheafInType ๐’œ ๐“œ).obj.obj U} :
                        s = t โ†” โ†‘s = โ†‘t
                        source
                        def AlgebraicGeometry.Proj.sectionInBasicOpen {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (x : ProjectiveSpectrum ๐’œ) (c : GradedModule.NumDenSameDeg ๐’œ ๐“œ x.asHomogeneousIdeal.toIdeal.primeCompl) :
                        (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ โ†‘c.den))

                        A homogeneous module fraction at x defines a section on the basic open cut out by its denominator.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[simp]
                          theorem AlgebraicGeometry.Proj.sectionInBasicOpen_apply {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (x : ProjectiveSpectrum ๐’œ) (c : GradedModule.NumDenSameDeg ๐’œ ๐“œ x.asHomogeneousIdeal.toIdeal.primeCompl) (y : โ†ฅ(ProjectiveSpectrum.basicOpen ๐’œ โ†‘c.den)) :
                          โ†‘(sectionInBasicOpen ๐’œ ๐“œ x c) y = GradedModule.DegreeZeroLocalization.mk { deg := c.deg, num := c.num, den := c.den, den_mem := โ‹ฏ }
                          source
                          theorem AlgebraicGeometry.Proj.mem_basicOpen_den {A M ฯƒA ฯƒM : Type u} [CommRing A] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (c : GradedModule.NumDenSameDeg ๐’œ ๐“œ x.asHomogeneousIdeal.toIdeal.primeCompl) :
                          x โˆˆ ProjectiveSpectrum.basicOpen ๐’œ โ†‘c.den
                          source
                          noncomputable def AlgebraicGeometry.Proj.stalkToFiber {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                          (associatedSheafInType ๐’œ ๐“œ).presheaf.stalk x โŸถ โ†ฅ(Fiber ๐’œ ๐“œ x)

                          Evaluation of germs gives the canonical map from the stalk of Mฬƒ to the degree-zero homogeneous localization at x.

                          Equations
                          Instances For
                            source
                            @[simp]
                            theorem AlgebraicGeometry.Proj.stalkToFiber_germ {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) (s : (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op U)) :
                            (CategoryTheory.ConcreteCategory.hom (stalkToFiber ๐’œ ๐“œ x)) ((CategoryTheory.ConcreteCategory.hom ((associatedSheafInType ๐’œ ๐“œ).presheaf.germ U x hx)) s) = โ†‘s โŸจx, hxโŸฉ
                            source
                            theorem AlgebraicGeometry.Proj.stalkToFiber_surjective {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                            Function.Surjective โ‡‘(CategoryTheory.ConcreteCategory.hom (stalkToFiber ๐’œ ๐“œ x))
                            source
                            theorem AlgebraicGeometry.Proj.stalkToFiber_injective {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                            Function.Injective โ‡‘(CategoryTheory.ConcreteCategory.hom (stalkToFiber ๐’œ ๐“œ x))
                            source
                            noncomputable def AlgebraicGeometry.Proj.stalkEquiv {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                            (associatedSheafInType ๐’œ ๐“œ).presheaf.stalk x โ‰ƒ โ†ฅ(Fiber ๐’œ ๐“œ x)

                            The stalk of the associated sheaf at x is the degree-zero homogeneous localization of the graded module at the corresponding homogeneous prime.

                            Equations
                            Instances For
                              source
                              @[simp]
                              theorem AlgebraicGeometry.Proj.stalkEquiv_germ {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) (s : (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op U)) :
                              (stalkEquiv ๐’œ ๐“œ x) ((CategoryTheory.ConcreteCategory.hom ((associatedSheafInType ๐’œ ๐“œ).presheaf.germ U x hx)) s) = โ†‘s โŸจx, hxโŸฉ

                              Changing the grading by a membership equivalence #

                              The section-level counterpart of DegreeZeroLocalization.linearEquivOfMemIff. Applied pointwise, it moves nothing: the underlying dependent function and the local fraction's numerator and denominator are unchanged, and only the membership certificate is rebuilt.

                              source
                              noncomputable def AlgebraicGeometry.Proj.sectionAddEquivOfMemIff {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {ฯƒN : Type u} [SetLike ฯƒN M] [AddSubgroupClass ฯƒN M] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (hmem : โˆ€ (i : โ„•) (m : M), m โˆˆ ๐“œ i โ†” m โˆˆ ๐“ i) (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                              (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op U) โ‰ƒ+ (associatedSheafInType ๐’œ ๐“).obj.obj (Opposite.op U)

                              Sections of the associated sheaf depend only on the membership predicates of the graded pieces.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[simp]
                                theorem AlgebraicGeometry.Proj.sectionAddEquivOfMemIff_apply {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {ฯƒN : Type u} [SetLike ฯƒN M] [AddSubgroupClass ฯƒN M] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (hmem : โˆ€ (i : โ„•) (m : M), m โˆˆ ๐“œ i โ†” m โˆˆ ๐“ i) (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (s : (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op U)) (x : โ†ฅU) :
                                โ†‘((sectionAddEquivOfMemIff ๐’œ ๐“œ ๐“ hmem U) s) x = (GradedModule.DegreeZeroLocalization.linearEquivOfMemIff ๐“ hmem) (โ†‘s x)

                                Sections on a basic open #

                                source
                                noncomputable def AlgebraicGeometry.Proj.moduleAwayToSection {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (f : A) :
                                โ†ฅ(GradedModule.DegreeZeroLocalization ๐’œ ๐“œ (Submonoid.powers f)) โ†’+ (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ f))

                                The canonical additive map from the degree-zero homogeneous localization away from f to sections of Mฬƒ on Dโ‚Š(f). At a point x, it enlarges the denominator submonoid from the powers of f to the complement of the corresponding homogeneous prime.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[simp]
                                  theorem AlgebraicGeometry.Proj.moduleAwayToSection_apply {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (f : A) (z : โ†ฅ(GradedModule.DegreeZeroLocalization ๐’œ ๐“œ (Submonoid.powers f))) (x : โ†ฅ(ProjectiveSpectrum.basicOpen ๐’œ f)) :
                                  โ†‘((moduleAwayToSection ๐’œ ๐“œ f) z) x = (GradedModule.DegreeZeroLocalization.mapOfLE โ‹ฏ) z
                                  source
                                  @[simp]
                                  theorem AlgebraicGeometry.Proj.moduleAwayToSection_mk {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (f : A) (c : GradedModule.NumDenSameDeg ๐’œ ๐“œ (Submonoid.powers f)) :
                                  (moduleAwayToSection ๐’œ ๐“œ f) (GradedModule.DegreeZeroLocalization.mk c) = โŸจfun (x : โ†ฅ(Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ f)))) => GradedModule.DegreeZeroLocalization.mk { deg := c.deg, num := c.num, den := c.den, den_mem := โ‹ฏ }, โ‹ฏโŸฉ
                                  source
                                  theorem AlgebraicGeometry.Proj.moduleAwayToSection_unique {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (f : A) (g : โ†ฅ(GradedModule.DegreeZeroLocalization ๐’œ ๐“œ (Submonoid.powers f)) โ†’+ (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ f))) (hg : โˆ€ (c : GradedModule.NumDenSameDeg ๐’œ ๐“œ (Submonoid.powers f)), g (GradedModule.DegreeZeroLocalization.mk c) = (moduleAwayToSection ๐’œ ๐“œ f) (GradedModule.DegreeZeroLocalization.mk c)) :
                                  g = moduleAwayToSection ๐’œ ๐“œ f

                                  Universal characterization of the basic-open comparison: an additive map out of the degree-zero localization is the canonical comparison as soon as it has the canonical value on every homogeneous fraction.

                                  Faces and restriction #

                                  The ฤŒech differential restricts a section from an intersection to a smaller one, and on the algebraic side that is DegreeZeroLocalization.faceMap. These two results say the basic-open comparison intertwines them, which is what lets the differential be transported.

                                  source
                                  theorem AlgebraicGeometry.Proj.mapOfLE_faceMap {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {f g h : A} {e : โ„•} (hh : h โˆˆ ๐’œ e) (hgh : f * h โˆˆ Submonoid.powers g) (hg : f * h = g) {T : Submonoid A} (hfT : Submonoid.powers f โ‰ค T) (hgT : Submonoid.powers g โ‰ค T) (z : โ†ฅ(GradedModule.DegreeZeroLocalization ๐’œ ๐“œ (Submonoid.powers f))) :
                                  (GradedModule.DegreeZeroLocalization.mapOfLE hgT) ((GradedModule.DegreeZeroLocalization.faceMap hh hgh hg) z) = (GradedModule.DegreeZeroLocalization.mapOfLE hfT) z

                                  Enlarging the denominators past both face denominators absorbs the face map.

                                  Once f and g = f * h are both inverted in T, the fraction hโฟ m / gโฟ produced by the face map is the same element as m / fโฟ: the two differ by the unit hโฟ.

                                  source
                                  theorem AlgebraicGeometry.Proj.moduleAwayToSection_res_faceMap {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {f g h : A} {e : โ„•} (hh : h โˆˆ ๐’œ e) (hgh : f * h โˆˆ Submonoid.powers g) (hg : f * h = g) (i : Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ f) โŸถ Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ g)) (z : โ†ฅ(GradedModule.DegreeZeroLocalization ๐’œ ๐“œ (Submonoid.powers f))) :
                                  (CategoryTheory.ConcreteCategory.hom ((associatedSheafInType ๐’œ ๐“œ).obj.map i)) ((moduleAwayToSection ๐’œ ๐“œ f) z) = (moduleAwayToSection ๐’œ ๐“œ g) ((GradedModule.DegreeZeroLocalization.faceMap hh hgh hg) z)

                                  The basic-open comparison commutes with restriction along a face.

                                  This is the sheaf-level form of mapOfLE_faceMap. It holds pointwise and for a cheap reason: moduleAwayToSection is defined by enlarging denominators at each point, and restriction only reindexes the point, so nothing has to be pushed through a constructed equivalence.

                                  source
                                  @[simp]
                                  theorem AlgebraicGeometry.Proj.stalkEquiv_germ_moduleAwayToSection {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] (f : A) (z : โ†ฅ(GradedModule.DegreeZeroLocalization ๐’œ ๐“œ (Submonoid.powers f))) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ ProjectiveSpectrum.basicOpen ๐’œ f) :
                                  (stalkEquiv ๐’œ ๐“œ x) ((CategoryTheory.ConcreteCategory.hom ((associatedSheafInType ๐’œ ๐“œ).presheaf.germ (ProjectiveSpectrum.basicOpen ๐’œ f) x hx)) ((moduleAwayToSection ๐’œ ๐“œ f) z)) = (GradedModule.DegreeZeroLocalization.mapOfLE โ‹ฏ) z

                                  Germ evaluation of the basic-open comparison is the canonical enlargement-of-denominators map into the homogeneous localization at the point.

                                  Functoriality in the graded module #

                                  source
                                  noncomputable def AlgebraicGeometry.Proj.mapSection {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {N ฯƒN : Type u} [AddCommGroup N] [Module A N] [SetLike ฯƒN N] [AddSubgroupClass ฯƒN N] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (f : GradedModule.GradedLinearMap ๐“œ ๐“) {U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s : (associatedSheafInType ๐’œ ๐“œ).obj.obj U) :
                                  (associatedSheafInType ๐’œ ๐“).obj.obj U

                                  Apply a grading-preserving linear map pointwise to a locally fractional section.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem AlgebraicGeometry.Proj.mapSection_apply {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {N ฯƒN : Type u} [AddCommGroup N] [Module A N] [SetLike ฯƒN N] [AddSubgroupClass ฯƒN N] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (f : GradedModule.GradedLinearMap ๐“œ ๐“) {U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s : (associatedSheafInType ๐’œ ๐“œ).obj.obj U) (x : โ†ฅ(Opposite.unop U)) :
                                    โ†‘(mapSection ๐’œ ๐“œ ๐“ f s) x = (GradedModule.GradedLinearMap.map ๐’œ ๐“œ (โ†‘x).asHomogeneousIdeal.toIdeal.primeCompl ๐“ f) (โ†‘s x)
                                    source
                                    noncomputable def AlgebraicGeometry.Proj.mapSectionLinear {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {N ฯƒN : Type u} [AddCommGroup N] [Module A N] [SetLike ฯƒN N] [AddSubgroupClass ฯƒN N] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (f : GradedModule.GradedLinearMap ๐“œ ๐“) (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
                                    (associatedSheafInType ๐’œ ๐“œ).obj.obj U โ†’โ‚—[โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj U)] (associatedSheafInType ๐’œ ๐“).obj.obj U

                                    The pointwise map on sections, bundled as a linear map over the sections of ๐’ช.

                                    Equations
                                    Instances For
                                      source
                                      noncomputable def AlgebraicGeometry.Proj.associatedMapPresheaf {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {N ฯƒN : Type u} [AddCommGroup N] [Module A N] [SetLike ฯƒN N] [AddSubgroupClass ฯƒN N] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (f : GradedModule.GradedLinearMap ๐“œ ๐“) :
                                      associatedPresheaf ๐’œ ๐“œ โŸถ associatedPresheaf ๐’œ ๐“

                                      A grading-preserving map induces a morphism of the associated presheaves of modules.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        noncomputable def AlgebraicGeometry.Proj.associatedMap {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {N ฯƒN : Type u} [AddCommGroup N] [Module A N] [SetLike ฯƒN N] [AddSubgroupClass ฯƒN N] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (f : GradedModule.GradedLinearMap ๐“œ ๐“) :
                                        associatedSheaf ๐’œ ๐“œ โŸถ associatedSheaf ๐’œ ๐“

                                        A grading-preserving linear map M โ†’ N induces the sheaf morphism Mฬƒ โ†’ Nฬƒ.

                                        Equations
                                        Instances For
                                          source
                                          @[simp]
                                          theorem AlgebraicGeometry.Proj.associatedMap_app_apply {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {N ฯƒN : Type u} [AddCommGroup N] [Module A N] [SetLike ฯƒN N] [AddSubgroupClass ฯƒN N] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (f : GradedModule.GradedLinearMap ๐“œ ๐“) (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (s : (associatedSheafInType ๐’œ ๐“œ).obj.obj (Opposite.op U)) (x : โ†ฅU) :
                                          โ†‘((CategoryTheory.ConcreteCategory.hom (Scheme.Modules.Hom.app (associatedMap ๐’œ ๐“œ ๐“ f) U)) s) x = (GradedModule.GradedLinearMap.map ๐’œ ๐“œ (โ†‘x).asHomogeneousIdeal.toIdeal.primeCompl ๐“ f) (โ†‘s x)

                                          Isomorphisms induced by equal graded-piece memberships #

                                          source
                                          def AlgebraicGeometry.Proj.identityGradedMap {A M ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒM M] (๐“œ : โ„• โ†’ ฯƒM) {ฯƒN : Type u} [SetLike ฯƒN M] [AddSubgroupClass ฯƒN M] (๐“ : โ„• โ†’ ฯƒN) (h : โˆ€ (i : โ„•), โˆ€ m โˆˆ ๐“œ i, m โˆˆ ๐“ i) :
                                          GradedModule.GradedLinearMap ๐“œ ๐“

                                          The identity linear map bundled as a graded map when every source piece is contained in the corresponding target piece.

                                          Equations
                                          Instances For
                                            source
                                            noncomputable def AlgebraicGeometry.Proj.associatedIsoOfPiecewiseIff {A M ฯƒA ฯƒM : Type u} [CommRing A] [AddCommGroup M] [Module A M] [SetLike ฯƒA A] [AddSubgroupClass ฯƒA A] [SetLike ฯƒM M] [AddSubgroupClass ฯƒM M] (๐’œ : โ„• โ†’ ฯƒA) (๐“œ : โ„• โ†’ ฯƒM) [GradedRing ๐’œ] [SetLike.GradedSMul ๐’œ ๐“œ] {ฯƒN : Type u} [SetLike ฯƒN M] [AddSubgroupClass ฯƒN M] (๐“ : โ„• โ†’ ฯƒN) [SetLike.GradedSMul ๐’œ ๐“] (h : โˆ€ (i : โ„•) (m : M), m โˆˆ ๐“œ i โ†” m โˆˆ ๐“ i) :
                                            associatedSheaf ๐’œ ๐“œ โ‰… associatedSheaf ๐’œ ๐“

                                            Associated sheaves only depend on the membership predicates of the graded pieces. This packages the identity on the underlying module as an isomorphism whenever those predicates agree.

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