English
The rank of the range of a linear map is at most the rank of the domain.
Русский
Ранг образа линейного отображения не превосходит ранг области.
LaTeX
$$$\operatorname{rank}_R(\operatorname{Range}(f)) \le \operatorname{rank}_R(M)$$$
Lean4
/-- The rank of the range of a linear map is at most the rank of the source. -/
-- The proof is: a free submodule of the range lifts to a free submodule of the
-- source, by arbitrarily lifting a basis.
theorem lift_rank_range_le (f : M →ₗ[R] M') :
Cardinal.lift.{v} (Module.rank R (LinearMap.range f)) ≤ Cardinal.lift.{v'} (Module.rank R M) :=
by
simp only [Module.rank_def]
rw [Cardinal.lift_iSup (Cardinal.bddAbove_range _)]
apply ciSup_le'
rintro ⟨s, li⟩
apply le_trans
swap
· apply Cardinal.lift_le.mpr
refine le_ciSup (Cardinal.bddAbove_range _) ⟨rangeSplitting f '' s, ?_⟩
apply LinearIndependent.of_comp f.rangeRestrict
convert li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _) using 1
· exact (Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge
