English
There is an equivalence between finsupps on the disjoint sum and a product of finsupps: (Finsupp (Sum α β) γ) ≃ (Finsupp α γ) × (Finsupp β γ).
Русский
Существует эквивалентность между конечноподдерживаемыми функциями на дизъюнктной сумме и произведением таких функций: Finsupp (Sum α β) γ ≃ Finsupp α γ × Finsupp β γ.
LaTeX
$$$\text{sumFinsuppEquivProdFinsupp} : Finsupp (Sum α β) γ \simeq (Finsupp α γ) \times (Finsupp β γ)$$$
Lean4
/-- The equivalence between `(α ⊕ β) →₀ γ` and `(α →₀ γ) × (β →₀ γ)`.
This is the `Finsupp` version of `Equiv.sum_arrow_equiv_prod_arrow`. -/
@[simps apply symm_apply]
def sumFinsuppEquivProdFinsupp {α β γ : Type*} [Zero γ] : (α ⊕ β →₀ γ) ≃ (α →₀ γ) × (β →₀ γ)
where
toFun f := ⟨f.comapDomain Sum.inl Sum.inl_injective.injOn, f.comapDomain Sum.inr Sum.inr_injective.injOn⟩
invFun fg := sumElim fg.1 fg.2
left_inv
f := by
ext ab
rcases ab with a | b <;> simp
right_inv fg := by ext <;> simp
