English
The two-step process of uncurryLeft then curryLeft is the identity on Linear maps.
Русский
Два шага: uncurryLeft затем curryLeft — тождественный переход на линейных отображениях.
LaTeX
$$$$f.uncurryLeft.curryLeft = f.$$$$
Lean4
/-- The space of multilinear maps on `Π (i : Fin (n+1)), M i` is canonically isomorphic to
the space of linear maps from `M 0` to the space of multilinear maps on
`Π (i : Fin n), M i.succ`, by separating the first variable. We register this isomorphism as a
linear isomorphism in `multilinearCurryLeftEquiv R M M₂`.
The direct and inverse maps are given by `f.curryLeft` and `f.uncurryLeft`. Use these
unless you need the full framework of linear equivs. -/
@[simps]
def multilinearCurryLeftEquiv : MultilinearMap R M M₂ ≃ₗ[R] (M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂)
where
toFun := MultilinearMap.curryLeft
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun := LinearMap.uncurryLeft
left_inv := MultilinearMap.uncurry_curryLeft
right_inv := LinearMap.curry_uncurryLeft
