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')
:
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]
:
The localization of an R-module M at a submonoid S is isomorphic to S⁻¹R ⊗[R] M as
an S⁻¹R-module.
Equations
Instances For
@[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)
:
@[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)
:
@[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)
:
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₂]
:
If A is a localization of R, tensoring two A-modules over A is the same as
tensoring them over R.
Equations
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₁]
:
If A is a localization of R, tensoring an A-module with A over R does nothing.
Equations
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]
:
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]
:
If A is a localization of R, tensoring an A-algebra with A over R does nothing.
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.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]
:
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]
:
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]
:
(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}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Type u_9)
[CommRing 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}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Type u_9)
[CommRing A]
[Algebra R A]
(M : Submonoid R)
[IsLocalization M A]
:
IsLocalization (Algebra.algebraMapSubmonoid S M) (TensorProduct R A S)
instance
IsLocalization.Away.tensor
{R : Type u_7}
{S : Type u_8}
[CommRing R]
[CommRing S]
[Algebra R S]
(r : R)
(A : Type u_9)
[CommRing A]
[Algebra R A]
[Away r A]
:
Away ((algebraMap R S) r) (TensorProduct R S A)
instance
IsLocalization.Away.tensorRight
{R : Type u_7}
{S : Type u_8}
[CommRing R]
[CommRing S]
[Algebra R S]
(r : R)
(A : Type u_9)
[CommRing A]
[Algebra R A]
[Away r A]
:
Away ((algebraMap R S) r) (TensorProduct R A S)