English
Given hv: LinearIndepOn R id s and h: n < rank_R M, there exists t with s ⊆ t, and t realizes the full rank: #t = rank_R M and LinearIndepOn R id t.
Русский
Пусть hv: LinearIndepOn R id s и h: n < rank_R M; тогда существует t, содержащий s, который достигает полного ранга: #t = rank_R M и LinearIndepOn R id t.
LaTeX
$$$\exists t\; (s \subseteq t) \land (\#t = \operatorname{Module.rank} R M) \land \operatorname{LinearIndepOn} R id t$$$
Lean4
theorem exists_linearIndepOn_of_lt_rank [StrongRankCondition R] {s : Set M} (hs : LinearIndepOn R id s) :
∃ t, s ⊆ t ∧ #t = Module.rank R M ∧ LinearIndepOn R id t :=
by
obtain ⟨t, ht, ht'⟩ := exists_set_linearIndependent R (M ⧸ Submodule.span R s)
choose sec hsec using Submodule.mkQ_surjective (Submodule.span R s)
have hsec' : (Submodule.mkQ _) ∘ sec = _root_.id := funext hsec
have hst : Disjoint s (sec '' t) := by
rw [Set.disjoint_iff]
rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩
apply ht'.ne_zero ⟨x, hxt⟩
rw [Subtype.coe_mk, ← hsec x, mkQ_apply, Quotient.mk_eq_zero]
exact Submodule.subset_span hxs
refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩
· rw [Cardinal.mk_union_of_disjoint hst, Cardinal.mk_image_eq, ht, ← rank_quotient_add_rank (Submodule.span R s),
add_comm, rank_span_set hs]
exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩
· apply LinearIndepOn.union_id_of_quotient Submodule.subset_span hs
rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp, ← image_comp, hsec', image_id]
