Documentation

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

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

    Instances
      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

      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.

      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.
      Instances For

        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.

          Equations
          • =

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

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

          Equations
          • =