Localized Module

Given a commutative semiring R, a multiplicative subset S ⊆ R and an R-module M, we can localize M by S. This gives us a Localization S-module.

Main definition

• isLocalizedModule_iff_isBaseChange : A localization of modules corresponds to a base change.

theorem IsLocalizedModule.isBaseChange {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : IsBaseChange A f

The forward direction of isLocalizedModule_iff_isBaseChange. It is also used to prove the other direction.

theorem isLocalizedModule_iff_isBaseChange {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') : IsLocalizedModule S f ↔ IsBaseChange A f

The map (f : M →ₗ[R] M') is a localization of modules iff the map (Localization S) × M → N, (s, m) ↦ s • f m is the tensor product (insomuch as it is the universal bilinear map). In particular, there is an isomorphism between LocalizedModule S M and (Localization S) ⊗[R] M given by m/s ↦ (1/s) ⊗ₜ m.

noncomputable def LocalizedModule.equivTensorProduct {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_3) [AddCommMonoid M] [Module R M] : LocalizedModule S M ≃ₗ[Localization S] TensorProduct R (Localization S) M

The localization of an R-module M at a submonoid S is isomorphic to S⁻¹R ⊗[R] M as an S⁻¹R-module.

Equations

• LocalizedModule.equivTensorProduct S M = ⋯.equiv.symm

@[simp]

theorem LocalizedModule.equivTensorProduct_symm_apply_tmul {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_3} [AddCommMonoid M] [Module R M] (x : M) (r : R) (s : ↥S) : (equivTensorProduct S M).symm (Localization.mk r s ⊗ₜ[R] x) = r • mk x s

@[simp]

theorem LocalizedModule.equivTensorProduct_symm_apply_tmul_one {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_3} [AddCommMonoid M] [Module R M] (x : M) : (equivTensorProduct S M).symm (1 ⊗ₜ[R] x) = mk x 1

@[simp]

theorem LocalizedModule.equivTensorProduct_apply_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_3} [AddCommMonoid M] [Module R M] (x : M) (s : ↥S) : (equivTensorProduct S M) (mk x s) = Localization.mk 1 s ⊗ₜ[R] x

instance IsLocalization.tensorProduct_isLocalizedModule {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_3} [AddCommMonoid M] [Module R M] : IsLocalizedModule S ((TensorProduct.mk R A M) 1)

theorem IsLocalization.tensorProduct_compatibleSMul {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (M₁ : Type u_5) (M₂ : Type u_6) [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Module A M₁] [Module A M₂] [IsScalarTower R A M₁] [IsScalarTower R A M₂] : TensorProduct.CompatibleSMul R A M₁ M₂

noncomputable def IsLocalization.moduleTensorEquiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (M₁ : Type u_5) (M₂ : Type u_6) [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Module A M₁] [Module A M₂] [IsScalarTower R A M₁] [IsScalarTower R A M₂] : TensorProduct A M₁ M₂ ≃ₗ[A] TensorProduct R M₁ M₂

If A is a localization of R, tensoring two A-modules over A is the same as tensoring them over R.

Equations

• IsLocalization.moduleTensorEquiv S A M₁ M₂ = TensorProduct.equivOfCompatibleSMul R A M₁ M₂

noncomputable def IsLocalization.moduleLid {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (M₁ : Type u_5) [AddCommMonoid M₁] [Module R M₁] [Module A M₁] [IsScalarTower R A M₁] : TensorProduct R A M₁ ≃ₗ[A] M₁

If A is a localization of R, tensoring an A-module with A over R does nothing.

Equations

• IsLocalization.moduleLid S A M₁ = (TensorProduct.equivOfCompatibleSMul R A A M₁).symm.trans (TensorProduct.lid A M₁)

noncomputable def IsLocalization.algebraTensorEquiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (B : Type u_5) (C : Type u_6) [Semiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Semiring C] [Algebra R C] [Algebra A C] [IsScalarTower R A C] : TensorProduct A B C ≃ₐ[A] TensorProduct R B C

If A is a localization of R, tensoring two A-algebras over A is the same as tensoring them over R.

Equations

• IsLocalization.algebraTensorEquiv S A B C = Algebra.TensorProduct.equivOfCompatibleSMul R A B C

noncomputable def IsLocalization.algebraLid {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (B : Type u_5) [Semiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] : TensorProduct R A B ≃ₐ[A] B

If A is a localization of R, tensoring an A-algebra with A over R does nothing.

Equations

• IsLocalization.algebraLid S A B = Algebra.TensorProduct.lidOfCompatibleSMul R A B

theorem IsLocalization.bijective_linearMap_mul' {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] : Function.Bijective ⇑(LinearMap.mul' R A)

theorem Algebra.isLocalization_iff_isPushout {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] {T : Type u_5} {B : Type u_6} [CommSemiring T] [CommSemiring B] [Algebra R T] [Algebra T B] [Algebra R B] [Algebra A B] [IsScalarTower R T B] [IsScalarTower R A B] : IsLocalization (algebraMapSubmonoid T S) B ↔ IsPushout R T A B

theorem Algebra.isPushout_of_isLocalization {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (T : Type u_5) (B : Type u_6) [CommSemiring T] [CommSemiring B] [Algebra R T] [Algebra T B] [Algebra R B] [Algebra A B] [IsScalarTower R T B] [IsScalarTower R A B] [IsLocalization (algebraMapSubmonoid T S) B] : IsPushout R T A B

instance instIsLocalizedModuleFinsuppLinearMap (R : Type u_7) (M : Type u_8) [CommRing R] [AddCommGroup M] [Module R M] {α : Type u_9} (S : Submonoid R) {Mₛ : Type u_10} [AddCommGroup Mₛ] [Module R Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] : IsLocalizedModule S (Finsupp.mapRange.linearMap f)

instance IsLocalizedModule.rTensor {R : Type u_1} [CommSemiring R] (A : Type u_2) [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (S : Submonoid A) {N : Type u_7} [AddCommMonoid N] [Module R N] [Module A M] [IsScalarTower R A M] (g : M →ₗ[A] M') [h : IsLocalizedModule S g] : IsLocalizedModule S ((TensorProduct.AlgebraTensorModule.rTensor R N) g)

S⁻¹M ⊗[R] N = S⁻¹(M ⊗[R] N).

theorem IsLocalizedModule.map_lTensor {R : Type u_1} [CommSemiring R] (A : Type u_2) [CommSemiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] (S : Submonoid A) {N : Type u_7} [AddCommMonoid N] [Module R N] [Module A M] [IsScalarTower R A M] {P : Type u_8} [AddCommMonoid P] [Module R P] (f : N →ₗ[R] P) (g : M →ₗ[A] M') [h : IsLocalizedModule S g] : (map S ((TensorProduct.AlgebraTensorModule.rTensor R N) g) ((TensorProduct.AlgebraTensorModule.rTensor R P) g)) ((TensorProduct.AlgebraTensorModule.lTensor A M) f) = (TensorProduct.AlgebraTensorModule.lTensor A M') f

instance IsLocalization.tensor {R : Type u_7} {S : Type u_8} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_9) [CommSemiring A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] : IsLocalization (Algebra.algebraMapSubmonoid S M) (TensorProduct R S A)

instance IsLocalization.tensorRight {R : Type u_7} {S : Type u_8} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_9) [CommSemiring A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] : IsLocalization (Algebra.algebraMapSubmonoid S M) (TensorProduct R A S)

theorem IsLocalization.tmul_mk' {R : Type u_7} {S : Type u_8} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_9) [CommSemiring A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] (s : S) (x : R) (y : ↥M) : s ⊗ₜ[R] mk' A x y = mk' (TensorProduct R S A) ((algebraMap R S) x * s) ⟨(algebraMap R S) ↑y, ⋯⟩

theorem IsLocalization.mk'_tmul {R : Type u_7} {S : Type u_8} [CommSemiring R] [CommSemiring S] [Algebra R S] (A : Type u_9) [CommSemiring A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] (s : S) (x : R) (y : ↥M) : mk' A x y ⊗ₜ[R] s = mk' (TensorProduct R A S) ((algebraMap R S) x * s) ⟨(algebraMap R S) ↑y, ⋯⟩

instance IsLocalization.Away.tensor {R : Type u_7} {S : Type u_8} [CommSemiring R] [CommSemiring S] [Algebra R S] (r : R) (A : Type u_9) [CommSemiring A] [Algebra R A] [Away r A] : Away ((algebraMap R S) r) (TensorProduct R S A)

@[reducible, inline]

noncomputable abbrev IsLocalization.Away.tensorEquiv {R : Type u_7} (S : Type u_8) [CommSemiring R] [CommSemiring S] [Algebra R S] (r : R) (A : Type u_9) [CommSemiring A] [Algebra R A] [Away r A] : TensorProduct R S A ≃ₐ[S] Localization.Away ((algebraMap R S) r)

The S-isomorphism S ⊗[R] Rᵣ ≃ₐ Sᵣ.

Equations

• IsLocalization.Away.tensorEquiv S r A = IsLocalization.algEquiv (Submonoid.powers ((algebraMap R S) r)) (TensorProduct R S A) (Localization.Away ((algebraMap R S) r))

instance IsLocalization.Away.tensorRight {R : Type u_7} {S : Type u_8} [CommSemiring R] [CommSemiring S] [Algebra R S] (r : R) (A : Type u_9) [CommSemiring A] [Algebra R A] [Away r A] : Away ((algebraMap R S) r) (TensorProduct R A S)

@[reducible, inline]

noncomputable abbrev IsLocalization.Away.tensorRightEquiv {R : Type u_7} (S : Type u_8) [CommSemiring R] [CommSemiring S] [Algebra R S] (r : R) (A : Type u_9) [CommSemiring A] [Algebra R A] [Away r A] : TensorProduct R A S ≃ₐ[S] Localization.Away ((algebraMap R S) r)

The S-isomorphism S ⊗[R] Rᵣ ≃ₐ Sᵣ.

Equations

• IsLocalization.Away.tensorRightEquiv S r A = IsLocalization.algEquiv (Submonoid.powers ((algebraMap R S) r)) (TensorProduct R A S) (Localization.Away ((algebraMap R S) r))