Tensor products of finitely supported functions

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

Main results

• ofDFinsuppEquiv: the linear equivalence between a PiTensorProduct of DFinsupps and the DFinsupp of the PiTensorProducts.

def PiTensorProduct.ofDFinsuppEquiv {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 ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] : (PiTensorProduct R fun (i : ι) => Π₀ (j : κ i), M i j) ≃ₗ[R] Π₀ (p : (i : ι) → κ i), PiTensorProduct R fun (i : ι) => M i (p i)

The ι-ary tensor product distributes over κ i-ary finitely supported functions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PiTensorProduct.ofDFinsuppEquiv_tprod_single {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 ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)) : ofDFinsuppEquiv ((tprod R) fun (i : ι) => DFinsupp.single (p i) (x i)) = DFinsupp.single p ((tprod R) fun (i : ι) => x i)

@[simp]

theorem PiTensorProduct.ofDFinsuppEquiv_symm_single_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 ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)) : ofDFinsuppEquiv.symm (DFinsupp.single p ((tprod R) x)) = (tprod R) fun (i : ι) => DFinsupp.single (p i) (x i)

@[simp]

theorem PiTensorProduct.ofDFinsuppEquiv_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)] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] (x : (i : ι) → Π₀ (j : κ i), M i j) (p : (i : ι) → κ i) : (ofDFinsuppEquiv ((tprod R) x)) p = (tprod R) fun (i : ι) => (x i) (p i)