mathlib3 documentation

group_theory.nielsen_schreier

The Nielsen-Schreier theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main result #

subgroup_is_free_of_is_free 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,

is_free_groupoid G corresponds to saying that a space is a graph.
End_mul_equiv_subgroup H plays the role of replacing 'subgroup of fundamental group' with 'fundamental group of covering space'.
action_groupoid_is_free G A corresponds to the fact that a covering of a (single-vertex) graph is a graph.
End_is_free 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 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 #

https://ncatlab.org/nlab/show/Nielsen-Schreier+theorem

Tags #

free group, free groupoid, Nielsen-Schreier

@[nolint]

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.

Equations

is_free_groupoid.generators G = G

Instances for is_free_groupoid.generators

is_free_groupoid.quiver_generators

@[class]

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

Type (max u_1 (v+1))

quiver_generators : quiver (is_free_groupoid.generators G)
of : Π {a b : is_free_groupoid.generators G}, (a ⟶ b) → ((show G, from a) ⟶ b)
unique_lift : ∀ {X : Type ?} [_inst_1_1 : group X] (f : quiver.labelling (is_free_groupoid.generators G) X), ∃! (F : G ⥤ category_theory.single_obj X), ∀ (a b : is_free_groupoid.generators G) (g : a ⟶ b), F.map (is_free_groupoid.of g) = f g

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.

Instances of this typeclass

is_free_groupoid.action_groupoid_is_free

Instances of other typeclasses for is_free_groupoid

is_free_groupoid.has_sizeof_inst

@[ext]

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), f.map (is_free_groupoid.of e) = g.map (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.

@[protected, instance]

def is_free_groupoid.action_groupoid_is_free {G A : Type u} [group G] [is_free_group G] [mul_action G A] :

is_free_groupoid (category_theory.action_category 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

is_free_groupoid.action_groupoid_is_free = {quiver_generators := {hom := λ (a b : is_free_groupoid.generators (category_theory.action_category G A)), {e // is_free_group.of e • category_theory.action_category.back a = category_theory.action_category.back b}}, of := λ (a b : is_free_groupoid.generators (category_theory.action_category G A)) (e : a ⟶ b), ⟨is_free_group.of ↑e, _⟩, unique_lift := _}

noncomputable def is_free_groupoid.spanning_tree.hom_of_path {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] {a : G} :

quiver.path (quiver.root ↥T) a → (root' T ⟶ a)

A path in the tree gives a hom, by composition.

Equations

is_free_groupoid.spanning_tree.hom_of_path T (p.cons f) = is_free_groupoid.spanning_tree.hom_of_path T p ≫ sum.rec_on f.val (λ (e : a_6 ⟶ a), is_free_groupoid.of e) (λ (e : a ⟶ a_6), category_theory.inv (is_free_groupoid.of e))
is_free_groupoid.spanning_tree.hom_of_path T quiver.path.nil = 𝟙 (root' T)

noncomputable def is_free_groupoid.spanning_tree.tree_hom {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] (a : G) :

root' T ⟶ a

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

Equations

is_free_groupoid.spanning_tree.tree_hom T a = is_free_groupoid.spanning_tree.hom_of_path T inhabited.default

theorem is_free_groupoid.spanning_tree.tree_hom_eq {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] {a : G} (p : quiver.path (quiver.root ↥T) a) :

is_free_groupoid.spanning_tree.tree_hom T a = is_free_groupoid.spanning_tree.hom_of_path T p

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

@[simp]

theorem is_free_groupoid.spanning_tree.tree_hom_root {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] :

is_free_groupoid.spanning_tree.tree_hom T (root' T) = 𝟙 (root' T)

noncomputable def is_free_groupoid.spanning_tree.loop_of_hom {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] {a b : G} (p : a ⟶ b) :

category_theory.End (root' T)

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

Equations

is_free_groupoid.spanning_tree.loop_of_hom T p = is_free_groupoid.spanning_tree.tree_hom T a ≫ p ≫ category_theory.inv (is_free_groupoid.spanning_tree.tree_hom T b)

theorem is_free_groupoid.spanning_tree.loop_of_hom_eq_id {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] {a b : is_free_groupoid.generators G} (e : a ⟶ b) (H : e ∈ quiver.wide_subquiver_symmetrify T a b) :

is_free_groupoid.spanning_tree.loop_of_hom T (is_free_groupoid.of e) = 𝟙 (root' T)

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

noncomputable def is_free_groupoid.spanning_tree.functor_of_monoid_hom {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] {X : Type u_1} [monoid X] (f : category_theory.End (root' T) →* X) :

G ⥤ category_theory.single_obj 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

is_free_groupoid.spanning_tree.functor_of_monoid_hom T f = {obj := λ (_x : G), unit.star(), map := λ (a b : G) (p : a ⟶ b), ⇑f (is_free_groupoid.spanning_tree.loop_of_hom T p), map_id' := _, map_comp' := _}

@[simp]

theorem is_free_groupoid.spanning_tree.functor_of_monoid_hom_map {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] {X : Type u_1} [monoid X] (f : category_theory.End (root' T) →* X) (a b : G) (p : a ⟶ b) :

(is_free_groupoid.spanning_tree.functor_of_monoid_hom T f).map p = ⇑f (is_free_groupoid.spanning_tree.loop_of_hom T p)

@[simp]

theorem is_free_groupoid.spanning_tree.functor_of_monoid_hom_obj {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] {X : Type u_1} [monoid X] (f : category_theory.End (root' T) →* X) (_x : G) :

(is_free_groupoid.spanning_tree.functor_of_monoid_hom T f).obj _x = unit.star()

noncomputable def is_free_groupoid.spanning_tree.End_is_free {G : Type u} [category_theory.groupoid G] [is_free_groupoid G] (T : wide_subquiver (quiver.symmetrify (is_free_groupoid.generators G))) [quiver.arborescence ↥T] :

is_free_group (category_theory.End (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.

Equations

is_free_groupoid.spanning_tree.End_is_free T = is_free_group.of_unique_lift ↥(⇑quiver.wide_subquiver_equiv_set_total (quiver.wide_subquiver_symmetrify T))ᶜ (λ (e : ↥(⇑quiver.wide_subquiver_equiv_set_total (quiver.wide_subquiver_symmetrify T))ᶜ), is_free_groupoid.spanning_tree.loop_of_hom T (is_free_groupoid.of e.val.hom)) _

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.

@[protected, instance]

def is_free_groupoid.generators_connected (G : Type u) [category_theory.groupoid G] [category_theory.is_connected G] [is_free_groupoid G] (r : G) :

quiver.rooted_connected (symgen r)

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

@[protected, instance]

noncomputable def is_free_groupoid.End_is_free_of_connected_free {G : Type u_1} [category_theory.groupoid G] [category_theory.is_connected G] [is_free_groupoid G] (r : G) :

is_free_group (category_theory.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

is_free_groupoid.End_is_free_of_connected_free r = is_free_groupoid.spanning_tree.End_is_free (quiver.geodesic_subtree (symgen r))

@[protected, instance]

noncomputable def subgroup_is_free_of_is_free {G : Type u} [group G] [is_free_group G] (H : subgroup G) :

is_free_group ↥H

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

Equations

subgroup_is_free_of_is_free H = is_free_group.of_mul_equiv (category_theory.action_category.End_mul_equiv_subgroup H)