English
There is a construction that, given a linear map from the p-th component into the space of multilinear maps on the remaining components, yields a multilinear map on all components.
Русский
Существует конструкция, которая из линейного отображения из p-й компоненты в пространство много-линейных отображений по прочим компонентам строит много-линейное отображение на все компоненты.
LaTeX
$$$\\text{uncurryMid} : M_p \\to_\\!R \\operatorname{MultilinearMap} R (\\lambda i. M (p.succAbove i)) M_2 \\to \\operatorname{MultilinearMap} R M M_2$ and its defining formula: $(\\text{uncurryMid}(p,f))(m) = f(m(p))(p.removeNth(m))$$$
Lean4
/-- Given a linear map from `M p` to the space of multilinear maps
in `n` variables `M 0`, ..., `M n` with `M p` removed,
returns a multilinear map in all `n + 1` variables. -/
@[simps!]
def uncurryMid (p : Fin (n + 1)) (f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂) :
MultilinearMap R M M₂ :=
.mk' (fun m ↦ f (m p) (p.removeNth m)) (fun m i x y ↦ by cases i using Fin.succAboveCases p <;> simp)
(fun m i x y ↦ by cases i using Fin.succAboveCases p <;> simp)
