The Nielsen-Schreier theorem #
This file proves that a subgroup of a free group is itself free.
Main result #
subgroupIsFreeOfIsFree H
: an instance saying that a subgroup of a free group is free.
Proof overview #
The proof is analogous to the proof using covering spaces and fundamental groups of graphs, but we work directly with groupoids instead of topological spaces. Under this analogy,
IsFreeGroupoid G
corresponds to saying that a space is a graph.endMulEquivSubgroup H
plays the role of replacing 'subgroup of fundamental group' with 'fundamental group of covering space'.actionGroupoidIsFree G A
corresponds to the fact that a covering of a (single-vertex) graph is a graph.endIsFree T
corresponds to the fact that, given a spanning treeT
of a graph, its fundamental group is free (generated by loops from the complement of the tree).
Implementation notes #
Our definition of IsFreeGroupoid
is nonstandard. Normally one would require that functors
G ⥤ X
to any groupoid X
are given by graph homomorphisms from the generators, but we only
consider groups X
. This simplifies the argument since functor equality is complicated in
general, but simple for functors to single object categories.
References #
https://ncatlab.org/nlab/show/Nielsen-Schreier+theorem
Tags #
free group, free groupoid, Nielsen-Schreier
IsFreeGroupoid.Generators G
is a type synonym for G
. We think of this as
the vertices of the generating quiver of G
when G
is free. We can't use G
directly,
since G
already has a quiver instance from being a groupoid.
Equations
Instances For
A groupoid G
is free when we have the following data:
a quiver on
IsFreeGroupoid.Generators G
(a type synonym forG
)a function
of
taking a generating arrow to a morphism inG
such that a functor from
G
to any groupX
is uniquely determined by assigning labels inX
to the generating arrows.This definition is nonstandard. Normally one would require that functors
G ⥤ X
to any groupoidX
are given by graph homomorphisms fromgenerators
.
- quiverGenerators : Quiver (IsFreeGroupoid.Generators G)
- of : {a b : IsFreeGroupoid.Generators G} → (a ⟶ b) → ((let_fun this := a; this) ⟶ b)
- unique_lift : ∀ {X : Type v} [inst : Group X] (f : Quiver.Labelling (IsFreeGroupoid.Generators G) X), ∃! F : CategoryTheory.Functor G (CategoryTheory.SingleObj X), ∀ (a b : IsFreeGroupoid.Generators G) (g : a ⟶ b), F.map (IsFreeGroupoid.of g) = f g
Instances
Two functors from a free groupoid to a group are equal when they agree on the generating quiver.
An action groupoid over a free group is free. More generally, one could show that the groupoid of elements over a free groupoid is free, but this version is easier to prove and suffices for our purposes.
Analogous to the fact that a covering space of a graph is a graph. (A free groupoid is like a graph, and a groupoid of elements is like a covering space.)
Equations
- One or more equations did not get rendered due to their size.
A path in the tree gives a hom, by composition.
Equations
- One or more equations did not get rendered due to their size.
- IsFreeGroupoid.SpanningTree.homOfPath T Quiver.Path.nil = CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)
Instances For
For every vertex a
, there is a canonical hom from the root, given by the path in the tree.
Equations
Instances For
Any path to a
gives treeHom T a
, since paths in the tree are unique.
Any hom in G
can be made into a loop, by conjugating with treeHom
s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turning an edge in the spanning tree into a loop gives the identity loop.
Since a hom gives a loop, any homomorphism from the vertex group at the root extends to a functor on the whole groupoid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a free groupoid and an arborescence of its generating quiver, the vertex group at the root is freely generated by loops coming from generating arrows in the complement of the tree.
If there exists a morphism a → b
in a free groupoid, then there also exists a zigzag
from a
to b
in the generating quiver.
Given a connected free groupoid, its generating quiver is rooted-connected.
A vertex group in a free connected groupoid is free. With some work one could drop the connectedness assumption, by looking at connected components.
The Nielsen-Schreier theorem: a subgroup of a free group is free.