English
If φ' is a linear map that agrees with φ on simple tensors via tprod, then φ' = lift φ.
Русский
Если φ' линейное отображение, совпадающее с φ на простых тензорах через tprod, то φ' = lift φ.
LaTeX
$$$$ \forall f, φ'(tprod(R,f)) = φ(f) \Rightarrow φ' = \text{lift } φ $$$$
Lean4
/-- Constructing a linear map `(⨂[R] i, s i) → E` given a `MultilinearMap R s E` with the
property that its composition with the canonical `MultilinearMap R s E` is
the given multilinear map `φ`. -/
def lift : MultilinearMap R s E ≃ₗ[R] (⨂[R] i, s i) →ₗ[R] E
where
toFun φ := { liftAux φ with map_smul' := liftAux.smul }
invFun φ' := φ'.compMultilinearMap (tprod R)
left_inv
φ := by
ext
simp [liftAux_tprod, LinearMap.compMultilinearMap]
right_inv
φ := by
ext
simp [liftAux_tprod]
map_add' φ₁
φ₂ := by
ext
simp [liftAux_tprod]
map_smul' r
φ₂ := by
ext
simp [liftAux_tprod]
