Stallings graphs of finitely generated subgroups

Starting with the flower of a finite list of words, a finite sequence of folds produces a folded graph. Taking its based core gives a finite connected folded core graph which reads exactly the subgroup generated by the words. The construction chooses a terminal fold sequence; uniqueness up to based labelled isomorphism is a separate property of folded cores. Every finitely generated subgroup of a free group arises in this way.

References

• I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, Section 3, Proposition 3.8, and Section 7, Proposition 7.1.

noncomputable def TauCeti.StallingsGraph.foldedFlower {α : Type u} (ws : List (List (α × Bool))) : StallingsGraph α

A terminal finite folding of the flower of a list of words.

theorem TauCeti.StallingsGraph.flower_foldSequence {α : Type u} (ws : List (List (α × Bool))) : (flower ws).FoldSequence (foldedFlower ws)

The chosen folding is reached from the flower by finitely many folds.

theorem TauCeti.StallingsGraph.foldedFlower_isFolded {α : Type u} (ws : List (List (α × Bool))) : (foldedFlower ws).IsFolded

The chosen terminal folding has no two equally labelled outgoing darts.

noncomputable def TauCeti.StallingsGraph.stallingsGraph {α : Type u} (ws : List (List (α × Bool))) : StallingsGraph α

The based core of a terminal folding of the flower. Its base vertex is retained, including when it lies at the end of a stem.

instance TauCeti.StallingsGraph.stallingsGraph_finite_vertex {α : Type u} (ws : List (List (α × Bool))) : Finite (stallingsGraph ws).graph.V

The Stallings graph has finitely many vertices.

instance TauCeti.StallingsGraph.stallingsGraph_finite_dart {α : Type u} (ws : List (List (α × Bool))) : Finite (stallingsGraph ws).graph.E

The Stallings graph has finitely many darts.

theorem TauCeti.StallingsGraph.stallingsGraph_isFolded {α : Type u} (ws : List (List (α × Bool))) : (stallingsGraph ws).IsFolded

The Stallings graph is folded.

theorem TauCeti.StallingsGraph.stallingsGraph_isCore {α : Type u} (ws : List (List (α × Bool))) : (stallingsGraph ws).graph.IsCore (stallingsGraph ws).base

Every vertex of the Stallings graph lies on a reduced based closed path.

theorem TauCeti.StallingsGraph.stallingsGraph_connected {α : Type u} (ws : List (List (α × Bool))) : (stallingsGraph ws).graph.Connected

The Stallings graph is connected, including for the empty list of words.

theorem TauCeti.StallingsGraph.subgroup_stallingsGraph {α : Type u} (ws : List (List (α × Bool))) : (stallingsGraph ws).subgroup (stallingsGraph ws).base = Subgroup.closure {g : FreeGroup α | ∃ w ∈ ws, FreeGroup.mk w = g}

The subgroup read at the base of the Stallings graph is generated by the input words.

@[simp]

theorem TauCeti.StallingsGraph.subgroup_stallingsGraph_nil (α : Type u) : (stallingsGraph []).subgroup (stallingsGraph []).base = ⊥

The Stallings graph of the empty generating list accepts the trivial subgroup.

theorem TauCeti.StallingsGraph.exists_subgroup_stallingsGraph_eq {α : Type u} {H : Subgroup (FreeGroup α)} (hH : H.FG) : ∃ (ws : List (List (α × Bool))), (stallingsGraph ws).subgroup (stallingsGraph ws).base = H

Every finitely generated subgroup of a free group is accepted at the base vertex of the Stallings graph of some finite list of words.