English
Given a multilinear map on a sum of index sets, currySum produces a multilinear map whose domain splits into the left and right parts, taking values in a space of maps on one side with outputs in the other.
Русский
Для много-линейного отображения на сумме индексов currySum порождает отображение, чья область определения разбита на левую и правую части, принимающее значения в пространстве отображений слева с выводами на правую сторону.
LaTeX
$$$\\text{currySum}: \\operatorname{MultilinearMap} R (N) M_2 \\to \\operatorname{MultilinearMap} R (\\lambda i. N(\\mathrm{inl}\, i)) (\\operatorname{MultilinearMap} R (\\lambda i. N(\\mathrm{inr}\, i)) M_2)$$$
Lean4
/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map
on `(fun _ : ι ⊕ ι' => M')` induces a multilinear map on
`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))`. -/
def currySum (f : MultilinearMap R N M₂) :
MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)
where
toFun
u :=
{ toFun v := f (Sum.rec u v)
map_update_add' := by letI := Classical.decEq ι; aesop
map_update_smul' := by letI := Classical.decEq ι; aesop }
map_update_add' u i x y := ext fun _ ↦ by letI := Classical.decEq ι'; simp
map_update_smul' u i c x := ext fun _ ↦ by letI := Classical.decEq ι'; simp
