English
Let W be a finite-dimensional subspace of a space V endowed with a separating dual. For any linear map f from W to V, the induced map on duals, obtained by taking the dual of f and composing with the natural inclusion W → V, is surjective if and only if f is injective. In other words, every continuous linear functional on W extends to a continuous linear functional on V exactly when f is injective.
Русский
Пусть W — конечномерное подпространство пространства V с разделяющим двойственным. Для любой линейной картины f: W → V получим отображение на двойственных пространствах, которое является сюрьективным тогда и только тогда, когда f инъективна. Иными словами, каждый непрерывный линейный функционал на W продлевается до непрерывного линейного функционала на V тогда и только тогда, когда f инъективна.
LaTeX
$$$\\operatorname{Surjective}(f^* \\circ \\mathrm{toLinearMap}) \;\Longleftrightarrow\; \\operatorname{Injective}(f)\\;,$$$
Lean4
/-- Given a finite-dimensional subspace `W` of a space `V` with separating dual, any
linear functional on `W` extends to a continuous linear functional on `V`.
This is stated more generally for an injective linear map from `W` to `V`. -/
theorem dualMap_surjective_iff {W} [AddCommGroup W] [Module R W] [FiniteDimensional R W] {f : W →ₗ[R] V} :
Surjective (f.dualMap ∘ ContinuousLinearMap.toLinearMap) ↔ Injective f :=
by
constructor <;> intro hf
· exact LinearMap.dualMap_surjective_iff.mp hf.of_comp
have := (separatingDual_iff_injective.mp ‹_›).comp hf
rw [← LinearMap.coe_comp] at this
exact LinearMap.flip_surjective_iff₁.mpr this
