Finitely supported functions from the symmetric square

This file lifts functions α →₀ M₀ to functions Sym2 α →₀ M₀ by precomposing with multiplication.

theorem Finsupp.sym2_support_eq_preimage_support_mul {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] (f : α →₀ M₀) : ↑f.support.sym2 = Sym2.map ⇑f ⁻¹' Function.support Sym2.mul

theorem Finsupp.mem_sym2_support_of_mul_ne_zero {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] {f : α →₀ M₀} (p : Sym2 α) (hp : (Sym2.map (⇑f) p).mul ≠ 0) : p ∈ f.support.sym2

noncomputable def Finsupp.sym2Mul {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] (f : α →₀ M₀) : Sym2 α →₀ M₀

The composition of a Finsupp with Sym2.mul as a Finsupp.

Equations

• f.sym2Mul = Finsupp.onFinset f.support.sym2 (fun (p : Sym2 α) => (Sym2.map (⇑f) p).mul) ⋯

theorem Finsupp.support_sym2Mul_subset {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] {f : α →₀ M₀} : f.sym2Mul.support ⊆ f.support.sym2

@[simp]

theorem Finsupp.coe_sym2Mul {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] (f : α →₀ M₀) : ⇑f.sym2Mul = Sym2.mul ∘ Sym2.map ⇑f

theorem Finsupp.sym2Mul_apply_mk {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] {f : α →₀ M₀} (p : α × α) : f.sym2Mul (Sym2.mk p) = f p.1 * f p.2