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.

Equations

• PiTensorProduct.ofFinsuppEquiv = ((PiTensorProduct.congr fun (x : ι) => finsuppLequivDFinsupp R).trans PiTensorProduct.ofDFinsuppEquiv).trans (finsuppLequivDFinsupp R).symm

@[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 : ι) => Finsupp.single (p i) (m i)) = Finsupp.single 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 (Finsupp.single p (⨂ₜ[R] (i : ι), m i)) = (tprod R) fun (i : ι) => Finsupp.single (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.

Equations

• PiTensorProduct.ofFinsuppEquiv' = PiTensorProduct.ofFinsuppEquiv.trans (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) ↑(PiTensorProduct.constantBaseRingEquiv ι R))

@[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 : ι) => Finsupp.single (p i) (r i)) = Finsupp.single p (∏ i : ι, r i)