English
There exists an auxiliary additive map liftAux that extends a bilinear map f' to a map on the tensor product, consistent with evaluating on simple tensors.
Русский
Существует вспомогательное отображение liftAux, расширяющее билинейный отображение f' на тензорное произведение, сохраняющее значение на простых тензорах.
LaTeX
$$$\\mathrm{liftAux} : M ⊗_R N \\to_+ P_2.$$$
Lean4
/-- Auxiliary function to constructing a linear map `M ⊗ N → P` given a bilinear map `M → N → P`
with the property that its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`. -/
def liftAux : M ⊗[R] N →+ P₂ :=
liftAddHom (LinearMap.toAddMonoidHom'.comp <| f'.toAddMonoidHom) fun r m n => by dsimp;
rw [LinearMap.map_smulₛₗ₂, map_smulₛₗ]
