Morphisms into folded labelled graphs

A based label-preserving morphism from a graph reachable from its base vertex into a folded graph is unique. Starting at the base point, the target dart is determined by its source and label; following a path then determines the target of each source vertex. This is the uniqueness part of the Stallings subgroup-graph correspondence. Morphisms out of folded graphs also preserve reduced paths; this lets them restrict to based cores.

References

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

theorem TauCeti.StallingsGraph.Hom.eq_of_isFolded_of_reachable {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (hT : T.IsFolded) (hS : ∀ (a : S.graph.V), Nonempty (S.graph.Path S.base a)) (f g : S.Hom T) : f = g

Two based label-preserving morphisms to a folded graph agree if every source vertex is reachable from the base vertex.

theorem TauCeti.StallingsGraph.Hom.isReduced_mapPath {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (hS : S.IsFolded) {a b : S.graph.V} (p : S.graph.Path a b) (hp : SerreGraph.Path.IsReduced S.graph p) : SerreGraph.Path.IsReduced T.graph (f.graphHom.toPrefunctor.mapPath p)

A label-preserving morphism out of a folded graph preserves reduced paths, even when it identifies vertices or darts globally.

theorem TauCeti.StallingsGraph.Hom.injective_mapE_of_injective_mapV {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (hS : S.IsFolded) (hf : Function.Injective f.graphHom.mapV) : Function.Injective f.graphHom.mapE

A label-preserving morphism from a folded graph that is injective on vertices is also injective on darts.