English
There is a linear equivalence between the space of multilinear maps on Fin(n+1) and the space of linear maps from multilinear maps on Fin n to linear maps on M(last n).
Русский
Существет линейное эквивалентное отображение между пространством много-линейных отображений на Fin(n+1) и пространством линейных отображений из много-линейных отображений на Fin n в линейные отображения на M(last n).
LaTeX
$$$\\text{multilinearCurryRightEquiv}: \\operatorname{MultilinearMap} R M M_2 \\simeq_L \\operatorname{MultilinearMap} R (\\lambda i. M (p.succAbove i)) (M (\\text{last } n) \\to_\\!R M_2)$$$
Lean4
/-- Interpret a multilinear map in `n + 1` variables
as a linear map in `p`th variable with values in the multilinear maps in the other variables. -/
@[simps!]
def curryMid (p : Fin (n + 1)) (f : MultilinearMap R M M₂) : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
where
toFun x := .mk' fun m ↦ f (p.insertNth x m)
map_add' x y := by ext; simp [map_insertNth_add]
map_smul' c x := by ext; simp [map_insertNth_smul]
