# Tensor products of direct sums #

This file shows that taking TensorProducts commutes with taking DirectSums in both arguments.

## Main results #

• TensorProduct.directSum
• TensorProduct.directSumLeft
• TensorProduct.directSumRight
noncomputable def TensorProduct.directSum (R : Type u) [] (S : Type u_1) [] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [] [] (M₁ : ι₁Type w₁) (M₂ : ι₂Type w₂) [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] :
TensorProduct R (DirectSum ι₁ fun (i₁ : ι₁) => M₁ i₁) (DirectSum ι₂ fun (i₂ : ι₂) => M₂ i₂) ≃ₗ[S] DirectSum (ι₁ × ι₂) fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)

The linear equivalence (⨁ i₁, M₁ i₁) ⊗ (⨁ i₂, M₂ i₂) ≃ (⨁ i₁, ⨁ i₂, M₁ i₁ ⊗ M₂ i₂), i.e. "tensor product distributes over direct sum".

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def TensorProduct.directSumLeft (R : Type u) [] {ι₁ : Type v₁} [] (M₁ : ι₁Type w₁) (M₂' : Type w₂') [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] :
TensorProduct R (DirectSum ι₁ fun (i₁ : ι₁) => M₁ i₁) M₂' ≃ₗ[R] DirectSum ι₁ fun (i : ι₁) => TensorProduct R (M₁ i) M₂'

Tensor products distribute over a direct sum on the left .

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def TensorProduct.directSumRight (R : Type u) [] {ι₂ : Type v₂} [] (M₁' : Type w₁') (M₂ : ι₂Type w₂) [] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] :
TensorProduct R M₁' (DirectSum ι₂ fun (i : ι₂) => M₂ i) ≃ₗ[R] DirectSum ι₂ fun (i : ι₂) => TensorProduct R M₁' (M₂ i)

Tensor products distribute over a direct sum on the right.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TensorProduct.directSum_lof_tmul_lof (R : Type u) [] (S : Type u_1) [] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [] [] {M₁ : ι₁Type w₁} {M₂ : ι₂Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
(TensorProduct.directSum R S M₁ M₂) ((DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂) = (DirectSum.lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
@[simp]
theorem TensorProduct.directSum_symm_lof_tmul (R : Type u) [] (S : Type u_1) [] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [] [] {M₁ : ι₁Type w₁} {M₂ : ι₂Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
(TensorProduct.directSum R S M₁ M₂).symm ((DirectSum.lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) = (DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂
@[simp]
theorem TensorProduct.directSumLeft_tmul_lof (R : Type u) [] {ι₁ : Type v₁} [] {M₁ : ι₁Type w₁} {M₂' : Type w₂'} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
() ((DirectSum.lof R ι₁ M₁ i) x ⊗ₜ[R] y) = (DirectSum.lof R ι₁ (fun (i : ι₁) => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)
@[simp]
theorem TensorProduct.directSumLeft_symm_lof_tmul (R : Type u) [] {ι₁ : Type v₁} [] {M₁ : ι₁Type w₁} {M₂' : Type w₂'} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [] [(i₁ : ι₁) → Module R (M₁ i₁)] [Module R M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
().symm ((DirectSum.lof R ι₁ (fun (i : ι₁) => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)) = (DirectSum.lof R ι₁ M₁ i) x ⊗ₜ[R] y
@[simp]
theorem TensorProduct.directSumRight_tmul_lof (R : Type u) [] {ι₂ : Type v₂} [] {M₁' : Type w₁'} {M₂ : ι₂Type w₂} [] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
() (x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y) = (DirectSum.lof R ι₂ (fun (i : ι₂) => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)
@[simp]
theorem TensorProduct.directSumRight_symm_lof_tmul (R : Type u) [] {ι₂ : Type v₂} [] {M₁' : Type w₁'} {M₂ : ι₂Type w₂} [] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [Module R M₁'] [(i₂ : ι₂) → Module R (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
().symm ((DirectSum.lof R ι₂ (fun (i : ι₂) => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y