English
There is a linear map sigmaLuncurry which is the inverse of sigmaLcurry, sending the nested direct sum back to the single direct sum over pairs, so that the coefficient at ⟨i, j⟩ is preserved as f i j.
Русский
Существует линейное отображение sigmaLuncurry, являющееся об inversе sigmaLcurry, переводя вложенную прямую сумму обратно в прямую сумму по парам, сохраняющее коэффициент при ⟨i, j⟩: он равен f i j.
LaTeX
$$$\sigma_{\mathrm{Luncurry}} : (\bigoplus_{i} \bigoplus_{j} \delta(i,j)) \to_\!R (\bigoplus_{(i,j)} \delta(i,j)).$ \\ (\sigma_{\mathrm{Luncurry}} f) \langle i,j \rangle = f \, i \, j.$$$
Lean4
/-- `uncurry` as a linear map. -/
def sigmaLuncurry : (⨁ (i) (j), δ i j) →ₗ[R] ⨁ i : Σ _, _, δ i.1 i.2 :=
{ sigmaUncurry with map_smul' := DFinsupp.sigmaUncurry_smul }
