mathlib documentation


The Nielsen-Schreier theorem #

This file proves that a subgroup of a free group is itself free.

Main result #

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,

Implementation notes #

Our definition of is_free_groupoid 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 #

Tags #

free group, free groupoid, Nielsen-Schreier

def is_free_groupoid.generators (G : Type u_1) [category_theory.groupoid G] :
Type u_1

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

structure is_free_groupoid (G : Type u_1) [category_theory.groupoid G] :
Type (max u_1 (v+1))

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

  • a quiver on is_free_groupoid.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.

theorem is_free_groupoid.ext_functor {G : Type u_1} [category_theory.groupoid G] [is_free_groupoid G] {X : Type v} [group X] (f g : G category_theory.single_obj X) (h : ∀ (a b : is_free_groupoid.generators G) (e : a b), (is_free_groupoid.of e) = (is_free_groupoid.of e)) :
f = g

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


An action groupoid over a free froup 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.)


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


Since a hom gives a loop, any homomorphism from the vertex group at the root extends to a functor on the whole groupoid.

theorem is_free_groupoid.path_nonempty_of_hom {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] {a b : G} :
nonempty (a b)nonempty (quiver.path (symgen a) (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.


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.