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.

@[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₂

instance IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1 {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M₁ : Type u_5) (M₂ : Type u_6) [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Module (Localization S) M₁] [Module (Localization S) M₂] [IsScalarTower R (Localization S) M₁] [IsScalarTower R (Localization S) M₂] : TensorProduct.CompatibleSMul R (Localization S) M₁ M₂

instance IsLocalization.instIsLocalizedModuleTensorProductMap {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (N : Type u_5) (N' : Type u_6) [AddCommMonoid N] [Module R N] [AddCommMonoid N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S f] [IsLocalizedModule S g] : IsLocalizedModule S (TensorProduct.map f g)

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.

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.

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.

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.

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_1) [CommSemiring R] (S : Submonoid R) (M : Type u_3) [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') {α : Type u_7} [IsLocalizedModule S f] : IsLocalizedModule S (Finsupp.mapRange.linearMap f)

theorem IsLocalizedModule.map_linearCombination {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') {α : Type u_7} {v : α → M} [IsLocalizedModule S f] : (map S (Finsupp.mapRange.linearMap (Algebra.linearMap R A)) f) (Finsupp.linearCombination R v) = ↑R (Finsupp.linearCombination A (⇑f ∘ v))

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, ⋯⟩

theorem IsLocalization.tensorProduct_tensorProduct (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 A) (B : Type u_10) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsLocalization M B] [Algebra (TensorProduct R A S) (TensorProduct R B S)] [IsScalarTower A (TensorProduct R A S) (TensorProduct R B S)] (H : (algebraMap (TensorProduct R A S) (TensorProduct R B S)).comp Algebra.TensorProduct.includeRight.toRingHom = Algebra.TensorProduct.includeRight.toRingHom) : IsLocalization (Algebra.algebraMapSubmonoid (TensorProduct R A S) M) (TensorProduct R B S)

A[M⁻¹] ⊗[R] S is the localization of A ⊗[R] S at M.

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ᵣ.

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ᵣ.