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.
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₂
Instances For
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₁)
Instances For
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
Instances For
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
Instances For
@[deprecated IsLocalization.algebraLid]
def
IsLocalization.tensorSelfAlgEquiv
{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
Alias of IsLocalization.algebraLid.
If A is a localization of R, tensoring an A-algebra with A over R does nothing.
Instances For
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.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 (Algebra.algebraMapSubmonoid T S) B]
:
Algebra.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]
:
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]
:
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]
:
(IsLocalizedModule.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