The subgroup accepted by a Stallings fold

Identifying equally labelled outgoing darts does not change the subgroup read by loops. The key point is that the two vertices identified by a fold are connected by a path whose label is the identity. Such paths repair the joins when a path in the quotient is lifted dart by dart. This is the local step needed for finite folding.

References

• I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, Section 3, Lemma 3.4.

theorem TauCeti.StallingsGraph.exists_path_read_eq_one_of_foldHom_mapV_eq {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {x y : S.graph.V} (hxy : (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV x = (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV y) : ∃ (p : S.graph.Path x y), S.read p = 1

Vertices identified by a fold can be joined by a path with trivial reading.

theorem TauCeti.StallingsGraph.exists_fold_path_lift {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) {a b : (S.foldAt f₁ f₂ hsrc hlabel).graph.V} (q : (S.foldAt f₁ f₂ hsrc hlabel).graph.Path a b) (x : S.graph.V) (hx : (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV x = a) : ∃ (y : S.graph.V) (p : S.graph.Path x y), (S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV y = b ∧ S.read p = (S.foldAt f₁ f₂ hsrc hlabel).read q

A path in a single fold can be lifted from any chosen preimage of its start, without changing its free-group reading.

@[simp]

theorem TauCeti.StallingsGraph.foldAt_subgroup {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) (x : S.graph.V) : (S.foldAt f₁ f₂ hsrc hlabel).subgroup ((S.foldHom f₁ f₂ hsrc hlabel).graphHom.mapV x) = S.subgroup x

A single Stallings fold preserves the subgroup read at every vertex.

@[simp]

theorem TauCeti.StallingsGraph.foldAt_subgroup_base {α : Type u} (S : StallingsGraph α) (f₁ f₂ : S.graph.E) (hsrc : S.graph.src f₁ = S.graph.src f₂) (hlabel : S.label f₁ = S.label f₂) : (S.foldAt f₁ f₂ hsrc hlabel).subgroup (S.foldAt f₁ f₂ hsrc hlabel).base = S.subgroup S.base

A single Stallings fold preserves the subgroup accepted at its base vertex.