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)
[CommRing 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)
[CommRing 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
Algebra.isPushout_of_isLocalization
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
(A : Type u_2)
[CommRing 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