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 tree T 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

def IsFreeGroupoid.Generators (G : Type u_1) [CategoryTheory.Groupoid G] : Type u_1

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

• IsFreeGroupoid.Generators G = G

class IsFreeGroupoid (G : Type u_1) [CategoryTheory.Groupoid G] : Type (max u_1 (v + 1))

A groupoid G is free when we have the following data:

• a quiver on IsFreeGroupoid.Generators G (a type synonym for G)

• a function of taking a generating arrow to a morphism in G

• such that a functor from G to any group X is uniquely determined by assigning labels in X to the generating arrows.

  This definition is nonstandard. Normally one would require that functors G ⥤ X to any groupoid X are given by graph homomorphisms from generators.

• 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

theorem IsFreeGroupoid.unique_lift {G : Type u_1} : ∀ {inst : CategoryTheory.Groupoid G} [self : IsFreeGroupoid G] {X : Type v} [inst_1 : 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

theorem IsFreeGroupoid.ext_functor {G : Type u_1} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] {X : Type v} [Group X] (f : CategoryTheory.Functor G (CategoryTheory.SingleObj X)) (g : CategoryTheory.Functor G (CategoryTheory.SingleObj X)) (h : ∀ (a b : IsFreeGroupoid.Generators G) (e : a ⟶ b), f.map (IsFreeGroupoid.of e) = g.map (IsFreeGroupoid.of e)) : f = g

Two functors from a free groupoid to a group are equal when they agree on the generating quiver.

instance IsFreeGroupoid.actionGroupoidIsFree {G : Type u} {A : Type u} [Group G] [IsFreeGroup G] [MulAction G A] : IsFreeGroupoid (CategoryTheory.ActionCategory G A)

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.

def IsFreeGroupoid.SpanningTree.homOfPath {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : G} : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a → (IsFreeGroupoid.SpanningTree.root' T ⟶ a)

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)

def IsFreeGroupoid.SpanningTree.treeHom {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] (a : G) : IsFreeGroupoid.SpanningTree.root' T ⟶ a

For every vertex a, there is a canonical hom from the root, given by the path in the tree.

Equations

• IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T default

theorem IsFreeGroupoid.SpanningTree.treeHom_eq {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : G} (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a) : IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T p

Any path to a gives treeHom T a, since paths in the tree are unique.

@[simp]

theorem IsFreeGroupoid.SpanningTree.treeHom_root {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] : IsFreeGroupoid.SpanningTree.treeHom T (IsFreeGroupoid.SpanningTree.root' T) = CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root' T)

def IsFreeGroupoid.SpanningTree.loopOfHom {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : G} {b : G} (p : a ⟶ b) : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T)

Any hom in G can be made into a loop, by conjugating with treeHoms.

Equations

• One or more equations did not get rendered due to their size.

theorem IsFreeGroupoid.SpanningTree.loopOfHom_eq_id {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : IsFreeGroupoid.Generators G} {b : IsFreeGroupoid.Generators G} (e : a ⟶ b) (H : e ∈ Quiver.wideSubquiverSymmetrify T a b) : IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e) = CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root' T)

Turning an edge in the spanning tree into a loop gives the identity loop.

def IsFreeGroupoid.SpanningTree.functorOfMonoidHom {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {X : Type u_1} [Monoid X] (f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T) →* X) : CategoryTheory.Functor G (CategoryTheory.SingleObj X)

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.

@[simp]

theorem IsFreeGroupoid.SpanningTree.functorOfMonoidHom_obj {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {X : Type u_1} [Monoid X] (f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T) →* X) : ∀ (x : G), (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f).obj x = ()

@[simp]

theorem IsFreeGroupoid.SpanningTree.functorOfMonoidHom_map {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {X : Type u_1} [Monoid X] (f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T) →* X) : ∀ {X_1 Y : G} (p : X_1 ⟶ Y), (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f).map p = f (IsFreeGroupoid.SpanningTree.loopOfHom T p)

theorem IsFreeGroupoid.SpanningTree.endIsFree {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] : IsFreeGroup (CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T))

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.

theorem IsFreeGroupoid.path_nonempty_of_hom {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] {a : G} {b : G} : Nonempty (a ⟶ b) → Nonempty (Quiver.Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))

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.

instance IsFreeGroupoid.generators_connected (G : Type u) [CategoryTheory.Groupoid G] [CategoryTheory.IsConnected G] [IsFreeGroupoid G] (r : G) : Quiver.RootedConnected (IsFreeGroupoid.symgen r)

Given a connected free groupoid, its generating quiver is rooted-connected.

Equations

• ⋯ = ⋯

instance IsFreeGroupoid.endIsFreeOfConnectedFree {G : Type u} [CategoryTheory.Groupoid G] [CategoryTheory.IsConnected G] [IsFreeGroupoid G] (r : G) : IsFreeGroup (CategoryTheory.End r)

A vertex group in a free connected groupoid is free. With some work one could drop the connectedness assumption, by looking at connected components.

Equations

• ⋯ = ⋯

instance subgroupIsFreeOfIsFree {G : Type u} [Group G] [IsFreeGroup G] (H : Subgroup G) : IsFreeGroup ↥H

The Nielsen-Schreier theorem: a subgroup of a free group is free.

Equations

• ⋯ = ⋯