feat(linear_algebra): maximal linear independent (#7160)

Co-authored by Anne Baanen and Kevin Buzzard



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/linear_algebra/linear_independent.lean

@@ -305,6 +305,17 @@ begin
       exacts [λ _, zero_smul _ _, λ _ _ _, add_smul _ _ _] } }
 end
 
+lemma linear_dependent_comp_subtype' {s : set ι} :
+  ¬ linear_independent R (v ∘ coe : s → M) ↔
+  ∃ f : ι →₀ R, f ∈ finsupp.supported R R s ∧ finsupp.total ι M R v f = 0 ∧ f ≠ 0 :=
+by simp [linear_independent_comp_subtype]
+
+/-- A version of `linear_dependent_comp_subtype'` with `finsupp.total` unfolded. -/
+lemma linear_dependent_comp_subtype {s : set ι} :
+  ¬ linear_independent R (v ∘ coe : s → M) ↔
+  ∃ f : ι →₀ R, f ∈ finsupp.supported R R s ∧ ∑ i in f.support, f i • v i = 0 ∧ f ≠ 0 :=
+linear_dependent_comp_subtype'
+
 theorem linear_independent_subtype {s : set M} :
   linear_independent R (λ x, x : s → M) ↔
   ∀ l ∈ (finsupp.supported R R s), (finsupp.total M M R id) l = 0 → l = 0 :=
@@ -629,6 +640,65 @@ end, λ H, linear_independent_iff.2 $ λ l hl, begin
   { simp [hl] }
 end⟩
 
+variable (R)
+
+lemma exists_maximal_independent' (s : ι → M) :
+  ∃ I : set ι, linear_independent R (λ x : I, s x) ∧
+    ∀ J : set ι, I ⊆ J → linear_independent R (λ x : J, s x) → I = J :=
+begin
+  let indep : set ι → Prop := λ I, linear_independent R (s ∘ coe : I → M),
+  let X := { I : set ι // indep I },
+  let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
+  have key : ∀ c : set X, zorn.chain r c → indep (⋃ (I : X) (H : I ∈ c), I),
+  { intros c hc,
+    dsimp [indep],
+    rw [linear_independent_comp_subtype],
+    intros f hsupport hsum,
+    rcases eq_empty_or_nonempty c with rfl | ⟨a, hac⟩,
+    { simpa using hsupport },
+    haveI : is_refl X r := ⟨λ _, set.subset.refl _⟩,
+    obtain ⟨I, I_mem, hI⟩ : ∃ I ∈ c, (f.support : set ι) ⊆ I :=
+      finset.exists_mem_subset_of_subset_bUnion_of_directed_on hac hc.directed_on hsupport,
+    exact linear_independent_comp_subtype.mp I.2 f hI hsum },
+  have trans : transitive r := λ I J K, set.subset.trans,
+  obtain ⟨⟨I, hli : indep I⟩, hmax : ∀ a, r ⟨I, hli⟩ a → r a ⟨I, hli⟩⟩ :=
+    @zorn.exists_maximal_of_chains_bounded _ r
+    (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), key c hc⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
+  exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩,
+end
+
+lemma exists_maximal_independent (s : ι → M) : ∃ I : set ι, linear_independent R (λ x : I, s x) ∧
+  ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I) :=
+begin
+  classical,
+  rcases exists_maximal_independent' R s with ⟨I, hIlinind, hImaximal⟩,
+  use [I, hIlinind],
+  intros i hi,
+  specialize hImaximal (I ∪ {i}) (by simp),
+  set J := I ∪ {i} with hJ,
+  have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I, by simp [hJ],
+  have hiJ : i ∈ J := by simp,
+  have h := mt hImaximal _, swap,
+  { intro h2,
+    rw h2 at hi,
+    exact absurd hiJ hi },
+  obtain ⟨f, supp_f, sum_f, f_ne⟩ := linear_dependent_comp_subtype.mp h,
+  have hfi : f i ≠ 0,
+  { contrapose hIlinind,
+    refine linear_dependent_comp_subtype.mpr ⟨f, _, sum_f, f_ne⟩,
+    simp only [finsupp.mem_supported, hJ] at ⊢ supp_f,
+    rintro x hx,
+    refine (memJ.mp (supp_f hx)).resolve_left _,
+    rintro rfl,
+    exact hIlinind (finsupp.mem_support_iff.mp hx) },
+  use [f i, hfi],
+  have hfi' : i ∈ f.support := finsupp.mem_support_iff.mpr hfi,
+  rw [← finset.insert_erase hfi', finset.sum_insert (finset.not_mem_erase _ _),
+      add_eq_zero_iff_eq_neg] at sum_f,
+  rw sum_f,
+  refine neg_mem _ (sum_mem _ (λ c hc, smul_mem _ _ (subset_span ⟨c, _, rfl⟩))),
+  exact (memJ.mp (supp_f (finset.erase_subset _ _ hc))).resolve_left (finset.ne_of_mem_erase hc),
+end
 end repr
 
 lemma surjective_of_linear_independent_of_span [nontrivial R]