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 : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V U) (s : (M.tildeInModuleCat.obj (Opposite.op U))) (x : V) :
                  ((M.tildeInModuleCat.map i.op) 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