# mathlib3documentation

linear_algebra.direct_sum.tensor_product

# Tensor products of direct sums #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file shows that taking tensor_products commutes with taking direct_sums in both arguments.

## Main results #

• tensor_product.direct_sum
• tensor_product.direct_sum_left
• tensor_product.direct_sum_right
@[protected]
def tensor_product.direct_sum (R : Type u_1) [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] (M₁ : ι₁ Type u_4) (M₂ : ι₂ Type u_6) [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), (M₁ i₁)] [Π (i₂ : ι₂), (M₂ i₂)] :
(direct_sum ι₁ (λ (i₁ : ι₁), M₁ i₁)) (direct_sum ι₂ (λ (i₂ : ι₂), M₂ i₂)) ≃ₗ[R] direct_sum (ι₁ × ι₂) (λ (i : ι₁ × ι₂), (M₁ i.fst) (M₂ i.snd))

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

Equations
def tensor_product.direct_sum_left (R : Type u_1) [comm_ring R] {ι₁ : Type u_2} [decidable_eq ι₁] (M₁ : ι₁ Type u_4) (M₂' : Type u_7) [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [add_comm_group M₂'] [Π (i₁ : ι₁), (M₁ i₁)] [ M₂'] :
(direct_sum ι₁ (λ (i₁ : ι₁), M₁ i₁)) M₂' ≃ₗ[R] (λ (i : ι₁), (M₁ i) M₂')

Tensor products distribute over a direct sum on the left .

Equations
def tensor_product.direct_sum_right (R : Type u_1) [comm_ring R] {ι₂ : Type u_3} [decidable_eq ι₂] (M₁' : Type u_5) (M₂ : ι₂ Type u_6) [add_comm_group M₁'] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [ M₁'] [Π (i₂ : ι₂), (M₂ i₂)] :
M₁' (direct_sum ι₂ (λ (i : ι₂), M₂ i)) ≃ₗ[R] (λ (i : ι₂), M₁' (M₂ i))

Tensor products distribute over a direct sum on the right.

Equations
@[simp]
theorem tensor_product.direct_sum_lof_tmul_lof (R : Type u_1) [comm_ring R] {ι₁ : Type u_2} {ι₂ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] {M₁ : ι₁ Type u_4} {M₂ : ι₂ Type u_6} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), (M₁ i₁)] [Π (i₂ : ι₂), (M₂ i₂)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
M₂) ( ι₁ M₁ i₁) m₁ ⊗ₜ[R] ι₂ M₂ i₂) m₂) = (ι₁ × ι₂) (λ (i : ι₁ × ι₂), (M₁ i.fst) (M₂ i.snd)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
@[simp]
theorem tensor_product.direct_sum_left_tmul_lof (R : Type u_1) [comm_ring R] {ι₁ : Type u_2} [decidable_eq ι₁] {M₁ : ι₁ Type u_4} {M₂' : Type u_7} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [add_comm_group M₂'] [Π (i₁ : ι₁), (M₁ i₁)] [ M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
M₂') ( ι₁ (λ (i : ι₁), M₁ i) i) x ⊗ₜ[R] y) = ι₁ (λ (i : ι₁), (M₁ i) M₂') i) (x ⊗ₜ[R] y)
@[simp]
theorem tensor_product.direct_sum_left_symm_lof_tmul (R : Type u_1) [comm_ring R] {ι₁ : Type u_2} [decidable_eq ι₁] {M₁ : ι₁ Type u_4} {M₂' : Type u_7} [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [add_comm_group M₂'] [Π (i₁ : ι₁), (M₁ i₁)] [ M₂'] (i : ι₁) (x : M₁ i) (y : M₂') :
M₂').symm) ( ι₁ (λ (i : ι₁), (M₁ i) M₂') i) (x ⊗ₜ[R] y)) = ι₁ (λ (i : ι₁), M₁ i) i) x ⊗ₜ[R] y
@[simp]
theorem tensor_product.direct_sum_right_tmul_lof (R : Type u_1) [comm_ring R] {ι₂ : Type u_3} [decidable_eq ι₂] {M₁' : Type u_5} {M₂ : ι₂ Type u_6} [add_comm_group M₁'] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [ M₁'] [Π (i₂ : ι₂), (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
M₂) (x ⊗ₜ[R] ι₂ (λ (i : ι₂), M₂ i) i) y) = ι₂ (λ (i : ι₂), M₁' (M₂ i)) i) (x ⊗ₜ[R] y)
@[simp]
theorem tensor_product.direct_sum_right_symm_lof_tmul (R : Type u_1) [comm_ring R] {ι₂ : Type u_3} [decidable_eq ι₂] {M₁' : Type u_5} {M₂ : ι₂ Type u_6} [add_comm_group M₁'] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [ M₁'] [Π (i₂ : ι₂), (M₂ i₂)] (x : M₁') (i : ι₂) (y : M₂ i) :
M₂).symm) ( ι₂ (λ (i : ι₂), M₁' (M₂ i)) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] ι₂ (λ (i : ι₂), M₂ i) i) y