eval — Mathlib

English

There is a canonical linear map from M to its double dual given by m ↦ (l ↦ l(m)).

Русский

Существует каноническое линейное отображение из M в двойственное пространство двойственного: m ↦ (l ↦ l(m)).

LaTeX

$$$ \\mathrm{eval} : M \\to_\\mathsf{R} \\ \\mathrm{Dual}\\; R\\; (\\mathrm{Dual}\\; R\\; M),\\; m \\mapsto (\\lambda l, l(m)) $$$

Lean4

/-- Maps a module M to the dual of the dual of M. See `Module.erange_coe` and
`Module.evalEquiv`. -/
def eval : M →ₗ[R] Dual R (Dual R M) :=
  LinearMap.flip LinearMap.id

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