Documentation

DerivedAlgGeo.AlgebraicGeometry.ProjectiveSpectrum.Modules.StructureModule

The graded ring as its associated module sheaf #

This file identifies the sheaf associated to the graded ring, considered as a graded module over itself, with the structure sheaf of Proj. It is the concrete degree-zero base case for the Proj module comparison: the equivalence is defined on every open by applying the canonical equivalence between the two degree-zero localizations pointwise, and the local-fraction predicates are checked in both directions.

source
noncomputable def AlgebraicGeometry.Proj.selfFiberLinearEquiv {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] (x : ↑(ProjectiveSpectrum.top π’œ)) :
β†₯(Fiber π’œ π’œ x) ≃ₗ[HomogeneousLocalization π’œ x.asHomogeneousIdeal.toIdeal.primeCompl] HomogeneousLocalization π’œ x.asHomogeneousIdeal.toIdeal.primeCompl

The fiber comparison underlying the structure-module isomorphism.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Proj.selfFiberLinearEquiv_apply_mk {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] (x : ↑(ProjectiveSpectrum.top π’œ)) (c : GradedModule.NumDenSameDeg π’œ π’œ x.asHomogeneousIdeal.toIdeal.primeCompl) :
    (selfFiberLinearEquiv π’œ x) (GradedModule.DegreeZeroLocalization.mk c) = HomogeneousLocalization.mk { deg := c.deg, num := c.num, den := c.den, den_mem := β‹― }
    source
    @[simp]
    theorem AlgebraicGeometry.Proj.selfFiberLinearEquiv_symm_apply_mk {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] (x : ↑(ProjectiveSpectrum.top π’œ)) (c : HomogeneousLocalization.NumDenSameDeg π’œ x.asHomogeneousIdeal.toIdeal.primeCompl) :
    (selfFiberLinearEquiv π’œ x).symm (HomogeneousLocalization.mk c) = GradedModule.DegreeZeroLocalization.mk { deg := c.deg, num := c.num, den := c.den, den_mem := β‹― }
    source
    noncomputable def AlgebraicGeometry.Proj.selfSectionToStructure {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] {U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top π’œ))α΅’α΅–} (s : (associatedSheafInType π’œ π’œ).obj.obj U) :
    ↑((ProjectiveSpectrum.Proj.structureSheaf π’œ).obj.obj U)

    Send a locally homogeneous module fraction for the graded ring to the same fraction in Mathlib's structure sheaf.

    Equations
    Instances For
      source
      noncomputable def AlgebraicGeometry.Proj.selfSectionFromStructure {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] {U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top π’œ))α΅’α΅–} (s : ↑((ProjectiveSpectrum.Proj.structureSheaf π’œ).obj.obj U)) :
      (associatedSheafInType π’œ π’œ).obj.obj U

      Send a locally homogeneous structure-sheaf fraction to the same fraction in the associated module sheaf of the graded ring.

      Equations
      Instances For
        source
        noncomputable def AlgebraicGeometry.Proj.selfSectionAddEquiv {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top π’œ))α΅’α΅–) :
        (associatedSheafInType π’œ π’œ).obj.obj U ≃+ ↑((ProjectiveSpectrum.Proj.structureSheaf π’œ).obj.obj U)

        On every open, the locally fractional sections of the graded ring as a module are additively equivalent to the sections of the structure sheaf.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def AlgebraicGeometry.Proj.selfSectionLinearEquiv {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] (U : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top π’œ))α΅’α΅–) :
          (associatedSheafInType π’œ π’œ).obj.obj U ≃ₗ[↑((ProjectiveSpectrum.Proj.structureSheaf π’œ).obj.obj U)] ↑((ProjectiveSpectrum.Proj.structureSheaf π’œ).obj.obj U)

          The openwise comparison is linear over the structure-sheaf sections.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def AlgebraicGeometry.Proj.associatedPresheafSelfIso {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] :
            associatedPresheaf π’œ π’œ β‰… PresheafOfModules.unit ((ProjectiveSpectrum.Proj.structureSheaf π’œ).obj.comp (CategoryTheory.forgetβ‚‚ CommRingCat RingCat))

            The openwise comparisons commute with restriction and hence identify the two presheaves of modules.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def AlgebraicGeometry.Proj.associatedSheafSelfIso {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] :
              associatedSheaf π’œ π’œ β‰… SheafOfModules.unit (Proj π’œ).ringCatSheaf

              The sheaf associated to the graded ring, considered as a module over itself, is canonically the structure sheaf of Proj.

              Equations
              Instances For

                The canonical basic-open comparison for the structure module #

                source
                noncomputable def AlgebraicGeometry.Proj.selfBasicOpenSectionAddEquiv {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] {f : A} {m : β„•} (f_deg : f ∈ π’œ m) (hm : 0 < m) :
                β†₯(GradedModule.DegreeZeroLocalization π’œ π’œ (Submonoid.powers f)) ≃+ (associatedSheafInType π’œ π’œ).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen π’œ f))

                On a positive-degree basic open, the comparison for the graded ring as a module is the composite of the degree-zero localization comparison, Mathlib's structure-sheaf comparison, and the inverse of associatedSheafSelfIso.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem AlgebraicGeometry.Proj.selfBasicOpenSectionAddEquiv_apply_mk {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] {f : A} {m : β„•} (f_deg : f ∈ π’œ m) (hm : 0 < m) (c : GradedModule.NumDenSameDeg π’œ π’œ (Submonoid.powers f)) :
                  (selfBasicOpenSectionAddEquiv π’œ f_deg hm) (GradedModule.DegreeZeroLocalization.mk c) = (moduleAwayToSection π’œ π’œ f) (GradedModule.DegreeZeroLocalization.mk c)

                  The additive equivalence above has the canonical value on every homogeneous fraction.

                  source
                  theorem AlgebraicGeometry.Proj.moduleAwayToSection_self_bijective {A Οƒ : Type u} [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : β„• β†’ Οƒ) [GradedRing π’œ] {f : A} {m : β„•} (f_deg : f ∈ π’œ m) (hm : 0 < m) :
                  Function.Bijective ⇑(moduleAwayToSection π’œ π’œ f)

                  For the graded ring as a module over itself, the canonical basic-open section map is bijective on every positive-degree homogeneous chart.