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.

@[reducible, inline]

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

    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

      The property of a function f : ∏_{x ∈ U}, Mₓ being a fraction is stable under restriction.

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

        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
          @[simp]
          theorem ModuleCat.Tilde.isLocallyFraction_pred {R : Type u} [CommRing R] (M : ModuleCat R) {U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)} (f : (x : U) → ModuleCat.Tilde.Localizations M x) :
          (ModuleCat.Tilde.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 ((fun (x : V) => x, ) x) = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl M) m

          For any R-module M and any open subset U ⊆ Spec R, M^~(U) is an 𝒪_{Spec R}(U)-submodule of ∏_{𝔭 ∈ U} M_𝔭.

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

            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
              Equations
              Equations
              • One or more equations did not get rendered due to their size.
              noncomputable def ModuleCat.tilde {R : Type u} [CommRing R] (M : ModuleCat R) :

              M^~ as a sheaf of 𝒪_{Spec R}-modules

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

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[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) :
                  ((M.tildeInModuleCat.map i.op).hom s) x = s ((fun (x : V) => x, ) x)
                  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
                  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

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    noncomputable def ModuleCat.Tilde.toStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : (AlgebraicGeometry.PrimeSpectrum.Top R)) :
                    ModuleCat.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
                      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)
                      noncomputable def ModuleCat.Tilde.localizationToStalk {R : Type u} [CommRing R] (M : ModuleCat R) (x : (AlgebraicGeometry.PrimeSpectrum.Top R)) :
                      ModuleCat.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
                        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) ModuleCat.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
                          noncomputable def ModuleCat.Tilde.stalkToFiberLinearMap {R : Type u} [CommRing R] (M : ModuleCat R) (x : (AlgebraicGeometry.PrimeSpectrum.Top R)) :
                          M.tildeInModuleCat.stalk x ModuleCat.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
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[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))) :
                            (ModuleCat.Tilde.stalkToFiberLinearMap M x).hom ((M.tildeInModuleCat.germ U x hx).hom s) = s x, hx
                            @[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.forget (ModuleCat R)).obj (ModuleCat.of R M)) :
                            (M.tildeInModuleCat.germ U x hx) ((ModuleCat.Tilde.toOpen M U) x✝) = (ModuleCat.Tilde.toStalk M x) x✝
                            def ModuleCat.Tilde.const {R : Type u} [CommRing R] (M : ModuleCat R) (m : M) (r : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : xU, 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
                              @[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 : xU, r x.asIdeal.primeCompl) (x : U) :
                              (ModuleCat.Tilde.const M m r U hu) x = LocalizedModule.mk m r,
                              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 : xV, g x.asIdeal.primeCompl), ModuleCat.Tilde.const M f g V hg = (M.tildeInModuleCat.map i.op).hom s
                              @[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 : xU, g x.asIdeal.primeCompl) (V : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hv : xV, g x.asIdeal.primeCompl) (i : Opposite.op U Opposite.op V) :
                              (M.tildeInModuleCat.map i).hom (ModuleCat.Tilde.const M f g U hu) = ModuleCat.Tilde.const M f g V hv
                              @[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) :
                              (ModuleCat.Tilde.localizationToStalk M x).hom (LocalizedModule.mk f s) = (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen s) x ).hom (ModuleCat.Tilde.const M f (↑s) (PrimeSpectrum.basicOpen s) )
                              noncomputable def ModuleCat.Tilde.stalkIso {R : Type u} [CommRing R] (M : ModuleCat R) (x : (AlgebraicGeometry.PrimeSpectrum.Top R)) :
                              M.tildeInModuleCat.stalk x ModuleCat.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