## Stream: maths

### Topic: maximal independent family

#### Patrick Massot (Apr 01 2021 at 18:29):

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 (Apr 01 2021 at 18:30):

@Anne Baanen maybe?

#### Heather Macbeth (Apr 01 2021 at 18:32):

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 (Apr 01 2021 at 18:43):

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

#### Julian Berman (Apr 01 2021 at 18:51):

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 (Apr 01 2021 at 19:01):

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 (Apr 01 2021 at 19:08):

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

#### Adam Topaz (Apr 01 2021 at 19:10):

docs#finset.preimage

#### Kevin Buzzard (Apr 01 2021 at 19:10):

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

lol

#### Johan Commelin (Apr 01 2021 at 19:12):

There's finset.map and finset.image.

#### Adam Topaz (Apr 01 2021 at 19:13):

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

#### Johan Commelin (Apr 01 2021 at 19:22):

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

Oh I see.

#### Patrick Massot (Apr 01 2021 at 19:39):

I'm back, where is my proof?

#### Patrick Massot (Apr 01 2021 at 19:40):

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

#### Kevin Buzzard (Apr 01 2021 at 19:40):

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 (Apr 01 2021 at 19:40):

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 (Apr 01 2021 at 19:41):

You eat quickly for a Frenchman

#### Heather Macbeth (Apr 01 2021 at 19:41):

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 (Apr 01 2021 at 19:42):

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 (Apr 01 2021 at 19:46):

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 (Apr 01 2021 at 20:03):

We have docs#exists_linear_independent for division_rings

#### Heather Macbeth (Apr 01 2021 at 20:05):

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

#### Patrick Massot (Apr 01 2021 at 20:10):

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 (Apr 01 2021 at 20:11):

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

#### Yury G. Kudryashov (Apr 01 2021 at 20:11):

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

#### Sebastien Gouezel (Apr 01 2021 at 20:12):

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 (Apr 01 2021 at 20:14):

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 (Apr 01 2021 at 20:15):

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

#### Heather Macbeth (Apr 01 2021 at 20:15):

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

#### Yury G. Kudryashov (Apr 01 2021 at 20:15):

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 (Apr 01 2021 at 20:16):

@Patrick Massot Can you wait till tomorrow morning?

#### Yury G. Kudryashov (Apr 01 2021 at 20:17):

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

#### Patrick Massot (Apr 01 2021 at 20:18):

I can definitely wait for tomorrow morning.

#### Patrick Massot (Apr 01 2021 at 20:20):

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 (Apr 01 2021 at 20:31):

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 (Apr 01 2021 at 20:32):

I'll have a look at that part

#### Kevin Buzzard (Apr 01 2021 at 20:34):

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 (Apr 01 2021 at 20:35):

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 (Apr 01 2021 at 20:57):

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 (Apr 01 2021 at 21:07):

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 (Apr 01 2021 at 21:09):

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 (Apr 01 2021 at 21:21):

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 _ _),
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 (Apr 01 2021 at 21:23):

Now we just need to do Zorn

#### Kevin Buzzard (Apr 01 2021 at 21:32):

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

#### Anne Baanen (Apr 01 2021 at 21:38):

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 _ _),
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 (Apr 01 2021 at 21:42):

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 (Apr 01 2021 at 21:49):

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 (Apr 01 2021 at 21:52):

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 _ _),
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 (Apr 01 2021 at 21:54):

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

#### Kevin Buzzard (Apr 01 2021 at 22:17):

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 (Apr 01 2021 at 22:20):

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

#### Eric Rodriguez (Apr 02 2021 at 01:41):

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 (Apr 02 2021 at 09:51):

Thanks everybody, you are wonderful!

#### Patrick Massot (Apr 02 2021 at 09:53):

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 _ _),
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,

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 (Apr 02 2021 at 09:55): 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 (Apr 02 2021 at 09:57):

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

#### Kevin Buzzard (Apr 02 2021 at 09:57):

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

#### Patrick Massot (Apr 02 2021 at 10:00):

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

