feat(linear_algebra/linear_independent): add variant of `exists_linea…

…r_independent` (#9708)


Formalized as part of the Sphere Eversion project.

src/linear_algebra/dimension.lean

@@ -900,14 +900,9 @@ theorem linear_equiv.nonempty_equiv_iff_dim_eq :
 -- using `linear_independent_le_span'`
 lemma dim_span_le (s : set V) : module.rank K (span K s) ≤ #s :=
 begin
-  classical,
-  rcases
-    exists_linear_independent (linear_independent_empty K V) (set.empty_subset s)
-    with ⟨b, hb, _, hsb, hlib⟩,
-  have hsab : span K s = span K b,
-    from span_eq_of_le _ hsb (span_le.2 (λ x hx, subset_span (hb hx))),
+  obtain ⟨b, hb, hsab, hlib⟩ := exists_linear_independent K s,
   convert cardinal.mk_le_mk_of_subset hb,
-  rw [hsab, dim_span_set hlib]
+  rw [← hsab, dim_span_set hlib]
 end
 
 lemma dim_span_of_finset (s : finset V) :

src/linear_algebra/linear_independent.lean

@@ -52,7 +52,7 @@ vectors.
 In many cases we additionally provide dot-style operations (e.g., `linear_independent.union`) to
 make the linear independence tests usable as `hv.insert ha` etc.
 
-We also prove that, when working over a field,
+We also prove that, when working over a division ring,
 any family of vectors includes a linear independent subfamily spanning the same subspace.
 
 ## Implementation notes
@@ -1164,10 +1164,10 @@ by rw [linear_independent_fin_succ, linear_independent_unique_iff, range_unique,
   mem_span_singleton, not_exists,
   show fin.tail f (default (fin 1)) = f 1, by rw ← fin.succ_zero_eq_one; refl]
 
-lemma exists_linear_independent (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ t) :
-  ∃b⊆t, s ⊆ b ∧ t ⊆ span K b ∧ linear_independent K (λ x, x : b → V) :=
+lemma exists_linear_independent_extension (hs : linear_independent K (coe : s → V)) (hst : s ⊆ t) :
+  ∃b⊆t, s ⊆ b ∧ t ⊆ span K b ∧ linear_independent K (coe : b → V) :=
 begin
-  rcases zorn.zorn_subset_nonempty {b | b ⊆ t ∧ linear_independent K (λ x, x : b → V)} _ _
+  rcases zorn.zorn_subset_nonempty {b | b ⊆ t ∧ linear_independent K (coe : b → V)} _ _
     ⟨hst, hs⟩ with ⟨b, ⟨bt, bi⟩, sb, h⟩,
   { refine ⟨b, bt, sb, λ x xt, _, bi⟩,
     by_contra hn,
@@ -1180,27 +1180,39 @@ begin
     { exact subset_sUnion_of_mem } }
 end
 
+variables (K t)
+
+lemma exists_linear_independent :
+  ∃ b ⊆ t, span K b = span K t ∧ linear_independent K (coe : b → V) :=
+begin
+  obtain ⟨b, hb₁, -, hb₂, hb₃⟩ :=
+    exists_linear_independent_extension (linear_independent_empty K V) (set.empty_subset t),
+  exact ⟨b, hb₁, (span_eq_of_le _ hb₂ (submodule.span_mono hb₁)).symm, hb₃⟩,
+end
+
+variables {K t}
+
 /-- `linear_independent.extend` adds vectors to a linear independent set `s ⊆ t` until it spans
 all elements of `t`. -/
 noncomputable def linear_independent.extend (hs : linear_independent K (λ x, x : s → V))
   (hst : s ⊆ t) : set V :=
-classical.some (exists_linear_independent hs hst)
+classical.some (exists_linear_independent_extension hs hst)
 
 lemma linear_independent.extend_subset (hs : linear_independent K (λ x, x : s → V))
   (hst : s ⊆ t) : hs.extend hst ⊆ t :=
-let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent hs hst) in hbt
+let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent_extension hs hst) in hbt
 
 lemma linear_independent.subset_extend (hs : linear_independent K (λ x, x : s → V))
   (hst : s ⊆ t) : s ⊆ hs.extend hst :=
-let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent hs hst) in hsb
+let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent_extension hs hst) in hsb
 
 lemma linear_independent.subset_span_extend (hs : linear_independent K (λ x, x : s → V))
   (hst : s ⊆ t) : t ⊆ span K (hs.extend hst) :=
-let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent hs hst) in htb
+let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent_extension hs hst) in htb
 
 lemma linear_independent.linear_independent_extend (hs : linear_independent K (λ x, x : s → V))
   (hst : s ⊆ t) : linear_independent K (coe : hs.extend hst → V) :=
-let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent hs hst) in hli
+let ⟨hbt, hsb, htb, hli⟩ := classical.some_spec (exists_linear_independent_extension hs hst) in hli
 
 variables {K V}