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 #
@[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₁ : ι₁), module R (M₁ i₁)]
[Π (i₂ : ι₂), module R (M₂ i₂)] :
tensor_product R (direct_sum ι₁ (λ (i₁ : ι₁), M₁ i₁)) (direct_sum ι₂ (λ (i₂ : ι₂), M₂ i₂)) ≃ₗ[R] direct_sum (ι₁ × ι₂) (λ (i : ι₁ × ι₂), tensor_product R (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 ι₁ (direct_sum ι₂ (λ (i₂ : ι₂), M₂ i₂) →ₗ[R] direct_sum (ι₁ × ι₂) (λ (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd))) (λ (i₁ : ι₁), (direct_sum.to_module R ι₂ (M₁ i₁ →ₗ[R] direct_sum (ι₁ × ι₂) (λ (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd))) (λ (i₂ : ι₂), (tensor_product.curry (direct_sum.lof R (ι₁ × ι₂) (λ (i : ι₁ × ι₂), tensor_product R (M₁ i.fst) (M₂ i.snd)) (i₁, i₂))).flip)).flip))) (direct_sum.to_module R (ι₁ × ι₂) (tensor_product R (direct_sum ι₁ (λ (i₁ : ι₁), M₁ i₁)) (direct_sum ι₂ (λ (i₂ : ι₂), M₂ i₂))) (λ (i : ι₁ × ι₂), tensor_product.map (direct_sum.lof R ι₁ M₁ i.fst) (direct_sum.lof R ι₂ M₂ i.snd))) _ _
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₁ : ι₁), module R (M₁ i₁)]
[module R M₂'] :
tensor_product R (direct_sum ι₁ (λ (i₁ : ι₁), M₁ i₁)) M₂' ≃ₗ[R] direct_sum ι₁ (λ (i : ι₁), tensor_product R (M₁ i) M₂')
Tensor products distribute over a direct sum on the left .
Equations
- tensor_product.direct_sum_left R M₁ M₂' = linear_equiv.of_linear (tensor_product.lift (direct_sum.to_module R ι₁ (M₂' →ₗ[R] direct_sum ι₁ (λ (i : ι₁), tensor_product R (M₁ i) M₂')) (λ (i : ι₁), (tensor_product.mk R (M₁ i) M₂').compr₂ (direct_sum.lof R ι₁ (λ (i : ι₁), tensor_product R (M₁ i) M₂') i)))) (direct_sum.to_module R ι₁ (tensor_product R (direct_sum ι₁ (λ (i₁ : ι₁), M₁ i₁)) M₂') (λ (i : ι₁), linear_map.rtensor M₂' (direct_sum.lof R ι₁ M₁ i))) _ _
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₂)]
[module R M₁']
[Π (i₂ : ι₂), module R (M₂ i₂)] :
tensor_product R M₁' (direct_sum ι₂ (λ (i : ι₂), M₂ i)) ≃ₗ[R] direct_sum ι₂ (λ (i : ι₂), tensor_product R M₁' (M₂ i))
Tensor products distribute over a direct sum on the right.
Equations
- tensor_product.direct_sum_right R M₁' M₂ = ((tensor_product.comm R M₁' (direct_sum ι₂ (λ (i₁ : ι₂), M₂ i₁))).trans (tensor_product.direct_sum_left R M₂ M₁')).trans (dfinsupp.map_range.linear_equiv (λ (i : ι₂), tensor_product.comm R (M₂ i) M₁'))
@[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₁ : ι₁), 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 : ι₁ × ι₂), tensor_product R (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₁ : ι₁), module R (M₁ i₁)]
[module R M₂']
(i : ι₁)
(x : M₁ i)
(y : M₂') :
⇑(tensor_product.direct_sum_left R M₁ M₂') (⇑(direct_sum.lof R ι₁ (λ (i : ι₁), M₁ i) i) x ⊗ₜ[R] y) = ⇑(direct_sum.lof R ι₁ (λ (i : ι₁), tensor_product R (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₁ : ι₁), module R (M₁ i₁)]
[module R M₂']
(i : ι₁)
(x : M₁ i)
(y : M₂') :
⇑((tensor_product.direct_sum_left R M₁ M₂').symm) (⇑(direct_sum.lof R ι₁ (λ (i : ι₁), tensor_product R (M₁ i) M₂') i) (x ⊗ₜ[R] y)) = ⇑(direct_sum.lof R ι₁ (λ (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₂)]
[module R M₁']
[Π (i₂ : ι₂), module R (M₂ i₂)]
(x : M₁')
(i : ι₂)
(y : M₂ i) :
⇑(tensor_product.direct_sum_right R M₁' M₂) (x ⊗ₜ[R] ⇑(direct_sum.lof R ι₂ (λ (i : ι₂), M₂ i) i) y) = ⇑(direct_sum.lof R ι₂ (λ (i : ι₂), tensor_product R 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₂)]
[module R M₁']
[Π (i₂ : ι₂), module R (M₂ i₂)]
(x : M₁')
(i : ι₂)
(y : M₂ i) :
⇑((tensor_product.direct_sum_right R M₁' M₂).symm) (⇑(direct_sum.lof R ι₂ (λ (i : ι₂), tensor_product R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] ⇑(direct_sum.lof R ι₂ (λ (i : ι₂), M₂ i) i) y