English
For a linear map f: V1 → V2, the finiteness of the dimension of the range of the dual map equals the finiteness of the dimension of the range of f.
Русский
Для линейного отображения f: V1 → V2 размерность образа дуального отображения равна размерности образа самого отображения.
LaTeX
$$$\\dim\\_K(\\operatorname{range}(f^{\\ast})) = \\dim\\_K(\\operatorname{range}(f))$$$
Lean4
@[simp]
theorem finrank_range_dualMap_eq_finrank_range (f : V₁ →ₗ[K] V₂) :
finrank K (LinearMap.range f.dualMap) = finrank K (LinearMap.range f) :=
by
rw [congr_arg dualMap (show f = (range f).subtype.comp f.rangeRestrict by rfl), ← dualMap_comp_dualMap, range_comp,
range_eq_top.mpr (dualMap_surjective_of_injective (range f).injective_subtype), Submodule.map_top,
finrank_range_of_inj, Subspace.dual_finrank_eq]
exact dualMap_injective_of_surjective (range_eq_top.mp f.range_rangeRestrict)