#### Patrick Massot (Apr 02 2021 at 10:00):

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

#### Kevin Buzzard (Apr 02 2021 at 10:05):

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 (Apr 02 2021 at 11:28):

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 (Apr 02 2021 at 11:43):

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!

#6813

#### Patrick Massot (Apr 02 2021 at 13:16):

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

#### Kevin Buzzard (Apr 02 2021 at 13:16):

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

#### Patrick Massot (Apr 02 2021 at 13:18):

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

#### Anne Baanen (Apr 02 2021 at 15:05):

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

#### Anne Baanen (Apr 02 2021 at 15:11):

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

#### Anne Baanen (Apr 02 2021 at 15:25):

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 (Apr 02 2021 at 17:26):

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 (Apr 02 2021 at 17:52):

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

#### Anne Baanen (Apr 02 2021 at 18:14):

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 (Apr 02 2021 at 18:25):

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

#### Johan Commelin (Apr 02 2021 at 18:48):

Patrick Massot said:

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

#### Kevin Buzzard (Apr 02 2021 at 20:21):

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

#### Adam Topaz (Apr 02 2021 at 20:25):

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 (Apr 02 2021 at 21:28):

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

#### Patrick Massot (Apr 03 2021 at 12:27):

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 (Apr 03 2021 at 12:28):

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 (Apr 03 2021 at 12:31):

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 (Apr 03 2021 at 12:31):

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 (Apr 03 2021 at 12:32):

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 (Apr 03 2021 at 12:33):

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

#### Patrick Massot (Apr 03 2021 at 12:33):

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 (Apr 03 2021 at 12:33):

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

#### Patrick Massot (Apr 03 2021 at 12:34):

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

Oh nice!

#### Kevin Buzzard (Apr 03 2021 at 12:34):

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

#### Kevin Buzzard (Apr 03 2021 at 12:34):

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

#### Patrick Massot (Apr 03 2021 at 12:35):

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

#### Patrick Massot (Apr 04 2021 at 16:57):

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 (Apr 04 2021 at 17:00):

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

#### Aaron Anderson (Apr 04 2021 at 17:04):

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 (Apr 04 2021 at 17:04):

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

#### Aaron Anderson (Apr 04 2021 at 17:22):

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

#### Aaron Anderson (Apr 04 2021 at 17:22):

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

#### Patrick Massot (Apr 04 2021 at 17:23):

That would be really nice!

#### Patrick Massot (Apr 04 2021 at 17:25):

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

#### Aaron Anderson (Apr 04 2021 at 17:52):

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 (Apr 04 2021 at 23:11):

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 (Apr 04 2021 at 23:13):

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 (Apr 04 2021 at 23:14):

φ 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 (Apr 04 2021 at 23:15):

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 (Apr 04 2021 at 23:16):

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 (Apr 04 2021 at 23:17):

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 (Apr 04 2021 at 23:18):

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

#### Kevin Buzzard (Apr 04 2021 at 23:19):

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 (Apr 04 2021 at 23:19):

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 (Apr 04 2021 at 23:19):

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

Very likely!

#### Kevin Buzzard (Apr 04 2021 at 23:20):

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 (Apr 04 2021 at 23:22):

See for example the way I teach Lean to mathematicians.

#### Greg Price (Apr 04 2021 at 23:22):

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 (Apr 04 2021 at 23:22):

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 (Apr 04 2021 at 23:24):

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 (Apr 04 2021 at 23:24):

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 (Apr 04 2021 at 23:25):

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 (Apr 04 2021 at 23:26):

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

#### Patrick Massot (Apr 05 2021 at 09:45):

@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 (Apr 05 2021 at 10:08):

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 (Apr 05 2021 at 10:08):

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

#### Johan Commelin (Apr 05 2021 at 10:48):

@Patrick Massot cool story (-;

#### Patrick Massot (Apr 05 2021 at 10:58):

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 (Apr 05 2021 at 11:00):

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 (Apr 05 2021 at 11:56):

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 :-)

Last updated: May 06 2021 at 19:30 UTC