English
An injective endomorphism gives a linear equivalence between finite-dimensional spaces of equal rank.
Русский
Инъективный эндоморфизм задаёт линейное эквивалентность между равной размерностью конечномерными простыми пространствами.
LaTeX
$$$\text{If } f:\ V\to V\text{ is injective and } \dim V = \dim V', \text{ then } V \cong_K V' \text{ via an explicit equivalence }$$$
Lean4
/-- An injective linear map between finite-dimensional modules of equal rank
is a linear equivalence.
Unlike `LinearEquiv.ofFinrankEq` (which creates an *abstract* linear equivalence from `V` to `V'`),
this lemma improves a *given* injective linear map to a linear equivalence.
-/
noncomputable def ofInjectiveOfFinrankEq (f : V →ₗ[K] V') (hinj : Function.Injective f)
(hrank : Module.finrank K V = Module.finrank K V') : V ≃ₗ[K] V' :=
haveI : LinearMap.range f = ⊤ := Submodule.eq_top_of_finrank_eq ((LinearMap.finrank_range_of_inj hinj).trans hrank)
(ofInjective f hinj).trans (ofTop (LinearMap.range f) this)
