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.tensorSelfAlgEquiv
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
(A : Type u_2)
[CommSemiring A]
[Algebra R A]
[IsLocalization S A]
:
TensorProduct R A A ≃ₐ[A] A
If A is a localization of a commutative ring R, the tensor product of A with A over R is canonically isomorphic as A-algebras to A itself.
Equations
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]
:
Equations
- ⋯ = ⋯