Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

The structure sheaf on ProjectiveSpectrum ๐’œ. #

In Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean, 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
๐Ÿ”น coverage
def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.IsFraction {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] {U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)} (f : (x : โ†ฅU) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal) :
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).

Instances For
    source
    ๐Ÿ”ธ coverage
    def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isFractionPrelocal {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
    TopCat.PrelocalPredicate fun (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) => HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal

    The predicate IsFraction is "prelocal", in the sense that if it holds on U it holds on any open subset V of U.

    Instances For
      source
      ๐Ÿ”ธ coverage
      def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
      TopCat.LocalPredicate fun (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) => HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal

      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.

      Instances For
        source
        ๐Ÿ“ coverage
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem' {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
        (isLocallyFraction ๐’œ).pred 0
        source
        ๐Ÿ“ coverage
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem' {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
        (isLocallyFraction ๐’œ).pred 1
        source
        ๐Ÿ“ coverage
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem' {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) (a b : (x : โ†ฅ(Opposite.unop U)) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal) (ha : (isLocallyFraction ๐’œ).pred a) (hb : (isLocallyFraction ๐’œ).pred b) :
        (isLocallyFraction ๐’œ).pred (a + b)
        source
        ๐Ÿ“ coverage
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem' {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) (a : (x : โ†ฅ(Opposite.unop U)) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal) (ha : (isLocallyFraction ๐’œ).pred a) :
        (isLocallyFraction ๐’œ).pred (-a)
        source
        ๐Ÿ“ coverage
        theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem' {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) (a b : (x : โ†ฅ(Opposite.unop U)) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal) (ha : (isLocallyFraction ๐’œ).pred a) (hb : (isLocallyFraction ๐’œ).pred b) :
        (isLocallyFraction ๐’œ).pred (a * b)
        source
        ๐Ÿ”ธ coverage
        def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.sectionsSubring {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
        Subring ((x : โ†ฅ(Opposite.unop U)) โ†’ HomogeneousLocalization.AtPrime ๐’œ (โ†‘x).asHomogeneousIdeal.toIdeal)

        The functions satisfying isLocallyFraction form a subring of all dependent functions ฮ  x : U, HomogeneousLocalization ๐’œ x.

        Instances For
          source
          ๐Ÿ”ธ coverage
          def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
          TopCat.Sheaf (Type u_1) (ProjectiveSpectrum.top ๐’œ)

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

          Instances For
            source
            ๐Ÿ”ธ coverage
            @[implicit_reducible]
            instance AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.commRingStructureSheafInTypeObj {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
            CommRing ((structureSheafInType ๐’œ).obj.obj U)
            source
            ๐Ÿ”ธ coverage
            def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
            TopCat.Presheaf CommRingCat (ProjectiveSpectrum.top ๐’œ)

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

            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (U : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–) :
              โ†‘((structurePresheafInCommRing ๐’œ).obj U) = (structureSheafInType ๐’œ).obj.obj U
              source
              ๐Ÿ”ธ coverage
              def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafCompForget {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
              CategoryTheory.Functor.comp (structurePresheafInCommRing ๐’œ) (CategoryTheory.forget CommRingCat) โ‰… (structureSheafInType ๐’œ).obj

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

              Instances For
                source
                ๐Ÿ”ธ coverage
                def AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
                TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top ๐’œ)

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

                Instances For
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AlgebraicGeometry.Proj.res_apply {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {U V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (i : V โŸถ U) (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj V)) (x : โ†ฅ(Opposite.unop U)) :
                  โ†‘((CategoryTheory.ConcreteCategory.hom ((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.map i)) s) x = โ†‘s (i.unop x)
                  source
                  theorem AlgebraicGeometry.Proj.ext {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj V)) (h : โ†‘s = โ†‘t) :
                  s = t
                  source
                  ๐Ÿ“ coverage
                  theorem AlgebraicGeometry.Proj.ext_iff {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] {๐’œ : โ„• โ†’ ฯƒ} [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} {s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj V)} :
                  s = t โ†” โ†‘s = โ†‘t
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AlgebraicGeometry.Proj.add_apply {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj V)) (x : โ†ฅ(Opposite.unop V)) :
                  โ†‘(s + t) x = โ†‘s x + โ†‘t x
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AlgebraicGeometry.Proj.mul_apply {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj V)) (x : โ†ฅ(Opposite.unop V)) :
                  โ†‘(s * t) x = โ†‘s x * โ†‘t x
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AlgebraicGeometry.Proj.sub_apply {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s t : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj V)) (x : โ†ฅ(Opposite.unop V)) :
                  โ†‘(s - t) x = โ†‘s x - โ†‘t x
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AlgebraicGeometry.Proj.pow_apply {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj V)) (x : โ†ฅ(Opposite.unop V)) (n : โ„•) :
                  โ†‘(s ^ n) x = โ†‘s x ^ n
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AlgebraicGeometry.Proj.zero_apply {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (x : โ†ฅ(Opposite.unop V)) :
                  โ†‘0 x = 0
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AlgebraicGeometry.Proj.one_apply {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] {V : (TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ))แต’แต–} (x : โ†ฅ(Opposite.unop V)) :
                  โ†‘1 x = 1
                  source
                  ๐Ÿ”ธ coverage
                  def AlgebraicGeometry.Proj.toSheafedSpace {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
                  SheafedSpace CommRingCat

                  Proj of a graded ring as a SheafedSpace

                  Instances For
                    source
                    ๐Ÿ”ธ coverage
                    def AlgebraicGeometry.openToLocalization {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) :
                    (ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj (Opposite.op U) โŸถ CommRingCat.of (HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal)

                    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.

                    Instances For
                      source
                      ๐Ÿ”ธ coverage
                      noncomputable def AlgebraicGeometry.stalkToFiberRingHom {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                      (ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.stalk x โŸถ CommRingCat.of (HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal)

                      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.

                      Instances For
                        source
                        ๐Ÿ“ coverage
                        @[simp]
                        theorem AlgebraicGeometry.germ_comp_stalkToFiberRingHom {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) :
                        CategoryTheory.CategoryStruct.comp ((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.germ U x hx) (stalkToFiberRingHom ๐’œ x) = openToLocalization ๐’œ U x hx
                        source
                        ๐Ÿ“ coverage
                        @[simp]
                        theorem AlgebraicGeometry.stalkToFiberRingHom_germ {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj (Opposite.op U))) :
                        (CategoryTheory.ConcreteCategory.hom (stalkToFiberRingHom ๐’œ x)) ((CategoryTheory.ConcreteCategory.hom ((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.germ U x hx)) s) = โ†‘s โŸจx, hxโŸฉ
                        source
                        ๐Ÿ“ coverage
                        theorem AlgebraicGeometry.mem_basicOpen_den {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (f : HomogeneousLocalization.NumDenSameDeg ๐’œ x.asHomogeneousIdeal.toIdeal.primeCompl) :
                        x โˆˆ ProjectiveSpectrum.basicOpen ๐’œ โ†‘f.den
                        source
                        ๐Ÿ”ธ coverage
                        def AlgebraicGeometry.sectionInBasicOpen {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (f : HomogeneousLocalization.NumDenSameDeg ๐’œ x.asHomogeneousIdeal.toIdeal.primeCompl) :
                        โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj (Opposite.op (ProjectiveSpectrum.basicOpen ๐’œ โ†‘f.den)))

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

                        Instances For
                          source
                          ๐Ÿ”ธ coverage
                          noncomputable def AlgebraicGeometry.homogeneousLocalizationToStalk {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (y : HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal) :
                          โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.stalk 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.

                          Instances For
                            source
                            ๐Ÿ“ coverage
                            theorem AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (z : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.stalk x)) :
                            homogeneousLocalizationToStalk ๐’œ x ((CategoryTheory.ConcreteCategory.hom (stalkToFiberRingHom ๐’œ x)) z) = z
                            source
                            ๐Ÿ“ coverage
                            theorem AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (z : HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal) :
                            (CategoryTheory.ConcreteCategory.hom (stalkToFiberRingHom ๐’œ x)) (homogeneousLocalizationToStalk ๐’œ x z) = z
                            source
                            ๐Ÿ”ธ coverage
                            noncomputable def AlgebraicGeometry.Proj.stalkIso' {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) :
                            โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.stalk x) โ‰ƒ+* HomogeneousLocalization.AtPrime ๐’œ x.asHomogeneousIdeal.toIdeal

                            Using homogeneousLocalizationToStalk, we construct a ring isomorphism between stalk at x and homogeneous localization at x for any point x in Proj.

                            Instances For
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem AlgebraicGeometry.Proj.stalkIso'_germ {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (U : TopologicalSpace.Opens โ†‘(ProjectiveSpectrum.top ๐’œ)) (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (hx : x โˆˆ U) (s : โ†‘((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).obj.obj (Opposite.op U))) :
                              (stalkIso' ๐’œ x) ((CategoryTheory.ConcreteCategory.hom ((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.germ U x hx)) s) = โ†‘s โŸจx, hxโŸฉ
                              source
                              ๐Ÿ“ coverage
                              @[simp]
                              theorem AlgebraicGeometry.Proj.stalkIso'_symm_mk {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] (x : โ†‘(ProjectiveSpectrum.top ๐’œ)) (f : HomogeneousLocalization.NumDenSameDeg ๐’œ x.asHomogeneousIdeal.toIdeal.primeCompl) :
                              (stalkIso' ๐’œ x).symm (HomogeneousLocalization.mk f) = (CategoryTheory.ConcreteCategory.hom ((ProjectiveSpectrum.Proj.structureSheaf ๐’œ).presheaf.germ (ProjectiveSpectrum.basicOpen ๐’œ โ†‘f.den) x โ‹ฏ)) (sectionInBasicOpen ๐’œ x f)
                              source
                              ๐Ÿ”ธ coverage
                              def AlgebraicGeometry.Proj.toLocallyRingedSpace {A : Type u_1} {ฯƒ : Type u_2} [CommRing A] [SetLike ฯƒ A] [AddSubgroupClass ฯƒ A] (๐’œ : โ„• โ†’ ฯƒ) [GradedRing ๐’œ] :
                              LocallyRingedSpace

                              Proj of a graded ring as a LocallyRingedSpace

                              Instances For