English
There is a canonical linear map from M* ⊗ N to Hom(M,N) sending f ⊗ n to the linear map m ↦ f(m)·n.
Русский
Существует каноническое линейное отображение из M* ⊗ N в Hom(M,N), отправляющее f ⊗ n в линейное отображение m ↦ f(m)·n.
LaTeX
$$$\operatorname{dualTensorHom}: (M^* \otimes N) \to \mathrm{Hom}(M,N), \quad (f \otimes n)(m) = f(m)\,n$.$$
Lean4
/-- The natural map associating a linear map to the tensor product of two modules. -/
def dualTensorHom : Module.Dual R M ⊗[R] N →ₗ[R] M →ₗ[R] N :=
let M' := Module.Dual R M
(uncurry R M' N (M →ₗ[R] N) : _ → M' ⊗ N →ₗ[R] M →ₗ[R] N) LinearMap.smulRightₗ