## Stream: maths

### Topic: subgroup of free group is free

#### David Wärn (Mar 21 2020 at 11:52):

@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 (Mar 21 2020 at 13:13):

Is there any advantage in using parameters over variables?

#### Kevin Buzzard (Mar 21 2020 at 13:17):

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 (Mar 21 2020 at 13:20):

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

#### Johan Commelin (Mar 21 2020 at 13:28):

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

#### Johan Commelin (Mar 21 2020 at 13:29):

It would be really nice to have this in mathlib

#### Johan Commelin (Mar 21 2020 at 13:29):

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

#### Johan Commelin (Mar 21 2020 at 13:29):

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

#### Mario Carneiro (Mar 21 2020 at 13:32):

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

Great job!

#### David Wärn (Mar 21 2020 at 15:52):

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 (Mar 21 2020 at 15:57):

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 (Mar 21 2020 at 16:24):

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 (Mar 21 2020 at 16:33):

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 (Mar 21 2020 at 16:35):

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 (Mar 21 2020 at 16:35):

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

#### Kevin Buzzard (Mar 21 2020 at 16:37):

@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 (Mar 21 2020 at 16:37):

Just make the stuff you need for your proof.

#### David Wärn (Mar 13 2021 at 21:51):

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