Tensor products of internal decompositions #
If M and N are internal direct sums of families of submodules A i and B j, then
M ⊗ N is the internal direct sum of the images A i ⊗ B j. Mathlib supplies the external
tensor-product/direct-sum equivalence and the decomposition obtained from one decomposed factor;
this file records the symmetric two-factor consequence for internal decompositions.
Main result #
DirectSum.IsInternal.tensorProduct: the images of the tensor products of the summands form an internal decomposition of the ambient tensor product.
theorem
DirectSum.IsInternal.tensorProduct
{K : Type u}
[CommSemiring K]
{M : Type v}
{N : Type w}
[AddCommMonoid M]
[Module K M]
[AddCommMonoid N]
[Module K N]
{ι : Type x}
{κ : Type y}
(A : ι → Submodule K M)
(B : κ → Submodule K N)
(hA : IsInternal A)
(hB : IsInternal B)
:
IsInternal fun (p : ι × κ) => Submodule.map₂ (TensorProduct.mk K M N) (A p.1) (B p.2)
Tensor products of internal decompositions are internal. If A and B internally
decompose M and N, the images of A i ⊗ B j under the canonical map internally decompose
M ⊗ N.
The summand is written with Submodule.map₂ because this is the canonical submodule of the
ambient tensor product spanned by pure tensors from the two factors.