Finite Stallings folding

A fold of two distinct equally labelled darts strictly decreases the number of darts. Consequently a finite labelled graph admits a finite sequence of folds ending in a folded graph. Every step preserves the subgroup read at the base vertex. This is the termination step in the construction of a finite folded graph from a flower of generating words. The fold sequence yields a surjective quotient morphism to the folded graph.

References

• I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, Section 2, Lemma 2.5 and Section 3, Proposition 3.8.

def TauCeti.StallingsGraph.FoldStep {α : Type u} (S T : StallingsGraph α) : Prop

A single fold of distinct equally labelled darts with the same source.

theorem TauCeti.StallingsGraph.foldStep_iff {α : Type u} (S T : StallingsGraph α) : S.FoldStep T ↔ ∃ (e : S.graph.E) (f : S.graph.E) (hsrc : S.graph.src e = S.graph.src f) (hlabel : S.label e = S.label f), e ≠ f ∧ T = S.foldAt e f hsrc hlabel

Characterize a fold step by its two distinct darts and the resulting quotient.

@[reducible, inline]

abbrev TauCeti.StallingsGraph.FoldSequence {α : Type u} (S T : StallingsGraph α) : Prop

A finite sequence of Stallings folds, including the empty sequence.

theorem TauCeti.StallingsGraph.FoldSequence.subgroup_base {α : Type u} {S T : StallingsGraph α} (h : S.FoldSequence T) : T.subgroup T.base = S.subgroup S.base

A finite fold sequence preserves the subgroup accepted at the base vertex.

theorem TauCeti.StallingsGraph.FoldSequence.finite_V {α : Type u} {S T : StallingsGraph α} (h : S.FoldSequence T) [Finite S.graph.V] : Finite T.graph.V

A finite fold sequence preserves finiteness of vertices.

theorem TauCeti.StallingsGraph.FoldSequence.finite_E {α : Type u} {S T : StallingsGraph α} (h : S.FoldSequence T) [Finite S.graph.E] : Finite T.graph.E

A finite fold sequence preserves finiteness of darts.

theorem TauCeti.StallingsGraph.FoldSequence.connected {α : Type u} {S T : StallingsGraph α} (h : S.FoldSequence T) (hS : S.graph.Connected) : T.graph.Connected

A finite fold sequence preserves connectedness.

theorem TauCeti.StallingsGraph.FoldSequence.exists_surjective_hom {α : Type u} {S T : StallingsGraph α} (h : S.FoldSequence T) : ∃ (f : S.Hom T), Function.Surjective f.graphHom.mapV ∧ Function.Surjective f.graphHom.mapE

A sequence of folds has a quotient morphism surjective on vertices and darts.

theorem TauCeti.StallingsGraph.card_foldAt_lt {α : Type u} (S : StallingsGraph α) [Finite S.graph.E] (e f : S.graph.E) (hne : e ≠ f) (hsrc : S.graph.src e = S.graph.src f) (hlabel : S.label e = S.label f) : Nat.card (S.foldAt e f hsrc hlabel).graph.E < Nat.card S.graph.E

Folding distinct darts strictly decreases the number of darts.

theorem TauCeti.StallingsGraph.exists_foldSequence_isFolded {α : Type u} (S : StallingsGraph α) [Finite S.graph.E] : ∃ (T : StallingsGraph α), S.FoldSequence T ∧ T.IsFolded

A finite labelled graph can be folded by a finite sequence of quotients.

theorem TauCeti.StallingsGraph.exists_folded_quotient {α : Type u} (S : StallingsGraph α) [Finite S.graph.V] [Finite S.graph.E] : ∃ (T : StallingsGraph α), Finite T.graph.V ∧ Finite T.graph.E ∧ ∃ (f : S.Hom T), T.IsFolded ∧ Function.Surjective f.graphHom.mapV ∧ Function.Surjective f.graphHom.mapE ∧ T.subgroup T.base = S.subgroup S.base ∧ (S.graph.Connected → T.graph.Connected)

Every finite labelled graph has a finite folded quotient with the same accepted subgroup. The quotient map is surjective on vertices and darts, so connected input remains connected.