English
For a linear map f: V → V', and any cardinal c, c ≤ rank f if and only if there exists a subset s ⊆ V with the image f|s being linearly independent and such that |s| = c (via lifting).
Русский
Для линейного отображения f: V → V' и любой кардинал c существует подмножество s ⊆ V такое, что образ f|s линейно независим и |s| = c (с учётом подъёма кардиналов).
LaTeX
$$$\exists s \subseteq V, \; (|s| = c).lift \land \operatorname{LinearIndepOn} K f s$$$
Lean4
theorem le_rank_iff_exists_linearIndependent {c : Cardinal} {f : V →ₗ[K] V'} :
c ≤ rank f ↔ ∃ s : Set V, Cardinal.lift.{v'} #s = Cardinal.lift.{v} c ∧ LinearIndepOn K f s :=
by
rcases f.rangeRestrict.exists_rightInverse_of_surjective f.range_rangeRestrict with ⟨g, hg⟩
have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg
refine ⟨fun h => ?_, ?_⟩
· rcases _root_.le_rank_iff_exists_linearIndependent.1 h with ⟨s, rfl, si⟩
refine ⟨g '' s, Cardinal.mk_image_eq_lift _ _ fg.injective, ?_⟩
replace fg : ∀ x, f (g x) = x := by
intro x
convert congr_arg Subtype.val (fg x)
replace si : LinearIndepOn K (fun x => f (g x)) s := by simpa only [fg] using si.map' _ (ker_subtype _)
exact si.image_of_comp
· rintro ⟨s, hsc, si⟩
have : LinearIndepOn K f.rangeRestrict s := LinearIndependent.of_comp (LinearMap.range f).subtype (by convert si)
convert this.id_image.cardinal_le_rank
rw [← Cardinal.lift_inj, ← hsc, Cardinal.mk_image_eq_of_injOn_lift]
exact injOn_iff_injective.2 this.injective
