English
Let b be a basis of an R-module M. There exists a canonical R-linear map toDual: M → M*, sending each basis vector b_i to the corresponding dual basis vector e^i. Equivalently, toDual(b_i) = e^i for all i, where {e^i} is the dual basis to {b_i}.
Русский
Пусть b — базис модуля M над R. Существует каноническое линейное отображение toDual: M → M*, отправляющее каждый базисный вектор b_i в соответствующий дуальный вектор e^i. Эквивалентно, для каждого i выполняется toDual(b_i) = e^i, где {e^i} — дуальная база к {b_i}.
LaTeX
$$$ b.toDual : M \to M^*, \quad b.toDual(b_i) = e^i \quad (\forall i \in \iota). $$$
Lean4
/-- The linear map from a vector space equipped with basis to its dual vector space,
taking basis elements to corresponding dual basis elements. -/
def toDual : M →ₗ[R] Module.Dual R M :=
b.constr ℕ fun v => b.constr ℕ fun w => if w = v then (1 : R) else 0
