English
Let f: V1 → V2 be a linear map between finite-dimensional vector spaces over K. Then the dual map f.dualMap: V2* → V1* is surjective if and only if f is injective.
Русский
Пусть f: V1 → V2 — линейное отображение между конечномерными пространствами над K. Тогда дуальный отображение f.dualMap: V2* → V1* сюръективно тогда и только тогда, когда f инъективно.
LaTeX
$$$\\operatorname{range}(f) = V2 \\Rightarrow (f^{\\ast} \\text{ surjective}) \\iff f \\text{ injective}$$$
Lean4
/-- For vector spaces, `f.dualMap` is surjective if and only if `f` is injective -/
@[simp]
theorem dualMap_surjective_iff {f : V₁ →ₗ[K] V₂} : Function.Surjective f.dualMap ↔ Function.Injective f := by
rw [← LinearMap.range_eq_top, range_dualMap_eq_dualAnnihilator_ker, ← Submodule.dualAnnihilator_bot,
Subspace.dualAnnihilator_inj, LinearMap.ker_eq_bot]
