Tensor products of direct sums #

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

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_5) [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] :

((⨁ (i₁ : ι₁), M₁ i₁) ⊗ ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[R] ⨁ (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

tensor_product.direct_sum R ι₁ ι₂ M₁ M₂ = linear_equiv.of_linear (tensor_product.lift (direct_sum.to_module R ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗ M₂ i.snd) (λ (i₁ : ι₁), (direct_sum.to_module R ι₂ (M₁ i₁ →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.fst ⊗ M₂ i.snd) (λ (i₂ : ι₂), (tensor_product.curry (direct_sum.lof R (ι₁ × ι₂) (λ (i : ι₁ × ι₂), M₁ i.fst ⊗ M₂ i.snd) (i₁, i₂))).flip)).flip))) (direct_sum.to_module R (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗ ⨁ (i₂ : ι₂), M₂ i₂) (λ (i : ι₁ × ι₂), tensor_product.map (direct_sum.lof R ι₁ M₁ i.fst) (direct_sum.lof R ι₂ M₂ i.snd))) _ _

source

@[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_5) [Π (i₁ : ι₁), add_comm_group (M₁ i₁)] [Π (i₂ : ι₂), add_comm_group (M₂ i₂)] [Π (i₁ : ι₁), module R (M₁ i₁)] [Π (i₂ : ι₂), module R (M₂ i₂)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :

⇑(tensor_product.direct_sum R ι₁ ι₂ M₁ M₂) (⇑(direct_sum.lof R ι₁ M₁ i₁) m₁ ⊗ₜ[R] ⇑(direct_sum.lof R ι₂ M₂ i₂) m₂) = ⇑(direct_sum.lof R (ι₁ × ι₂) (λ (i : ι₁ × ι₂), M₁ i.fst ⊗ M₂ i.snd) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)