English
There is a canonical linear isomorphism between the space of multilinear maps on n+1 variables and the space of linear maps from multilinear maps on the first n variables into linear maps on the last variable. This is realized by separating the last variable (multilinearCurryRightEquiv).
Русский
Существует каноническое линейное изоморфизм между пространством многолинейных отображений в n+1 переменных и пространством линейных отображений от многолинейных отображений в первых n переменных к линейным отображениям на последнюю переменную. Это реализовано через разделение последней переменной (multilinearCurryRightEquiv).
LaTeX
$$$ \\operatorname{MultilinearMap} R M M_2 \\cong_L [R] \\operatorname{MultilinearMap} R (\\lambda i. M (p.succAbove i)) (M (\\text{last } n) \\to_\\!R M_2) $$$
Lean4
/-- The space of multilinear maps on `Π (i : Fin (n+1)), M i` is canonically isomorphic to
the space of linear maps from the space of multilinear maps on `Π (i : Fin n), M (castSucc i)` to
the space of linear maps on `M (last n)`, by separating the last variable. We register this
isomorphism as a linear isomorphism in `multilinearCurryRightEquiv R M M₂`.
The direct and inverse maps are given by `f.curryRight` and `f.uncurryRight`. Use these
unless you need the full framework of linear equivs. -/
def multilinearCurryRightEquiv :
MultilinearMap R M M₂ ≃ₗ[R] MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)
where
toFun := MultilinearMap.curryRight
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun := MultilinearMap.uncurryRight
left_inv := MultilinearMap.uncurry_curryRight
right_inv := MultilinearMap.curry_uncurryRight
