English
Given a linear map f: M1 → M2, there is a canonical dual map f^*: Dual(R, M2) → Dual(R, M1) defined by f^*(φ) = φ ∘ f, sending a functional on M2 to its composition with f.
Русский
Пусть f: M1 → M2 — линейное отображение. Существуют естественное дуальное отображение f^*: (M2)^* → (M1)^*, задаваемое f^*(φ) = φ ∘ f, переводя функционал на M2 в функционал на M1.
LaTeX
$$$$ f^*(\\phi) = \\phi \\circ f \\quad (\\phi \\in \\mathrm{Dual}\\, R\, M_2). $$$$
Lean4
/-- Given a linear map `f : M₁ →ₗ[R] M₂`, `f.dualMap` is the linear map between the dual of
`M₂` and `M₁` such that it maps the functional `φ` to `φ ∘ f`. -/
def dualMap (f : M₁ →ₗ[R] M₂) : Dual R M₂ →ₗ[R] Dual R M₁ :=
Module.Dual.transpose f
