English
Suppose you have a family of modules δ indexed by pairs (i, j) with i in ι and j in α_i. The operation sigmaLcurry is a linear map that reorganizes the direct sum from a single-indexed sum over (i, j) into a nested sum over i and then j, yielding δ(i, j).
Русский
Пусть имеется семейство модулей δ(i, j) индексируемое парами (i, j). Операция sigmaLcurry образует линейное отображение, переводя прямую сумму по парам в вложенную прямую сумму по i затем по j, возвращая δ(i, j).
LaTeX
$$$\sigma_{\mathrm{Lcurry}} : (\bigoplus_{(i, j)} \delta(i, j)) \to_\!R (\bigoplus_{i} \bigoplus_{j} \delta(i, j)).$$$
Lean4
/-- `curry` as a linear map. -/
def sigmaLcurry : (⨁ i : Σ _, _, δ i.1 i.2) →ₗ[R] ⨁ (i) (j), δ i j :=
{ sigmaCurry with map_smul' := fun r ↦ by convert DFinsupp.sigmaCurry_smul (δ := δ) r }
