Decomposition of tensor product #
In this file, we describe the properties of decomposition under tensor product. Suppose ℳ is a
decomposition of an R-module M indexed by a type ι. Given an R-module N, the R-module
M ⊗[R] N has a decomposition into pieces fun i ↦ (ℳ i) ⊗[R] N. Given a commutative R-algebra
S, the S-module S ⊗[R] M has a decomposition fun i ↦ (ℳ i).baseChange S.
@[instance_reducible]
instance
DirectSum.Decomposition.baseChange
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[Decomposition ℳ]
[CommSemiring S]
[Algebra R S]
:
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}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[Decomposition ℳ]
[CommSemiring S]
[Algebra R S]
(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}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[Decomposition ℳ]
[CommSemiring S]
[Algebra R S]
(i : ι)
:
Function.Bijective ⇑(Submodule.toBaseChange S (ℳ i))
def
DirectSum.decomposeTensor
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
(i : ι)
:
Submodule R (TensorProduct R M N)
The submodule of a tensor product corresponding to a decomposition on the left.
Equations
- DirectSum.decomposeTensor ℳ N i = (LinearMap.rTensor N (ℳ i).subtype).range
Instances For
theorem
DirectSum.decomposeTensor_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
{i : ι}
:
theorem
DirectSum.subtype_rTensor_injective
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
[DecidableEq ι]
[Decomposition ℳ]
(i : ι)
:
Function.Injective ⇑(LinearMap.rTensor N (ℳ i).subtype)
noncomputable def
DirectSum.decomposeTensorEquiv
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
[DecidableEq ι]
[Decomposition ℳ]
(i : ι)
:
The linear isomorphism to the submodule from the tensor product with a summand.
Equations
- DirectSum.decomposeTensorEquiv ℳ N i = LinearEquiv.ofInjective (LinearMap.rTensor N (ℳ i).subtype) ⋯
Instances For
theorem
DirectSum.decomposeTensorEquiv_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
[DecidableEq ι]
[Decomposition ℳ]
{i : ι}
(x : TensorProduct R (↥(ℳ i)) N)
:
@[simp]
theorem
DirectSum.val_decomposeTensorEquiv_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
[DecidableEq ι]
[Decomposition ℳ]
{i : ι}
(x : TensorProduct R (↥(ℳ i)) N)
:
theorem
DirectSum.decomposeTensorEquiv_of_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
[DecidableEq ι]
[Decomposition ℳ]
{i : ι}
(x : TensorProduct R (↥(ℳ i)) N)
:
(congrLinearEquiv fun (i : ι) => decomposeTensorEquiv ℳ N i) ((of (fun (i : ι) => TensorProduct R (↥(ℳ i)) N) i) x) = (of (fun (i : ι) => ↥(decomposeTensor ℳ N i)) i) ((decomposeTensorEquiv ℳ N i) x)
theorem
DirectSum.decomposeLinearEquiv_comp_subtype
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[Decomposition ℳ]
{i : ι}
:
theorem
DirectSum.coe_decomposeTensor_apply
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
(N : Type u_5)
[AddCommMonoid N]
[Module R N]
[DecidableEq ι]
[Decomposition ℳ]
(x : DirectSum ι fun (i : ι) => ↥(decomposeTensor ℳ N i))
:
(DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) x = (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ).symm)
((TensorProduct.directSumLeft R R (fun (i : ι) => ↥(ℳ i)) N).symm
((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm x))
@[reducible]
noncomputable def
DirectSum.tensorDecomposition
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[Decomposition ℳ]
(N : Type u_6)
[AddCommGroup N]
[Module R N]
:
Decomposition (decomposeTensor ℳ N)
The decomposition of a tensor product induced by a decomposition of the left module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
DirectSum.IsInternal.baseChange
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{S : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[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}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[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}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(ℳ : ι → Submodule R M)
[DecidableEq ι]
[CommSemiring S]
[Algebra R S]
(hm : IsInternal ℳ)
(i : ι)
:
Function.Injective ⇑(Submodule.toBaseChange S (ℳ i))