Results on finitely supported functions.

• ofFinsuppEquiv, the tensor product of the family κ i →₀ M i indexed by ι is linearly equivalent to ∏ i, κ i →₀ ⨂[R] i, M i.

noncomputable def PiTensorProduct.ofFinsuppEquiv {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → DecidableEq (M i)] : (PiTensorProduct R fun (i : ι) => κ i →₀ M i) ≃ₗ[R] ((i : ι) → κ i) →₀ PiTensorProduct R fun (i : ι) => M i

If ι is a Fintype, κ i is a family of types indexed by ι and M i is a family of modules indexed by ι, then the tensor product of the family κ i →₀ M i is linearly equivalent to ∏ i, κ i →₀ ⨂[R] i, M i.

@[simp]

theorem PiTensorProduct.ofFinsuppEquiv_tprod_single {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → DecidableEq (M i)] (p : (i : ι) → κ i) (m : (i : ι) → M i) : ofFinsuppEquiv ((tprod R) fun (i : ι) => fun₀ | p i => m i) = fun₀ | p => ⨂ₜ[R] (i : ι), m i

@[simp]

theorem PiTensorProduct.ofFinsuppEquiv_apply {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → DecidableEq (M i)] (f : (i : ι) → κ i →₀ M i) (p : (i : ι) → κ i) : (ofFinsuppEquiv ((tprod R) fun (i : ι) => f i)) p = ⨂ₜ[R] (i : ι), (f i) (p i)

@[simp]

theorem PiTensorProduct.ofFinsuppEquiv_symm_single_tprod {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → DecidableEq (M i)] (p : (i : ι) → κ i) (m : (i : ι) → M i) : (ofFinsuppEquiv.symm fun₀ | p => ⨂ₜ[R] (i : ι), m i) = (tprod R) fun (i : ι) => fun₀ | p i => m i

noncomputable def PiTensorProduct.ofFinsuppEquiv' {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [DecidableEq R] : (PiTensorProduct R fun (i : ι) => κ i →₀ R) ≃ₗ[R] ((i : ι) → κ i) →₀ R

A variant of ofFinsuppEquiv where all modules M i are the ground ring.

@[simp]

theorem PiTensorProduct.ofFinsuppEquiv'_apply_apply {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [DecidableEq R] (f : (i : ι) → κ i →₀ R) (p : (i : ι) → κ i) : (ofFinsuppEquiv' ((tprod R) fun (i : ι) => f i)) p = ∏ i : ι, (f i) (p i)

@[simp]

theorem PiTensorProduct.ofFinsuppEquiv'_tprod_single {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)] [DecidableEq R] (p : (i : ι) → κ i) (r : ι → R) : ofFinsuppEquiv' ((tprod R) fun (i : ι) => fun₀ | p i => r i) = fun₀ | p => ∏ i : ι, r i