Zulip Chat Archive

Stream: maths

Topic: subgroup of free group is free


view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 13:13):

Is there any advantage in using parameters over variables?

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 13:20):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 21 2020 at 13:29):

It would be really nice to have this in mathlib

view this post on Zulip Johan Commelin (Mar 21 2020 at 13:29):

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

view this post on Zulip Johan Commelin (Mar 21 2020 at 13:29):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Mar 21 2020 at 14:44):

Great job!

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 21 2020 at 16:37):

Just make the stuff you need for your proof.

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:24):

Yes please!


Last updated: May 14 2021 at 19:21 UTC