subgroup of free group is free

Stream: maths

[David Wärn]

@nielsen_schreier : Π {α : Type} (H : set (free_group α)) [is_subgroup H],
  ∃ (R : Type), nonempty (H ≃* free_group R) ∧ nonempty (quotient H × α ⊕ unit ≃ quotient H ⊕ R)

A while ago I decided to try to prove the Nielsen-Schreier theorem on free groups to get more familiar with Lean. Now, after countless days of self-isolation, I have a working proof. Comments welcome!

[Kevin Buzzard]

Is there any advantage in using parameters over variables?

[Kevin Buzzard]

non-terminal simps are discouraged in general, because they can cause trouble with maintenance. There are workarounds (e.g. run simp and then see what the goal has become, and try something like suffices : <new goal>, from simpa using this)

[Kevin Buzzard]

We are in the process of moving to bundled subgroups rather than is_subgroup

[Johan Commelin]

@David Wärn Nice work! At a first glance, a lot of the stuff there looks quite well done.

[Johan Commelin]

It would be really nice to have this in mathlib

[Johan Commelin]

But like you say, you might want to factor out some parts

[Johan Commelin]

Unfortunately we don't have any graph theory yet...

[Mario Carneiro]

I think it would be nice to have a predicate that asserts that a group is freely generated by a subset of its type, so that we can quantify over subsets of H here instead of arbitrary types

[Bhavik Mehta]

Great job!

[David Wärn]

Kevin Buzzard said:

Is there any advantage in using parameters over variables?

I think I chose parameters to try to convey the meaning of keeping things fixed, but variables might be better (at least it would let me use some lemmas for the two different free groups that occur in the argument)

[David Wärn]

Mario Carneiro said:

I think it would be nice to have a predicate that asserts that a group is freely generated by a subset of its type, so that we can quantify over subsets of H here instead of arbitrary types

That would be nice. You'd just need to prove that an isomorphism with a free group gives a freely generating subset

[David Wärn]

Johan Commelin said:

It would be really nice to have this in mathlib

I'll think about making this mathlib-friendly. Would it be worth it to create a small graph theory section with the proof of existence of spanning trees? The characterisation of spanning trees I used is somewhat non-standard: Basically I think of it as a rooted tree where I can do recursion along the edges.

[Patrick Massot]

I think we should stop complaining that there are many possible ways to formalize graphs and trees. We should go ahead, put them in mathlib, and we'll refactor (or add parallel implementations) if needed.

[Kevin Buzzard]

There are many possible ways to formalise algebra stuff -- there are groups, rings, fields etc and we just formalised all of them and proved the links between them. "Graphs" feel the same to me -- it is a catch-all word which can mean many things, and they should all be in.

[Kevin Buzzard]

it's only when they're in that we start realising how we should have done it.

[Kevin Buzzard]

@David Wärn why don't you start by just making a basic graph API and PR'ing it? This is how I started. I wrote a basic complex numbers API and PR'ed it, and I think that by the end of the process none of the lines of code I had originally written were left.

[Kevin Buzzard]

Just make the stuff you need for your proof.

[David Wärn]

Ok, I have had a bit of a think about this, and arrived at this new and improved proof. This version is very modular, uses universal properties rather than explicit constructions, and is still reasonably short. I think it would be relatively straightforward to move this into mathlib (presumably starting with a PR containing the definition of quivers).

[Scott Morrison]

Yes please!