Decomposition of tensor product #
In this file we show that if ℳ is a decomposition of an R-module M indexed by a type ι,
then the S-module S ⊗[R] M has a decomposition fun i ↦ (ℳ i).baseChange S indexed by the
same ι.
@[implicit_reducible]
instance
DirectSum.Decomposition.baseChange
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[DecidableEq ι]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[CommSemiring S]
[Algebra R S]
[Decomposition ℳ]
:
Decomposition fun (i : ι) => Submodule.baseChange S (ℳ i)
Equations
- One or more equations did not get rendered due to their size.
theorem
DirectSum.toBaseChange_injective
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[DecidableEq ι]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[CommSemiring S]
[Algebra R S]
[Decomposition ℳ]
(i : ι)
:
Function.Injective ⇑(Submodule.toBaseChange S (ℳ i))
theorem
DirectSum.toBaseChange_bijective
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[DecidableEq ι]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[CommSemiring S]
[Algebra R S]
[Decomposition ℳ]
(i : ι)
:
Function.Bijective ⇑(Submodule.toBaseChange S (ℳ i))
theorem
DirectSum.IsInternal.baseChange
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[DecidableEq ι]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[CommSemiring S]
[Algebra R S]
(hm : IsInternal ℳ)
:
IsInternal fun (i : ι) => Submodule.baseChange S (ℳ i)
theorem
DirectSum.IsInternal.toBaseChange_bijective
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[DecidableEq ι]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[CommSemiring S]
[Algebra R S]
(hm : IsInternal ℳ)
(i : ι)
:
Function.Bijective ⇑(Submodule.toBaseChange S (ℳ i))
theorem
DirectSum.IsInternal.toBaseChange_injective
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[DecidableEq ι]
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[CommSemiring S]
[Algebra R S]
(hm : IsInternal ℳ)
(i : ι)
:
Function.Injective ⇑(Submodule.toBaseChange S (ℳ i))