English
There is a linear equivalence between multilinear maps in n+1 variables and linear maps in the p-th variable with values in multilinear maps of the rest.
Русский
Существует линейное эквивалентное отображение между много-линейными отображениями в n+1 переменных и линейными отображениями по p-й переменной со значениями в много-линейные отображения по остальным переменным.
LaTeX
$$$\\text{curryMidLinearEquiv}(p): \\operatorname{MultilinearMap} R M M_2 \\simeq_{} \\_L \\operatorname{MplMap} R (\\lambda i. M (p.succAbove i)) M_2$$$
Lean4
/-- `MultilinearMap.curryMid` as a linear equivalence. -/
@[simps]
def curryMidLinearEquiv (p : Fin (n + 1)) :
MultilinearMap R M M₂ ≃ₗ[R] M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
where
toFun := MultilinearMap.curryMid p
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun := LinearMap.uncurryMid p
left_inv := MultilinearMap.uncurryMid_curryMid p
right_inv := LinearMap.curryMid_uncurryMid p
