Documentation

LeanPool.Stafford38.AlgebraicAnalysis.Module.BaseLocalizationModuleComparison

Comparison of base and coefficient localizations #

For an R-algebra C, localizing a C-module at the image of a submonoid S ≤ R agrees with localizing it as an R-module at S.

source
def AlgebraicAnalysis.BaseLocalizationModuleComparison.coefficientDenominator {R : Type u_1} {C : Type u_2} [CommRing R] [CommRing C] [Algebra R C] (S : Submonoid R) (s : ↥S) :
↥(Algebra.algebraMapSubmonoid C S)

The coefficient-algebra denominator induced by a base denominator.

Equations
Instances For
    source
    theorem AlgebraicAnalysis.BaseLocalizationModuleComparison.instIsScalarTowerLocalizedModuleAlgebraMapSubmonoid_leanPool {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] (S : Submonoid R) :
    IsScalarTower R C (LocalizedModule (Algebra.algebraMapSubmonoid C S) E)
    source
    theorem AlgebraicAnalysis.BaseLocalizationModuleComparison.localizedModule_isLocalizedOverBase {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] (S : Submonoid R) :
    IsLocalizedModule S (↑R (LocalizedModule.mkLinearMap (Algebra.algebraMapSubmonoid C S) E))
    source
    theorem AlgebraicAnalysis.BaseLocalizationModuleComparison.localizedModule_isLocalizedOverCoefficient {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module C E] (S : Submonoid R) :
    IsLocalizedModule (Algebra.algebraMapSubmonoid C S) (LocalizedModule.mkLinearMap (Algebra.algebraMapSubmonoid C S) E)
    source
    @[instance_reducible]
    noncomputable def AlgebraicAnalysis.BaseLocalizationModuleComparison.localizedBaseModule {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module C E] (S : Submonoid R) :
    Module (Localization S) (LocalizedModule (Algebra.algebraMapSubmonoid C S) E)

    The localized coefficient module viewed over the base localization.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AlgebraicAnalysis.BaseLocalizationModuleComparison.instIsScalarTowerLocalizationLocalizedModuleAlgebraMapSubmonoid_leanPool {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] (S : Submonoid R) :
      IsScalarTower R (Localization S) (LocalizedModule (Algebra.algebraMapSubmonoid C S) E)
      source
      noncomputable def AlgebraicAnalysis.BaseLocalizationModuleComparison.localizedModuleComparison {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] (S : Submonoid R) :
      LocalizedModule S E ≃ₗ[Localization S] LocalizedModule (Algebra.algebraMapSubmonoid C S) E

      The canonical equivalence between base and coefficient localizations.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AlgebraicAnalysis.BaseLocalizationModuleComparison.localizedModuleComparison_mkLinearMap {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] (S : Submonoid R) (m : E) :
        (localizedModuleComparison S) ((LocalizedModule.mkLinearMap S E) m) = (LocalizedModule.mkLinearMap (Algebra.algebraMapSubmonoid C S) E) m
        source
        @[simp]
        theorem AlgebraicAnalysis.BaseLocalizationModuleComparison.localizedModuleComparison_mk {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] (S : Submonoid R) (m : E) (s : ↥S) :
        (localizedModuleComparison S) (LocalizedModule.mk m s) = LocalizedModule.mk m (coefficientDenominator S s)
        source
        theorem AlgebraicAnalysis.BaseLocalizationModuleComparison.localizedModuleComparison_natural {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] (S : Submonoid R) {F : Type u_4} [AddCommGroup F] [Module R F] [Module C F] [IsScalarTower R C F] (f : E →ₗ[C] F) (x : LocalizedModule S E) :
        (localizedModuleComparison S) (((LocalizedModule.map S) (↑R f)) x) = ((LocalizedModule.map (Algebra.algebraMapSubmonoid C S)) f) ((localizedModuleComparison S) x)