maximal independent family

Stream: maths

[Patrick Massot]

Do we have the following?

import linear_algebra.basis
open submodule

lemma exists_maximal_independent {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (s : ι → M) :
  ∃ I : set ι, linear_independent R (λ x : I, s x) ∧
               ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I) :=

Does anyone feel they could prove this while I'm having dinner and putting my kids to bed?

[Patrick Massot]

@Anne Baanen maybe?

[Heather Macbeth]

Maybe this is two separate lemmas?

• existence of a maximal linearly independent set
• the fact that if {i} \union I is not linearly independent and I is then ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)

[Kevin Buzzard]

I might spend some time trying this and live streaming on Discord

[Julian Berman]

Depending on how long it takes to get children to bed you may get a proof of that out of the matroid merging work too :D

[Kevin Buzzard]

I'm assuming this

import linear_algebra.basis
open submodule

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (s : ι → M) :
  ∃ I : set ι, linear_independent R (λ x : I, s x) ∧
    ∀ J : set ι, I ⊆ J → linear_independent R (λ x : J, s x) → I = J :=
-- Zorn
sorry

and doing the dirty work of showing this is enough. I think you prove the above lemma with zorn_subset in order.zorn(and I won't start on it until I've shown it's enough, which might take a while, finsets are no fun)

[Kevin Buzzard]

There's no finset.comap under an injectivity assumption??

[Adam Topaz]

docs#finset.preimage

[Kevin Buzzard]

Thanks. The one the other way is called finset.map :-/

[Adam Topaz]

lol

[Johan Commelin]

There's finset.map and finset.image.

[Adam Topaz]

What's the difference? Oh map uses an embedding as the map?

[Johan Commelin]

Right, so for one of them the resulting finset is computable

[Adam Topaz]

Oh I see.

[Patrick Massot]

I'm back, where is my proof?

[Patrick Massot]

More seriously, is there any beginning of proof I should try to continue?

[Kevin Buzzard]

import linear_algebra.basis
open submodule

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (s : ι → M) :
  ∃ I : set ι, linear_independent R (λ x : I, s x) ∧
    ∀ J : set ι, I ⊆ J → linear_independent R (λ x : J, s x) → I = J :=
-- Zorn
sorry

open set

lemma exists_maximal_independent {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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
  rcases exists_maximal_independent' R s with ⟨I, hIlinind, hImaximal⟩,
  use [I, hIlinind],
  intros i hi,
  specialize hImaximal (I ∪ {i}) (by simp),
  have h := mt hImaximal _, swap,
  { intro h2,
    rw set.ext_iff at h2,
    rcases h2 i with ⟨-, h3⟩,
    apply hi,
    apply h3,
    simp,
  },
  set J := I ∪ {i} with hJ,
  rw linear_dependent_iff at h,
  rcases h with ⟨S, f, hS1, j, hj, hS2⟩,
  have hiJ : i ∈ J := by simp,
  have hIJ : I ⊆ J := by simp,
  have hiS : (⟨i, hiJ⟩ : J) ∈ S,
  { by_contra hiS',
    rw linear_independent_iff' at hIlinind,
    apply hS2,
    specialize hIlinind (finset.preimage S (λ i, ⟨i.1, hIJ i.2⟩) _),
    { rintros ⟨x, hxI⟩ hx ⟨y,hyI⟩ hy h, simpa using h },
    specialize hIlinind (λ i, f ⟨i.1, hIJ i.2⟩) _ ⟨j.1, _⟩ _,
    { rw ← hS1,
      convert finset.sum_preimage _ _ _ _ _,
      { ext, simp },
      rintros ⟨x, hxJ⟩ hxS hxI,
      exfalso, apply hxI,
      suffices : x ∈ I, by simpa,
      rw set.mem_union at hxJ,
      cases hxJ with hxI hxi, assumption,
      exfalso,
      apply hiS',
      convert hxS,
      rw mem_singleton_iff at hxi,
      exact hxi.symm },
    { cases j with j hjJ,
      rw mem_union at hjJ,
      cases hjJ with hjI hji, exact hjI,
      exfalso, apply hiS',
      convert hj,
      rw mem_singleton_iff at hji,
      exact hji.symm },
    { rw finset.mem_preimage,
      cases j,
      exact hj },
    { sorry }
  },
  sorry
end

[Kevin Buzzard]

I left you the Zorn and I'm nearly done with the proof that it implies what you want (I'm still going)

[Kevin Buzzard]

You eat quickly for a Frenchman

[Heather Macbeth]

Here's the easy part of the Zorn, btw:

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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 -- Zorn
  obtain ⟨I, H, hI⟩ := zorn.zorn_subset {J : set ι | linear_independent R (λ x : J, s x)} _,
  { refine ⟨I, H, _⟩,
    intros J hIJ hJ,
    exact (hI J hJ hIJ).symm },
  sorry,
end

[Heather Macbeth]

What's left is a variation on docs#linear_independent_bUnion_of_directed, docs#linear_independent_sUnion_of_directed etc, but I don't think it exists directly.

[Kevin Buzzard]

I need to go for my dinner now, there's still some work to do:

import linear_algebra.basis
open submodule

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (s : ι → M) :
  ∃ I : set ι, linear_independent R (λ x : I, s x) ∧
    ∀ J : set ι, I ⊆ J → linear_independent R (λ x : J, s x) → I = J :=
-- Zorn
sorry

open set

lemma exists_maximal_independent {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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
  rcases exists_maximal_independent' R s with ⟨I, hIlinind, hImaximal⟩,
  use [I, hIlinind],
  intros i hi,
  specialize hImaximal (I ∪ {i}) (by simp),
  have h := mt hImaximal _, swap,
  { intro h2,
    rw set.ext_iff at h2,
    rcases h2 i with ⟨-, h3⟩,
    apply hi,
    apply h3,
    simp,
  },
  set J := I ∪ {i} with hJ,
  rw linear_dependent_iff at h,
  rcases h with ⟨S, f, hS1, j, hj, hS2⟩,
  have hiJ : i ∈ J := by simp,
  have hIJ : I ⊆ J := by simp,
  have hiS : (⟨i, hiJ⟩ : J) ∈ S,
  { by_contra hiS',
    rw linear_independent_iff' at hIlinind,
    apply hS2,
    specialize hIlinind (finset.preimage S (λ i, ⟨i.1, hIJ i.2⟩) _),
    { rintros ⟨x, hxI⟩ hx ⟨y,hyI⟩ hy h, simpa using h },
    specialize hIlinind (λ i, f ⟨i.1, hIJ i.2⟩) _ ⟨j.1, _⟩ _,
    { rw ← hS1,
      convert finset.sum_preimage _ _ _ _ _,
      { ext, simp },
      rintros ⟨x, hxJ⟩ hxS hxI,
      exfalso, apply hxI,
      suffices : x ∈ I, by simpa,
      rw set.mem_union at hxJ,
      cases hxJ with hxI hxi, assumption,
      exfalso,
      apply hiS',
      convert hxS,
      rw mem_singleton_iff at hxi,
      exact hxi.symm },
    { cases j with j hjJ,
      rw mem_union at hjJ,
      cases hjJ with hjI hji, exact hjI,
      exfalso, apply hiS',
      convert hj,
      rw mem_singleton_iff at hji,
      exact hji.symm },
    { rw finset.mem_preimage,
      cases j,
      exact hj },
    { simpa using hIlinind },
  },
  use f ⟨i, hiJ⟩,
  split,
  { sorry },
  sorry
end

[Yury G. Kudryashov]

We have docs#exists_linear_independent for division_rings

[Heather Macbeth]

But it's stated for sets, not for parametrized sets (Patrick's function s : ι → M).

[Patrick Massot]

This is a nightmare. They are so many statements that are impossible to distinguish on paper yet crazily hard to prove from each other in Lean...

[Yury G. Kudryashov]

I don't know why all these lemmas are written for sets.

[Yury G. Kudryashov]

I'm going to rewrite most of them for indexed families.

[Sebastien Gouezel]

Weren't these things written initially for sets (even bases were sets at the beginning), and then we realized that indexed families were better but we haven't refactored everything yet?

[Patrick Massot]

I could cheat and rewrite what I'm actually interested in in terms of sets, but that would mean one more proof to refactor later.

[Yury G. Kudryashov]

I have a lecture in 1 hour, then I can refactor many proofs in linear_algebra/linear_independent to use families.

[Heather Macbeth]

I am guilty of this laziness myself ... docs#exists_maximal_orthonormal

[Yury G. Kudryashov]

Even if a theorem is about sets (and, e.g., unions), there is no reason to use s : set M + coe instead of s : set α and f ∘ coe.

[Yury G. Kudryashov]

@Patrick Massot Can you wait till tomorrow morning?

[Yury G. Kudryashov]

Probably you'll be asleep when (1 hr + 2 hr lecture + time for dinner + time for refactor) passes.

[Patrick Massot]

I can definitely wait for tomorrow morning.

[Patrick Massot]

It's a bit frustrating to be stuck on such a lemma while everything else was straightforward in the little goal I had for the second half of my afternoon: over a pid, finitely generated torsion free modules are free (Anne did all the hard work already).

[Kevin Buzzard]

By the way, the first sorry in the big proof has maths proof "if f i = 0 then hS1 says that we have a linear relation on f(I) and hS2 says it's nontrivial, contradicting hIlinind" (which still looks like some pain) and the second is just a rephrasing of hS1 using the fact that J is the disjoint union of I and {i}

[Patrick Massot]

I'll have a look at that part

[Kevin Buzzard]

It's annoying that I gets coerced to a type, somehow I spend far too long dancing between the type corresponding to I and the one corresponding to I union {i}. If we were doing finsupps supported on I or J I think life would be much easier.

[Kevin Buzzard]

You just say "if support of f is in I union {i} and f(i) = 0 then the support of f is in I"

[Patrick Massot]

Another solution maybe to copy the weird setup of docs#filter.has_basis. We would have a definition

def linear_independent_on (s : ι → M) (p : ι → Prop) : Prop

which would be equivalent to linear_independent R (λ x : subtype p, s x) with a good interface.

[Anne Baanen]

I'll take a stab at the following lemma, which should clear up a lot of the mucking about with subtypes:

lemma set.linear_dependent_iff {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (v : ι → M) (s : set ι) :
  ¬ linear_independent R (v ∘ coe : s → M) ↔
    ∃ f : ι →₀ R, ∑ i in f.support, f i • v i = 0 ∧ f ≠ 0 ∧ ↑f.support ⊆ s :=

[Anne Baanen]

OK, that was not so bad:

lemma set.linear_dependent_iff {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (v : ι → M) (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 :=
by simp only [linear_independent_comp_subtype, not_forall, exists_prop, finsupp.total_apply, finsupp.sum]

[Anne Baanen]

lemma exists_maximal_independent {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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
  haveI := classical.dec_eq ι,
  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 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⟩ := set.linear_dependent_iff.mp h,
  have hfi : f i ≠ 0,
  { contrapose hIlinind,
    refine set.linear_dependent_iff.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

[Anne Baanen]

Now we just need to do Zorn

[Kevin Buzzard]

Very nice! Yes this is much better than my approach, but I only realised it after struggling with my approach :-)

[Anne Baanen]

Nearly there, just one sorry that I'm sure is in the library somewhere:

import linear_algebra.basis
import order.zorn

open submodule

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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 X := { I : set ι // linear_independent R (s ∘ coe : I → M) },
  let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
  have trans : transitive r := λ I J K, set.subset.trans,
  obtain ⟨⟨I, hli⟩, hmax⟩ := @zorn.exists_maximal_of_chains_bounded _ r
    (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), _⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
  { exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩ },
  { rw linear_independent_comp_subtype,
    intros f hsupport hsum,
    -- `f` has finite support and `c` is a chain, so there must be an `I ∈ c`
    -- with `f.support ⊆ I`
    obtain ⟨I, I_mem, hI⟩ : ∃ I ∈ c, (↑f.support : set ι) ⊆ I := sorry,
    exact linear_independent_comp_subtype.mp I.2 f hI hsum },
end

open set
open_locale big_operators

lemma set.linear_dependent_iff {ι : Type*} {R : Type*} [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] {v : ι → M} {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 :=
by simp only [linear_independent_comp_subtype, not_forall, exists_prop, finsupp.total_apply, finsupp.sum]

lemma exists_maximal_independent {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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
  haveI := classical.dec_eq ι,
  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⟩ := set.linear_dependent_iff.mp h,
  have hfi : f i ≠ 0,
  { contrapose hIlinind,
    refine set.linear_dependent_iff.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

[Anne Baanen]

Hmm, I can't find the following lemma:

lemma finset.exists_mem_subset_of_subset_bUnion_of_chain {α ι : Type*}
  (f : ι → set α)  (c : set ι) (hc : zorn.chain (λ i j, f i ⊆ f j) c)
  (s : finset α) (hs : ↑s ⊆ (⋃ i ∈ c, f i)) : ∃ i ∈ c, ↑s ⊆ f i := sorry

[Anne Baanen]

Tried messing about with directed but can't make the puzzle fit yet and it's time to go to bed. So I'll let you fill in the last piece :)

[Anne Baanen]

Full code:

import linear_algebra.basis
import order.zorn

open submodule

lemma finset.exists_mem_subset_of_subset_bUnion_of_chain {α ι : Type*}
  (f : ι → set α)  (c : set ι) (hc : zorn.chain (λ i j, f i ⊆ f j) c)
  (s : finset α) (hs : ↑s ⊆ (⋃ i ∈ c, f i)) : ∃ i ∈ c, ↑s ⊆ f i :=
by library_search

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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 X := { I : set ι // linear_independent R (s ∘ coe : I → M) },
  let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
  have trans : transitive r := λ I J K, set.subset.trans,
  obtain ⟨⟨I, hli⟩, hmax⟩ := @zorn.exists_maximal_of_chains_bounded _ r
    (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), _⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
  { exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩ },
  { rw linear_independent_comp_subtype,
    intros f hsupport hsum,
    -- `f` has finite support and `c` is a chain, so there must be an `I ∈ c`
    -- with `f.support ⊆ I`
    obtain ⟨I, I_mem, hI⟩ : ∃ I ∈ c, (↑f.support : set ι) ⊆ I :=
      finset.exists_mem_subset_of_subset_bUnion_of_chain _ c hc f.support hsupport,
    exact linear_independent_comp_subtype.mp I.2 f hI hsum },
end

open set
open_locale big_operators

lemma set.linear_dependent_iff {ι : Type*} {R : Type*} [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] {v : ι → M} {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 :=
by simp only [linear_independent_comp_subtype, not_forall, exists_prop, finsupp.total_apply, finsupp.sum]

lemma exists_maximal_independent {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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
  haveI := classical.dec_eq ι,
  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⟩ := set.linear_dependent_iff.mp h,
  have hfi : f i ≠ 0,
  { contrapose hIlinind,
    refine set.linear_dependent_iff.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

[Kevin Buzzard]

I think the lemma is false because c can be empty.

[Kevin Buzzard]

I need to go to bed but we're nearly there: I went for the "just do it by induction" approach but unfortunately I don't have time to finish. I modified the lemma so it should hopefully be true now and I fixed the application:

import linear_algebra.basis
import order.zorn

open submodule

lemma finset.exists_mem_subset_of_subset_bUnion_of_chain {α ι : Type*}
  (f : ι → set α)  (c : set ι) (a : ι) (hac : a ∈ c) (hc : zorn.chain (λ i j, f i ⊆ f j) c)
  (s : finset α) (hs : ↑s ⊆ (⋃ i ∈ c, f i)) : ∃ i ∈ c, ↑s ⊆ f i :=
begin
  revert hs,
  classical,
  apply finset.induction_on s,
  { intro _,
    use [a, hac],
    simp },
  { intros b t hbt htc hbtc,
    specialize htc (set.subset.trans _ hbtc), simp,
    have hbc : b ∈ ⋃ (i : ι) (H : i ∈ c), f i,
    { apply hbtc, simp },
    rw set.mem_bUnion_iff at hbc,
    rcases htc with ⟨i, hic, hti⟩,
    rcases hbc with ⟨j, hjc, htj⟩,
    sorry }
end

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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 X := { I : set ι // linear_independent R (s ∘ coe : I → M) },
  let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
  have trans : transitive r := λ I J K, set.subset.trans,
  obtain ⟨⟨I, hli⟩, hmax⟩ := @zorn.exists_maximal_of_chains_bounded _ r
    (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), _⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
  { exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩ },
  { rw linear_independent_comp_subtype,
    intros f hsupport hsum,
    -- `f` has finite support and `c` is a chain, so there must be an `I ∈ c`
    -- with `f.support ⊆ I`
    by_cases ha : ∃ a : X, a ∈ c,
    { cases ha with a hac,
      obtain ⟨I, I_mem, hI⟩ : ∃ I ∈ c, (↑f.support : set ι) ⊆ I :=
        finset.exists_mem_subset_of_subset_bUnion_of_chain _ c a hac hc f.support hsupport,
    exact linear_independent_comp_subtype.mp I.2 f hI hsum },
    { ext x,
      rw finsupp.mem_supported' at hsupport,
      apply hsupport,
      simp only [not_exists, exists_prop, set.mem_Union, not_and, exists_and_distrib_right, subtype.exists, subtype.coe_mk,
  exists_imp_distrib],
      intros S hS hc,
      exfalso,
      apply ha,
      use ⟨S, hS⟩, exact hc } },
end

[Kevin Buzzard]

You just take the max of i and j to finish it

[Eric Rodriguez]

hadn't done lean for a couple days, so finished it up to get unrust a little. all that's needed after the sorry is this:

    haveI : is_refl ι (λ i j, f i ⊆ f j) := ⟨λ _, by refl⟩,
    cases hc.total_of_refl hic hjc,
      { use j, refine ⟨hjc, _⟩,
        rw [finset.coe_insert, set.insert_subset],
        exact ⟨htj, trans hti h⟩ },
      { use i, refine ⟨hic, _⟩,
        rw [finset.coe_insert, set.insert_subset],
        exact ⟨h htj, hti⟩ } }

If I wake up early tomorrow morning I'll try to tidy up to learn the style (tbh, all I know is that non-terminating simps should be replaced with simp only, but gotta start learning somewhere) but have a feeling I won't be the first awake :b

[Patrick Massot]

Thanks everybody, you are wonderful!

[Patrick Massot]

Tonight I'll open mathlib PR with all that (with proper coauthors) if nobody does it first. Right now, at the bottom of linear_algebra.free_module, right before the section end, if I have the following content. The plan is of course to move preparatory lemmas and definitions into proper place. But it can be helpful to see everything at once if @Anne Baanen wants to comment on the strategy.

open set submodule function finset
open_locale big_operators

lemma finset.exists_mem_subset_of_subset_bUnion_of_chain {α ι : Type*}
  (f : ι → set α)  (c : set ι) (a : ι) (hac : a ∈ c) (hc : zorn.chain (λ i j, f i ⊆ f j) c)
  (s : finset α) (hs : ↑s ⊆ (⋃ i ∈ c, f i)) : ∃ i ∈ c, ↑s ⊆ f i :=
begin
  revert hs,
  classical,
  apply finset.induction_on s,
  { intro _,
    use [a, hac],
    simp },
  { intros b t hbt htc hbtc,
    specialize htc (set.subset.trans _ hbtc), simp,
    have hbc : b ∈ ⋃ (i : ι) (H : i ∈ c), f i,
    { apply hbtc, simp },
    rw set.mem_bUnion_iff at hbc,
    rcases htc with ⟨i, hic, hti⟩,
    rcases hbc with ⟨j, hjc, htj⟩,
    haveI : is_refl ι (λ i j, f i ⊆ f j) := ⟨λ _, by refl⟩,
    cases hc.total_of_refl hic hjc,
      { use j, refine ⟨hjc, _⟩,
        rw [finset.coe_insert, set.insert_subset],
        exact ⟨htj, trans hti h⟩ },
      { use i, refine ⟨hic, _⟩,
        rw [finset.coe_insert, set.insert_subset],
        exact ⟨h htj, hti⟩ } }
end

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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 X := { I : set ι // linear_independent R (s ∘ coe : I → M) },
  let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
  have trans : transitive r := λ I J K, set.subset.trans,
  obtain ⟨⟨I, hli⟩, hmax⟩ := @zorn.exists_maximal_of_chains_bounded _ r
    (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), _⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
  { exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩ },
  { rw linear_independent_comp_subtype,
    intros f hsupport hsum,
    -- `f` has finite support and `c` is a chain, so there must be an `I ∈ c`
    -- with `f.support ⊆ I`
    by_cases ha : ∃ a : X, a ∈ c,
    { cases ha with a hac,
      obtain ⟨I, I_mem, hI⟩ : ∃ I ∈ c, (↑f.support : set ι) ⊆ I :=
        finset.exists_mem_subset_of_subset_bUnion_of_chain _ c a hac hc f.support hsupport,
    exact linear_independent_comp_subtype.mp I.2 f hI hsum },
    { ext x,
      rw finsupp.mem_supported' at hsupport,
      apply hsupport,
      simp only [not_exists, exists_prop, set.mem_Union, not_and, exists_and_distrib_right, subtype.exists, subtype.coe_mk,
  exists_imp_distrib],
      intros S hS hc,
      exfalso,
      apply ha,
      use ⟨S, hS⟩, exact hc } },
end

lemma set.linear_dependent_iff {ι : Type*} {R : Type*} [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] {v : ι → M} {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 :=
by simp only [linear_independent_comp_subtype, not_forall, exists_prop, finsupp.total_apply, finsupp.sum]

lemma exists_maximal_independent {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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
  haveI := classical.dec_eq ι,
  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⟩ := set.linear_dependent_iff.mp h,
  have hfi : f i ≠ 0,
  { contrapose hIlinind,
    refine set.linear_dependent_iff.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

/-- A module is torsion free if `a • x = 0` implies `a = 0` or `x = 0`. -/
def torsion_free (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M] [module R M] : Prop :=
∀ (a : R) (x : M), a • x = 0 → a = 0 ∨ x = 0

variable (M)
def linear_map.smul_left (a : R) : M →ₗ[R] M :=
{ to_fun := λ x, a  • x,
  map_smul' := λ b, smul_algebra_smul_comm b a,
  map_add' := smul_add a }

variable {M}


lemma torsion_free.injective_smul_left (h : torsion_free R M) {a : R} (ha : a ≠ 0) :
  injective (linear_map.smul_left M a) :=
begin
  rw ← linear_map.ker_eq_bot,
  ext x,
  rw [linear_map.mem_ker, mem_bot],
  change a • x = 0 ↔ _,
  split,
  { intro hax,
    have := h a x hax,
    tauto },
  { rintro rfl,
    exact smul_zero a },
end

lemma torsion_free.ker_smul_left (h : torsion_free R M) {a : R} (ha : a ≠ 0) :
  (linear_map.smul_left M a).ker = ⊥ :=
linear_map.ker_eq_bot_of_injective (h.injective_smul_left ha)

lemma finset.prod_eq_mul_prod_erase {α : Type*} [decidable_eq α] {M : Type*} [comm_monoid M] {s : finset α} {a : α} (h : a ∈ s) (f : α → M) :
∏ i in s, f i = (f a) * ∏ i in erase s a, f i :=
begin
  conv_lhs { rw ← insert_erase h },
  rw finset.prod_insert,
  exact not_mem_erase a s
end

lemma finset.prod_eq_prod_erase_mul {α : Type*} [decidable_eq α] {M : Type*} [comm_monoid M] {s : finset α} {a : α} (h : a ∈ s) (f : α → M) :
∏ i in s, f i = (∏ i in erase s a, f i) * f a :=
by rw [finset.prod_eq_mul_prod_erase h, mul_comm]

lemma fintype.prod_eq_mul_prod_erase {α : Type*} [fintype α] [decidable_eq α] {M : Type*} [comm_monoid M] (a : α) (f : α → M) :
∏ i, f i = (f a) * ∏ i in erase univ a, f i :=
begin
  rw finset.prod_eq_mul_prod_erase,
  exact mem_univ a
end

lemma fintype.prod_eq_prod_erase_mul {α : Type*} [fintype α] [decidable_eq α] {M : Type*} [comm_monoid M] (a : α) (f : α → M) :
∏ i, f i = (∏ i in erase univ a, f i) * f a :=
begin
  rw finset.prod_eq_prod_erase_mul,
  exact mem_univ a
end

lemma linear_map.map_span_le {R M M₂ : Type*} [semiring R] [add_comm_monoid M]
  [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂)
  (s : set M) (N : submodule R M₂) : map f (span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N :=
begin
  rw [map_span, span_le, set.image_subset_iff],
  exact iff.rfl
end


lemma module.free_of_finite_type_torsion_free [fintype ι] {s : ι → M} (hs : span R (range s) = ⊤)
  (h : torsion_free R M) :
  ∃ (n : ℕ) (B : fin n → M), is_basis R B :=
begin
  classical,
  obtain ⟨I : set ι,
          indepI : linear_independent R (s ∘ coe : I → M),
          hI : ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)⟩ :=
    exists_maximal_independent R s,
  let N := span R (range $ (s ∘ coe : I → M)), -- same as `span R (s '' I)` but more convenient
  let sI : I → N := λ i, ⟨s i.1, subset_span (mem_range_self i)⟩, -- `s` restricted to `I`
  have sI_basis : is_basis R sI, -- `s` restricted to `I` is a basis of `N`
    from is_basis_span indepI,
  have exists_a : ∀ i : ι, ∃ a : R, a ≠ 0 ∧ a • s i ∈ N,
  { intro i,
    by_cases hi : i ∈ I,
    { use [1, zero_ne_one.symm],
      rw one_smul,
      exact subset_span (mem_range_self (⟨i, hi⟩ : I)) },
    { simpa [image_eq_range s I] using hI i hi } },
  choose a ha ha' using exists_a,
  let A := ∏ i, a i,
  have ha : A ≠ 0,
  { rw finset.prod_ne_zero_iff,
    simpa using ha },
  let φ : M →ₗ[R] M := linear_map.smul_left M A,
  have : φ.ker = ⊥,
    from h.ker_smul_left ha,
  let ψ : M ≃ₗ[R] φ.range := linear_equiv.of_injective φ this,
  have : φ.range ≤ N,
  { suffices : ∀ i, φ (s i) ∈ N,
    { rw [linear_map.range, ← hs, φ.map_span_le],
      rintros _ ⟨i, rfl⟩, apply this },
    intro i,
    calc (∏ j, a j) • s i = (∏ j in finset.univ.erase i, a j) • a i • s i : by rw [fintype.prod_eq_prod_erase_mul i, mul_smul]
                      ... ∈ N  : N.smul_mem _ (ha' i) },
  obtain ⟨n, B : fin n → φ.range, hB : is_basis R B⟩ :=
    submodule.exists_is_basis_of_le this sI_basis,
  exact ⟨n, ψ.symm ∘ B, linear_equiv.is_basis hB ψ.symm⟩
end

[Patrick Massot]

Note for everyone: since the final lemma is pretty important, I tried to write it in a readable style. I'd be interested in people skipping everything and trying to read it, without tactic state help. Let me copy it again on its own:

lemma module.free_of_finite_type_torsion_free [fintype ι] {s : ι → M} (hs : span R (range s) = ⊤)
  (h : torsion_free R M) :
  ∃ (n : ℕ) (B : fin n → M), is_basis R B :=
begin
  classical,
  obtain ⟨I : set ι,
          indepI : linear_independent R (s ∘ coe : I → M),
          hI : ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)⟩ :=
    exists_maximal_independent R s,
  let N := span R (range $ (s ∘ coe : I → M)), -- same as `span R (s '' I)` but more convenient
  let sI : I → N := λ i, ⟨s i.1, subset_span (mem_range_self i)⟩, -- `s` restricted to `I`
  have sI_basis : is_basis R sI, -- `s` restricted to `I` is a basis of `N`
    from is_basis_span indepI,
  have exists_a : ∀ i : ι, ∃ a : R, a ≠ 0 ∧ a • s i ∈ N,
  { intro i,
    by_cases hi : i ∈ I,
    { use [1, zero_ne_one.symm],
      rw one_smul,
      exact subset_span (mem_range_self (⟨i, hi⟩ : I)) },
    { simpa [image_eq_range s I] using hI i hi } },
  choose a ha ha' using exists_a,
  let A := ∏ i, a i,
  have ha : A ≠ 0,
  { rw finset.prod_ne_zero_iff,
    simpa using ha },
  let φ : M →ₗ[R] M := linear_map.smul_left M A,
  have : φ.ker = ⊥,
    from h.ker_smul_left ha,
  let ψ : M ≃ₗ[R] φ.range := linear_equiv.of_injective φ this,
  have : φ.range ≤ N,
  { suffices : ∀ i, φ (s i) ∈ N,
    { rw [linear_map.range, ← hs, φ.map_span_le],
      rintros _ ⟨i, rfl⟩, apply this },
    intro i,
    calc (∏ j, a j) • s i = (∏ j in finset.univ.erase i, a j) • a i • s i : by rw [fintype.prod_eq_prod_erase_mul i, mul_smul]
                      ... ∈ N  : N.smul_mem _ (ha' i) },
  obtain ⟨n, B : fin n → φ.range, hB : is_basis R B⟩ :=
    submodule.exists_is_basis_of_le this sI_basis,
  exact ⟨n, ψ.symm ∘ B, linear_equiv.is_basis hB ψ.symm⟩
end

[Patrick Massot]

We should probably also discuss introducing more definitions, like "finite type module" and "free module", but maybe not.

[Kevin Buzzard]

We've been waiting for this result for years :-)

[Patrick Massot]

Let me quote myself from yesterday: "Anne did all the hard work already"

[Patrick Massot]

The hard work is proving a submodule of a free module is free (with appropriate assumptions).

[Kevin Buzzard]

Related: the structure theorem for f.g. modules over a PID R says they're isomorphic to the direct sum of finitely many modules of the form R/(f) and one can go further to say something about uniqueness of the f's in question (this is a bit subtle and there are several approaches, but for example if you restrict the f's to be 0 or positive powers of irreducibles then the multiset is well defined up to associates). How close are we to this general statement?

[Patrick Massot]

There is an intermediate statement that is easy with what we now have: $M$ is isomorphic to $M/Tor(M) \oplus Tor(M)$, $M/Tor(M)$ is free and $Tor(M)$ is... torsion. Then the big piece is classification of torsion modules. This is indeed subtle, already with abelian groups. In the abelian group case there are shortcuts, but I'm not sure mathlib is interested in shortcuts.

[Kevin Buzzard]

We know the torsion-free quotient is free so we can deduce it's projective and hence the surjection splits :-) I think I made a PR about this recently!

[Kevin Buzzard]

#6813

[Patrick Massot]

I wasn't aware of this PR. With it the result is indeed even more within reach...

[Kevin Buzzard]

Oh I was only being half-serious: of course freeness implies the surjection splits immediately :-)

[Patrick Massot]

You should be careful when writing that anything is immediate in mathlib linear algebra.

[Anne Baanen]

Isn't the docs#no_zero_smul_divisors class the same as the definition of torsion_free above?

[Anne Baanen]

And linear_map.smul_left is called docs#linear_map.lsmul (see also docs#linear_map.lsmul_injective).

[Anne Baanen]

The proof of the final lemma is readable enough for a long tactic proof, I'd add a couple of comments highlighting the strategy ("let N be the submodule spanned by a maximal lin.ind. subset of s", "then there is an A such that ∀ x, A • x ∈ N", "the basis on N gives a basis on A • M, which gives a basis on M")

[Patrick Massot]

Thanks Anne. docs#no_zero_smul_divisors is indeed the correct definition, but with a very unfriendly name. I think we should at least write "torsion free" in the docstring. I did grep for torsion before writing my definition.

[Eric Wieser]

Should we add torsion_free as an abbreviation like we do with vector_space?

[Anne Baanen]

I know a slightly different definition of torsion-free: if c • x = 0, then x = 0 or c is a zero divisor. Of course, we should mention "torsion free" in no_zero_smul_divisors.

[Eric Wieser]

So [no_zero_divisors R] [torsion_free R M] would imply [no_zero_smul_divisors R M]?

[Johan Commelin]

Patrick Massot said:

We should probably also discuss introducing more definitions, like "finite type module" and "free module", but maybe not.

docs#module.finite already exists

[Kevin Buzzard]

I can quite believe that torsion-free becomes an ambiguous concept when the underlying ring has zero divisors

[Adam Topaz]

In general if $M$ is an $A$-module and $a \in A$ there is a canoniccal map $M/ann(a) \cdot M \to M$ given by $m \mapsto a \cdot m$. I guess the "correct(?)" general definition is to say that this map is injective for all $a \in A$? In this sense flat modules are torsion free in general.

[Adam Topaz]

(and over a principal ideal ring, flat is equivalent to torsion free with this definition)

[Patrick Massot]

I just checked my notes from my lecture in early December: as the very beginning of the section about Torsion I wrote that all rings in this section are domains.

[Kevin Buzzard]

It's like factoring perhaps -- you can try and struggle along to make some kind of a general theory, but if you can solve $xy=0$ in a non-trivial way then factoring is not going to be much fun.

[Patrick Massot]

Kevin, since you're here and I'm cleaning up this story before PRing, let me tell you about a trick you missed.

[Patrick Massot]

You wrote

import linear_algebra.basis
import order.zorn

open submodule set

lemma finset.exists_mem_subset_of_subset_bUnion_of_chain {α ι : Type*}
  (f : ι → set α)  (c : set ι) (a : ι) (hac : a ∈ c) (hc : zorn.chain (λ i j, f i ⊆ f j) c)
  (s : finset α) (hs : ↑s ⊆ (⋃ i ∈ c, f i)) : ∃ i ∈ c, ↑s ⊆ f i :=
sorry

lemma exists_maximal_independent' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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 X := { I : set ι // linear_independent R (s ∘ coe : I → M) },
  let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
  have trans : transitive r := λ I J K, set.subset.trans,
  obtain ⟨⟨I, hli⟩, hmax⟩ := @zorn.exists_maximal_of_chains_bounded _ r
    (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), _⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
  { exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩ },
  { rw linear_independent_comp_subtype,
    intros f hsupport hsum,
    -- `f` has finite support and `c` is a chain, so there must be an `I ∈ c`
    -- with `f.support ⊆ I`
    by_cases ha : ∃ a : X, a ∈ c,
    { cases ha with a hac,
      obtain ⟨I, I_mem, hI⟩ : ∃ I ∈ c, (↑f.support : set ι) ⊆ I :=
        finset.exists_mem_subset_of_subset_bUnion_of_chain _ c a hac hc f.support hsupport,
    exact linear_independent_comp_subtype.mp I.2 f hI hsum },
    { ext x,
      rw finsupp.mem_supported' at hsupport,
      apply hsupport,
      simp only [not_exists, exists_prop, set.mem_Union, not_and, exists_and_distrib_right, subtype.exists, subtype.coe_mk,
  exists_imp_distrib],
      intros S hS hc,
      exfalso,
      apply ha,
      use ⟨S, hS⟩, exact hc } },
end

lemma exists_maximal_independent'' {ι : Type*} (R : Type*) [comm_ring R]
  {M : Type*} [add_comm_group M] [module R M] (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 X := { I : set ι // linear_independent R (s ∘ coe : I → M) },
  let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
  have trans : transitive r := λ I J K, set.subset.trans,
  obtain ⟨⟨I, hli⟩, hmax⟩ := @zorn.exists_maximal_of_chains_bounded _ r
    (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), _⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
  { exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩ },
  { rw linear_independent_comp_subtype,
    intros f hsupport hsum,
    -- `f` has finite support and `c` is a chain, so there must be an `I ∈ c`
    -- with `f.support ⊆ I`
    by_cases ha : ∃ a : X, a ∈ c,
    { cases ha with a hac,
      obtain ⟨I, I_mem, hI⟩ : ∃ I ∈ c, (↑f.support : set ι) ⊆ I :=
        finset.exists_mem_subset_of_subset_bUnion_of_chain _ c a hac hc f.support hsupport,
    exact linear_independent_comp_subtype.mp I.2 f hI hsum },
    { ext x,
      rw finsupp.mem_supported' at hsupport,
      apply hsupport,
      simp only [not_exists, exists_prop, set.mem_Union, not_and, exists_and_distrib_right, subtype.exists, subtype.coe_mk,
  exists_imp_distrib],
      intros S hS hc,
      exfalso,
      apply ha,
      use ⟨S, hS⟩, exact hc } },
end

[Patrick Massot]

Note the line by_cases ha : ∃ a : X, a ∈ c,. The interesting case is of course the case where a exists. But the proof in the other case is much longer and painful.

[Kevin Buzzard]

Right -- this was to work around Anne's slightly false lemma.

[Patrick Massot]

Since about one year ago, we have a very nice pattern to deal with this. Replace the by_cases line with:

rcases eq_empty_or_nonempty c with rfl | ⟨a, hac⟩,

[Patrick Massot]

Note that goals now come in the reversed order (the empty case comes first).

[Patrick Massot]

But the whole proof in that annoying empty case is now: simpa using hsupport,

[Kevin Buzzard]

Oh nice!

[Kevin Buzzard]

Yeah I agree "there doesn't exist c" was not the most appealing way of saying that c was empty :-)

[Kevin Buzzard]

By the way, now you're here you can tell me what I'm doing wrong with push_neg in #general ;-)

[Patrick Massot]

I encourage you to put that code in the editor (I posted a mwe) and see the miracle occur to internalize it.

[Patrick Massot]

I'm still very slowly working towards PRing the code from this thread. I have a location problem with:

lemma finset.exists_mem_subset_of_subset_bUnion_of_chain {α ι : Type*}
  (f : ι → set α)  (c : set ι) (a : ι) (hac : a ∈ c) (hc : zorn.chain (λ i j, f i ⊆ f j) c)
  (s : finset α) (hs : ↑s ⊆ (⋃ i ∈ c, f i)) : ∃ i ∈ c, ↑s ⊆ f i :=

It needs finset and docs#zorn.chain. But it doesn't use anything Zorny apart from this definition. Where should it go? One option would be to but it in finset.basic but spell out the definition of zorn.chain, but it would make it less readable, especially since this definition is in term of docs#pairwise.pairwise_on which is not so common. @Mario Carneiro any opinion here?

[Patrick Massot]

Actually it also uses docs#zorn.chain.total_of_refl which is the very first lemma after the definition.

[Aaron Anderson]

I'm pretty sure the answer is to remove chain from the zorn namespace and file, but that's not very convenient in the middle of a different project

[Patrick Massot]

Actually I never realized we had this definition of chain avoiding to say anything about reflexivity of the relation.

[Aaron Anderson]

Actually, you could also use directed_on, because it’s true just assuming that

[Aaron Anderson]

And there might be something in the compactly_generated file that makes that obvious

[Patrick Massot]

That would be really nice!

[Patrick Massot]

But it's dinner time, so I'll investigate this later (unless you do it in the mean time).

[Aaron Anderson]

I don't actually think anything in that file will make this lemma obvious, but it would be good to prove the maximal independent family results at the compactly_generated generality.

[Greg Price]

Patrick Massot said:

Note for everyone: since the final lemma is pretty important, I tried to write it in a readable style. I'd be interested in people skipping everything and trying to read it, without tactic state help. Let me copy it again on its own:

I tried this out -- just reading the proof from your message, with no interaction with Lean. I found it generally quite readable, with a few rough spots.

The major rough spot was here:

  have : φ.range ≤ N,
  { suffices : ∀ i, φ (s i) ∈ N,
    { rw [linear_map.range, ← hs, φ.map_span_le],
      rintros _ ⟨i, rfl⟩, apply this },

It's not hard to see in a paper-proof sense why the first line follows from the second. But this was the one place where I found I really couldn't follow in my head what the steps in the proof were doing. I think the major reason is that I found it hard to guess what linear_map.range and φ.map_span_le meant.

[Kevin Buzzard]

linear_map.range will be the range (i.e. the image) of a linear map. We don't use "image" because we use image to mean the image of a subspace under the linear map; the range is the image of the full source space.

[Kevin Buzzard]

φ has type linear_map so φ.map_span_le means linear_map.map_span_le φ, and this function is defined in Patrick's code.

[Kevin Buzzard]

If you're looking at the code in VS Code then you can click within the brackets in the rw line and see how the goal is changing as the results are applied.

[Greg Price]

One minor rough spot was here:

  have ha : A ≠ 0,
  { rw finset.prod_ne_zero_iff,
    simpa using ha },

where at first glance it appears to be trying to do something circular. It's not, of course, but the name ha is being reused.

The remaining small rough spots were all just a matter of seeing a reference to some hypothesis by a very terse name, and having to search a ways up in the proof to find what it meant. This happens with h, hs, and ha' at least. In a paper proof, naturally those would be spelled more like "Because M is torsion-free,". Perhaps some names more in the style of sI_basis would help.

[Kevin Buzzard]

You are reading this proof within a VS Code session, right? These things are not written to be read by just staring at the code.

[Greg Price]

Certainly they often aren't, but Patrick had said he was interested in polishing this one to that level of readability.

[Kevin Buzzard]

The way I typically make this sort of stuff readable in that way is just to add in comments explaining the mathematical steps which are happening in the code.

[Greg Price]

Which I think is a nice thing to aim for when polishing a proof one likes, even though it probably isn't practical for the whole library.

[Kevin Buzzard]

I think that mathlib would be a better place if there were more comments in code!

[Greg Price]

Very likely!

[Kevin Buzzard]

Not for the mathematical trivialities (e.g. 3000 lines of lemmas about finsets all of which take 1 or 2 cryptic lines of term mode and all of which are obvious to a mathematician), but for the deeper stuff, so a human can read along without having to fire up VS Code.

[Kevin Buzzard]

See for example the way I teach Lean to mathematicians.

[Greg Price]

Where applicable I think it's better yet to have names that make clear the same thing that a comment would. So for example instead of h.ker_smul_left ha, -- here we use that M is torsion-free, one could write something like M_torsion_free.ker_smul_left ha.

[Kevin Buzzard]

You can't write that because here one is using dot notation -- this doesn't offer the flexibility which you're thinking about.

[Kevin Buzzard]

Oh I see -- I think you're suggesting more long-winded hypothesis names. Yes I do think you have a point -- I hardly ever use h, I usually use stuff like hxC to denote the hypothesis that x is in C etc.

[Greg Price]

No? I just mean using a different name for the hypothesis -- instead of h : torsion_free R M, to write M_torsion_free : torsion_free R M.

I suppose that example would be annoying because it shows up in the lemma's own interface, and it's repetitive there. But one can do that for an intermediate hypothesis like ha'.

[Kevin Buzzard]

Yes, I see and I agree that this would also make things more readable. I think I'd rather go for hM_tf and maybe establish some standard abbreviations for stuff like this.

[Greg Price]

Sure. Yeah, hM_tf would be quite a good hint in the context of that proof as to what the hypothesis meant.

[Patrick Massot]

@Greg Price thank you very much for do this and reporting back. I'm sorry about the ha name, I changed some variable names and forgot to rename that assumption. I'll change some other variable names to a more verbose style. I think every statement that we would call a theorem when lecturing in the real world deserves a readable proof in this sense. But this is very time consuming.

[Patrick Massot]

There are also interesting differences between what I wrote on paper and the Lean proof. The story of that Lean proof began during a conversation with Johan when he mentioned that Anne proved a submodule of a free module over a PID is free, but not this important corollary. I immediately knew this was an easy corollary because I lectured about it in December. When preparing this lecture I noted the key idea of introducing these N and (some version of) A but then I probably improvised the proof details. One interesting side effect of remote teaching is that I have a written trace of exactly what I wrote on "blackboard". I'm using xournal++ as a whiteboard and I simply save the resulting file at the end of the lecture. So I can tell you that, although the proof is only half a hand-written page long, it is far less efficient than what I wrote in Lean. The main thing is that instead of stating ∀ i : ι, ∃ a : R, a ≠ 0 ∧ a • s i ∈ N, I numbered the elements of a finite generating set $s_1, \dots, s_n, \dots, s_N$ assuming that $s_1, \dots, s_n$ was free and maximal, and I only stated and proved the existence of $a_i$ for $i > n$ (I even started with a completely useless case disjunction depending on whether $n = N$ or not). And then I wrote each element of $N$ as a linear combination of the $s_i$ and split all sums into two pieces, $i \leq n$ and $i > n$. And I certainly did not write the analogue of suffices : ∀ i, φ (s i) ∈ N,. I applied φ to a sum, split the sum, distributed etc.

[Patrick Massot]

Next year I'll teach this following the Lean proof.

[Johan Commelin]

@Patrick Massot cool story (-;

[Patrick Massot]

It makes me think I think I never wrote here that, in my secret topology course, I taught the construction of the Stone-Cech compactification following the Lean file in mathlib. Actually I probably have a version with slightly more readable proofs that I should PR, because I edited the proofs while reading them.

[Patrick Massot]

I also need to modify the wikipedia page which claims you can use ultrafilters only for discrete spaces (sure there are additional steps in the general case, but there is no reason to switch to a completely different story).

[Kevin Buzzard]

I taught the Hilbert basis theorem for several years in an MSc algebra course and when I tried to formalise it I ultimately realised that my proof was both really ugly and also incorrect. I formalised it shortly after polynomials in one variable had been formalised by Chris Hughes and I thought the proof would be a good test of the API. I realised the proof was ugly very quickly -- there was a step I always left to the reader and it was really messy to do in lean. I realised it was incorrect a bit later -- I was cursing Chris for not having formalised the simple lemma that the degree of X was equal to 1, and it was only when I gave up and decided to prove it myself that I discovered that it wasn't true (the base ring could be the zero ring, and in fact Chris had proved the result for nonzero rings). This incident made me rethink the entire proof and ultimately I came up with a much better and cleaner one which furthermore worked for the zero ring too :-)