Documentation

Mathlib.AlgebraicGeometry.Modules.Tilde

Construction of M^~ #

Given any commutative ring R and R-module M, we construct the sheaf M^~ of ๐’ช_SpecR-modules such that M^~(U) is the set of dependent functions that are locally fractions.

Main definitions #

Technical note #

To get the R-module structure on the stalks on M^~, we had to define ModuleCat.tildeInModuleCat, which is M^~ seen as sheaf of R-modules. We get it by applying a forgetful functor to ModuleCat.tilde M.

source
@[reducible, inline]
abbrev ModuleCat.Tilde.Localizations {R : Type u} [CommRing R] (M : ModuleCat R) (P : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
Type u

For an R-module M and a point P in Spec R, Localizations P is the localized module M at the prime ideal P.

Equations
    Instances For
      source
      def ModuleCat.Tilde.isFraction {R : Type u} [CommRing R] (M : ModuleCat R) {U : TopologicalSpace.Opens (PrimeSpectrum R)} (f : (๐”ญ : โ†ฅU) โ†’ Localizations M โ†‘๐”ญ) :
      Prop

      For any open subset U โŠ† Spec R, IsFraction is the predicate expressing that a function f : โˆ_{x โˆˆ U}, Mโ‚“ is such that for any ๐”ญ โˆˆ U, f ๐”ญ = m / s for some m : M and s โˆ‰ ๐”ญ. In short f is a fraction on U.

      Equations
        Instances For
          source
          def ModuleCat.Tilde.isFractionPrelocal {R : Type u} [CommRing R] (M : ModuleCat R) :
          TopCat.PrelocalPredicate (Localizations M)

          The property of a function f : โˆ_{x โˆˆ U}, Mโ‚“ being a fraction is stable under restriction.

          Equations
            Instances For
              source
              def ModuleCat.Tilde.isLocallyFraction {R : Type u} [CommRing R] (M : ModuleCat R) :
              TopCat.LocalPredicate (Localizations M)

              For any open subset U โŠ† Spec R, IsLocallyFraction is the predicate expressing that a function f : โˆ_{x โˆˆ U}, Mโ‚“ is such that for any ๐”ญ โˆˆ U, there exists an open neighbourhood V โˆ‹ ๐”ญ, such that for any ๐”ฎ โˆˆ V, f ๐”ฎ = m / s for some m : M and s โˆ‰ ๐”ฎ. In short f is locally a fraction on U.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem ModuleCat.Tilde.isLocallyFraction_pred {R : Type u} [CommRing R] (M : ModuleCat R) {U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)} (f : (x : โ†ฅU) โ†’ Localizations M โ†‘x) :
                  (isLocallyFraction M).pred f = โˆ€ (y : โ†ฅU), โˆƒ (V : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (_ : โ†‘y โˆˆ V) (i : V โŸถ U) (m : โ†‘M) (s : R), โˆ€ (x : โ†ฅV), s โˆ‰ (โ†‘x).asIdeal โˆง s โ€ข f (i x) = (LocalizedModule.mkLinearMap (โ†‘x).asIdeal.primeCompl โ†‘M) m
                  source
                  noncomputable instance ModuleCat.Tilde.instModuleCarrierObjOppositeOpensCarrierTopCommRingCatValStructureSheafLocalizationsValMemUnop {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R))แต’แต–) (x : โ†ฅ(Opposite.unop U)) :
                  Module (โ†‘((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)) (Localizations M โ†‘x)
                  Equations
                    source
                    @[simp]
                    theorem ModuleCat.Tilde.sections_smul_localizations_def {R : Type u} [CommRing R] (M : ModuleCat R) {U : (TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R))แต’แต–} (x : โ†ฅ(Opposite.unop U)) (r : โ†‘((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)) (m : Localizations M โ†‘x) :
                    r โ€ข m = โ†‘r x โ€ข m
                    source
                    noncomputable def ModuleCat.Tilde.sectionsSubmodule {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens (PrimeSpectrum R))แต’แต–) :
                    Submodule (โ†‘((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)) ((x : โ†ฅ(Opposite.unop U)) โ†’ Localizations M โ†‘x)

                    For any R-module M and any open subset U โŠ† Spec R, M^~(U) is an ๐’ช_{Spec R}(U)-submodule of โˆ_{๐”ญ โˆˆ U} M_๐”ญ.

                    Equations
                      Instances For
                        source
                        def ModuleCat.tildeInType {R : Type u} [CommRing R] (M : ModuleCat R) :
                        TopCat.Sheaf (Type u) (AlgebraicGeometry.PrimeSpectrum.Top R)

                        For any R-module M, TildeInType R M is the sheaf of set on Spec R whose sections on U are the dependent functions that are locally fractions. This is often denoted by M^~.

                        See also Tilde.isLocallyFraction.

                        Equations
                          Instances For
                            source
                            noncomputable instance ModuleCat.instAddCommGroupObjOppositeOpensCarrierTopValTildeInType {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R))แต’แต–) :
                            AddCommGroup (M.tildeInType.val.obj U)
                            Equations
                              source
                              noncomputable instance ModuleCat.instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecOfRingCatValRingCatSheafTopTildeInType {R : Type u} [CommRing R] (M : ModuleCat R) (U : (TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R))แต’แต–) :
                              Module (โ†‘((AlgebraicGeometry.Spec (CommRingCat.of R)).ringCatSheaf.val.obj U)) (M.tildeInType.val.obj U)
                              Equations
                                source
                                noncomputable def ModuleCat.tilde {R : Type u} [CommRing R] (M : ModuleCat R) :
                                (AlgebraicGeometry.Spec (CommRingCat.of R)).Modules

                                M^~ as a sheaf of ๐’ช_{Spec R}-modules

                                Equations
                                  Instances For
                                    source
                                    noncomputable def ModuleCat.tildeInModuleCat {R : Type u} [CommRing R] (M : ModuleCat R) :
                                    TopCat.Presheaf (ModuleCat R) (AlgebraicGeometry.PrimeSpectrum.Top R)

                                    This is M^~ as a sheaf of R-modules.

                                    Equations
                                      Instances For
                                        source
                                        @[simp]
                                        theorem ModuleCat.Tilde.res_apply {R : Type u} [CommRing R] (M : ModuleCat R) (U V : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V โŸถ U) (s : โ†‘(M.tildeInModuleCat.obj (Opposite.op U))) (x : โ†ฅV) :
                                        โ†‘((CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.map i.op)) s) x = โ†‘s (i x)
                                        source
                                        theorem ModuleCat.Tilde.smul_section_apply {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (s : โ†‘(M.tildeInModuleCat.obj (Opposite.op U))) (x : โ†ฅU) :
                                        โ†‘(r โ€ข s) x = r โ€ข โ†‘s x
                                        source
                                        theorem ModuleCat.Tilde.smul_stalk_no_nonzero_divisor {R : Type u} [CommRing R] (M : ModuleCat R) {x : PrimeSpectrum R} (r : โ†ฅx.asIdeal.primeCompl) (st : โ†‘(M.tildeInModuleCat.stalk x)) (hst : โ†‘r โ€ข st = 0) :
                                        st = 0
                                        source
                                        noncomputable def ModuleCat.Tilde.toOpen {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                        of R โ†‘M โŸถ M.tildeInModuleCat.obj (Opposite.op U)

                                        If U is an open subset of Spec R, this is the morphism of R-modules from M to M^~(U).

                                        Equations
                                          Instances For
                                            source
                                            @[simp]
                                            theorem ModuleCat.Tilde.toOpen_res {R : Type u} [CommRing R] (M : ModuleCat R) (U V : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V โŸถ U) :
                                            CategoryTheory.CategoryStruct.comp (toOpen M U) (M.tildeInModuleCat.map i.op) = toOpen M V
                                            source
                                            noncomputable def ModuleCat.Tilde.toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                            of R โ†‘M โŸถ M.tildeInModuleCat.stalk x

                                            If x is a point of Spec R, this is the morphism of R-modules from M to the stalk of M^~ at x.

                                            Equations
                                              Instances For
                                                source
                                                theorem ModuleCat.Tilde.isUnit_toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (r : โ†ฅx.asIdeal.primeCompl) :
                                                IsUnit ((algebraMap R (Module.End R โ†‘(M.tildeInModuleCat.stalk x))) โ†‘r)
                                                source
                                                noncomputable def ModuleCat.Tilde.localizationToStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                                of R (LocalizedModule x.asIdeal.primeCompl โ†‘M) โŸถ M.tildeInModuleCat.stalk x

                                                The morphism of R-modules from the localization of M at the prime ideal corresponding to x to the stalk of M^~ at x.

                                                Equations
                                                  Instances For
                                                    source
                                                    noncomputable def ModuleCat.Tilde.openToLocalization {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens (PrimeSpectrum R)) (x : PrimeSpectrum R) (hx : x โˆˆ U) :
                                                    M.tildeInModuleCat.obj (Opposite.op U) โŸถ of R (LocalizedModule x.asIdeal.primeCompl โ†‘M)

                                                    The ring homomorphism that takes a section of the structure sheaf of R on the open set U, implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates the section on the point corresponding to a given prime ideal.

                                                    Equations
                                                      Instances For
                                                        source
                                                        noncomputable def ModuleCat.Tilde.stalkToFiberLinearMap {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                                        M.tildeInModuleCat.stalk x โŸถ of R (LocalizedModule x.asIdeal.primeCompl โ†‘M)

                                                        The morphism of R-modules from the stalk of M^~ at x to the localization of M at the prime ideal of R corresponding to x.

                                                        Equations
                                                          Instances For
                                                            source
                                                            @[simp]
                                                            theorem ModuleCat.Tilde.germ_comp_stalkToFiberLinearMap {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x โˆˆ U) :
                                                            CategoryTheory.CategoryStruct.comp (M.tildeInModuleCat.germ U x hx) (stalkToFiberLinearMap M x) = openToLocalization M U x hx
                                                            source
                                                            @[simp]
                                                            theorem ModuleCat.Tilde.stalkToFiberLinearMap_germ {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x โˆˆ U) (s : โ†‘(M.tildeInModuleCat.obj (Opposite.op U))) :
                                                            (Hom.hom (stalkToFiberLinearMap M x)) ((CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.germ U x hx)) s) = โ†‘s โŸจx, hxโŸฉ
                                                            source
                                                            @[simp]
                                                            theorem ModuleCat.Tilde.toOpen_germ {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x โˆˆ U) :
                                                            CategoryTheory.CategoryStruct.comp (toOpen M U) (M.tildeInModuleCat.germ U x hx) = toStalk M x
                                                            source
                                                            @[simp]
                                                            theorem ModuleCat.Tilde.toOpen_germ_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x โˆˆ U) {Z : ModuleCat R} (h : M.tildeInModuleCat.stalk x โŸถ Z) :
                                                            CategoryTheory.CategoryStruct.comp (toOpen M U) (CategoryTheory.CategoryStruct.comp (M.tildeInModuleCat.germ U x hx) h) = CategoryTheory.CategoryStruct.comp (toStalk M x) h
                                                            source
                                                            @[simp]
                                                            theorem ModuleCat.Tilde.toOpen_germ_apply {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x โˆˆ U) (xโœ : CategoryTheory.ToType (of R โ†‘M)) :
                                                            (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (toOpen M U)) xโœ) = (CategoryTheory.ConcreteCategory.hom (toStalk M x)) xโœ
                                                            source
                                                            @[simp]
                                                            theorem ModuleCat.Tilde.toStalk_comp_stalkToFiberLinearMap {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                                            CategoryTheory.CategoryStruct.comp (toStalk M x) (stalkToFiberLinearMap M x) = ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl โ†‘M)
                                                            source
                                                            @[simp]
                                                            theorem ModuleCat.Tilde.toStalk_comp_stalkToFiberLinearMap_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) {Z : ModuleCat R} (h : of R (LocalizedModule x.asIdeal.primeCompl โ†‘M) โŸถ Z) :
                                                            CategoryTheory.CategoryStruct.comp (toStalk M x) (CategoryTheory.CategoryStruct.comp (stalkToFiberLinearMap M x) h) = CategoryTheory.CategoryStruct.comp (ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl โ†‘M)) h
                                                            source
                                                            theorem ModuleCat.Tilde.stalkToFiberLinearMap_toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (m : โ†‘M) :
                                                            (Hom.hom (stalkToFiberLinearMap M x)) ((CategoryTheory.ConcreteCategory.hom (toStalk M x)) m) = LocalizedModule.mk m 1
                                                            source
                                                            def ModuleCat.Tilde.const {R : Type u} [CommRing R] (M : ModuleCat R) (m : โ†‘M) (r : R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : โˆ€ x โˆˆ U, r โˆˆ x.asIdeal.primeCompl) :
                                                            โ†‘(M.tildeInModuleCat.obj (Opposite.op U))

                                                            If U is an open subset of Spec R, m is an element of M and r is an element of R that is invertible on U (i.e. does not belong to any prime ideal corresponding to a point in U), this is m / r seen as a section of M^~ over U.

                                                            Equations
                                                              Instances For
                                                                source
                                                                @[simp]
                                                                theorem ModuleCat.Tilde.const_apply {R : Type u} [CommRing R] (M : ModuleCat R) (m : โ†‘M) (r : R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : โˆ€ x โˆˆ U, r โˆˆ x.asIdeal.primeCompl) (x : โ†ฅU) :
                                                                โ†‘(const M m r U hu) x = LocalizedModule.mk m โŸจr, โ‹ฏโŸฉ
                                                                source
                                                                theorem ModuleCat.Tilde.exists_const {R : Type u} [CommRing R] (M : ModuleCat R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (s : โ†‘(M.tildeInModuleCat.obj (Opposite.op U))) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hx : x โˆˆ U) :
                                                                โˆƒ (V : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (_ : x โˆˆ V) (i : V โŸถ U) (f : โ†‘M) (g : R) (hg : โˆ€ x โˆˆ V, g โˆˆ x.asIdeal.primeCompl), const M f g V hg = (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.map i.op)) s
                                                                source
                                                                @[simp]
                                                                theorem ModuleCat.Tilde.res_const {R : Type u} [CommRing R] (M : ModuleCat R) (f : โ†‘M) (g : R) (U : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : โˆ€ x โˆˆ U, g โˆˆ x.asIdeal.primeCompl) (V : TopologicalSpace.Opens โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (hv : โˆ€ x โˆˆ V, g โˆˆ x.asIdeal.primeCompl) (i : Opposite.op U โŸถ Opposite.op V) :
                                                                (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.map i)) (const M f g U hu) = const M f g V hv
                                                                source
                                                                @[simp]
                                                                theorem ModuleCat.Tilde.localizationToStalk_mk {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) (f : โ†‘M) (s : โ†ฅx.asIdeal.primeCompl) :
                                                                (Hom.hom (localizationToStalk M x)) (LocalizedModule.mk f s) = (CategoryTheory.ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen โ†‘s) x โ‹ฏ)) (const M f (โ†‘s) (PrimeSpectrum.basicOpen โ†‘s) โ‹ฏ)
                                                                source
                                                                noncomputable def ModuleCat.Tilde.stalkIso {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                                                M.tildeInModuleCat.stalk x โ‰… of R (LocalizedModule x.asIdeal.primeCompl โ†‘M)

                                                                The isomorphism of R-modules from the stalk of M^~ at x to the localization of M at the prime ideal corresponding to x.

                                                                Equations
                                                                  Instances For
                                                                    source
                                                                    @[simp]
                                                                    theorem ModuleCat.Tilde.stalkIso_hom {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                                                    (stalkIso M x).hom = stalkToFiberLinearMap M x
                                                                    source
                                                                    @[simp]
                                                                    theorem ModuleCat.Tilde.stalkIso_inv {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                                                    (stalkIso M x).inv = localizationToStalk M x
                                                                    source
                                                                    instance ModuleCat.Tilde.instIsLocalizedModulePrimeComplAsIdealCarrierOfStalkTildeInModuleCatHomToStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : โ†‘(AlgebraicGeometry.PrimeSpectrum.Top R)) :
                                                                    IsLocalizedModule x.asIdeal.primeCompl (Hom.hom (toStalk M x))