English
If two finite-dimensional vector spaces V and V2 have the same finite dimension, then for any linear map f: V → V2, f is injective if and only if f is surjective.
Русский
Если два конечномерных векторных пространства V и V₂ имеют одинаковую размерность, то для любого линейного отображения f: V → V₂ инъективность эквивалентна сюръективности.
LaTeX
$$$\operatorname{finrank}_K V = \operatorname{finrank}_K V_2 \Rightarrow \forall f: V \to V_2,\; \text{Injective}(f) \iff \text{Surjective}(f)$$$
Lean4
theorem injective_iff_surjective_of_finrank_eq_finrank [FiniteDimensional K V] [FiniteDimensional K V₂]
(H : finrank K V = finrank K V₂) {f : V →ₗ[K] V₂} : Function.Injective f ↔ Function.Surjective f :=
by
have := finrank_range_add_finrank_ker f
rw [← ker_eq_bot, ← range_eq_top]; refine ⟨fun h => ?_, fun h => ?_⟩
· rw [h, finrank_bot, add_zero, H] at this
exact eq_top_of_finrank_eq this
· rw [h, finrank_top, H] at this
exact Submodule.finrank_eq_zero.1 (add_right_injective _ this)
