English
There is a canonical additive equivalence between finitely supported functions on the disjoint sum α ⊕ β with values in a monoid M and the product of finitely supported functions on α and on β, respectively. This is the additive version of the standard sum-arrow equivalence.
Русский
Существует каноническая сумма-эквив между конечноподдерживаемыми функциямии на дизъюнктном сумме α ⊕ β со значениями в моноиде M и произведением функций на α и на β; это аддитивная версия стандартного эквивалента суммирования функций.
LaTeX
$$$(α ⊕ β →₀ M) \\simeq_+ (α →₀ M) × (β →₀ M)$$$
Lean4
/-- The additive equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`.
This is the `Finsupp` version of `Equiv.sum_arrow_equiv_prod_arrow`. -/
@[simps! apply symm_apply]
def sumFinsuppAddEquivProdFinsupp {α β : Type*} : (α ⊕ β →₀ M) ≃+ (α →₀ M) × (β →₀ M) :=
{ sumFinsuppEquivProdFinsupp with
map_add' := by
intros
ext <;>
simp only [Equiv.toFun_as_coe, Prod.fst_add, Prod.snd_add, add_apply, snd_sumFinsuppEquivProdFinsupp,
fst_sumFinsuppEquivProdFinsupp] }
