Tensor products of direct sums

This file shows that taking PiTensorProducts commutes with taking DirectSums in all arguments.

Main results

• ofDirectSumEquiv: the linear equivalence between a PiTensorProduct of DirectSums and the DirectSum of the PiTensorProducts.

noncomputable def PiTensorProduct.ofDirectSumEquiv {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Finite ι] : (PiTensorProduct R fun (i : ι) => DirectSum (κ i) fun (j : κ i) => M i j) ≃ₗ[R] DirectSum ((i : ι) → κ i) fun (p : (i : ι) → κ i) => PiTensorProduct R fun (i : ι) => M i (p i)

The n-ary tensor product distributes over m-ary direct sums.

Equations

• PiTensorProduct.ofDirectSumEquiv = PiTensorProduct.ofDFinsuppEquiv

@[simp]

theorem PiTensorProduct.ofDirectSumEquiv_tprod_lof {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Fintype ι] [(i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)) : ofDirectSumEquiv ((tprod R) fun (i : ι) => (DirectSum.lof R (κ i) (M i) (p i)) (x i)) = (DirectSum.lof R ((i : ι) → κ i) (fun (i : (i : ι) → κ i) => PiTensorProduct R fun (i_1 : ι) => M i_1 (i i_1)) p) ((tprod R) fun (i : ι) => x i)

@[simp]

theorem PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Fintype ι] [(i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)) : ofDirectSumEquiv.symm ((DirectSum.lof R ((i : ι) → κ i) (fun (p : (i : ι) → κ i) => PiTensorProduct R fun (i : ι) => M i (p i)) p) ((tprod R) x)) = (tprod R) fun (i : ι) => (DirectSum.lof R (κ i) (M i) (p i)) (x i)

@[simp]

theorem PiTensorProduct.ofDirectSumEquiv_tprod_apply {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [CommSemiring R] [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] [(i : ι) → (j : κ i) → Module R (M i j)] [Finite ι] (x : (i : ι) → DirectSum (κ i) fun (j : κ i) => M i j) (p : (i : ι) → κ i) : (ofDirectSumEquiv ((tprod R) x)) p = (tprod R) fun (i : ι) => (x i) (p i)