dualTensorHom — Mathlib

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ₗ

Похожие утверждения