Based cores preserve accepted subgroups

Restricting a labelled graph to the union of its reduced based loops preserves its accepted subgroup. The resulting graph is connected, is a core at its base vertex, and inherits foldedness and finiteness. The construction retains the stem from the base to a circuit; only vertices away from the base are forbidden to have degree one. A label-preserving morphism out of a folded graph restricts to a morphism of based cores.

References

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

def TauCeti.StallingsGraph.core {α : Type u_1} (S : StallingsGraph α) : StallingsGraph α

The based core, with labels inherited from the ambient graph. Its carrier computes to the Serre core so paths and finite-type instances can be used directly.

@[simp]

theorem TauCeti.StallingsGraph.core_graph {α : Type u_1} (S : StallingsGraph α) : S.core.graph = S.graph.core S.base

@[simp]

theorem TauCeti.StallingsGraph.core_base {α : Type u_1} (S : StallingsGraph α) : S.core.base = S.graph.coreBase S.base

@[simp]

theorem TauCeti.StallingsGraph.core_label {α : Type u_1} (S : StallingsGraph α) (e : S.core.graph.E) : S.core.label e = S.label ↑e

instance TauCeti.StallingsGraph.instFiniteVGraphCore {α : Type u_1} (S : StallingsGraph α) [Finite S.graph.V] : Finite S.core.graph.V

instance TauCeti.StallingsGraph.instFiniteEGraphCore {α : Type u_1} (S : StallingsGraph α) [Finite S.graph.E] : Finite S.core.graph.E

def TauCeti.StallingsGraph.coreInclusion {α : Type u_1} (S : StallingsGraph α) : S.core.Hom S

Inclusion of the core preserves the base vertex and every label. Its vertex map computes so that mapped paths have their original ambient endpoints.

@[simp]

theorem TauCeti.StallingsGraph.coreInclusion_graphHom {α : Type u_1} (S : StallingsGraph α) : S.coreInclusion.graphHom = S.graph.coreInclusion S.base

theorem TauCeti.StallingsGraph.core_isCore {α : Type u_1} (S : StallingsGraph α) : S.core.graph.IsCore S.core.base

The core is a core at its distinguished vertex; in particular all its vertices are reachable from that vertex.

theorem TauCeti.StallingsGraph.IsFolded.core {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) : S.core.IsFolded

Taking the based core preserves foldedness.

@[simp]

theorem TauCeti.StallingsGraph.core_subgroup {α : Type u_1} (S : StallingsGraph α) : S.core.subgroup (S.graph.coreBase S.base) = S.subgroup S.base

The based core accepts exactly the same subgroup as the original labelled graph.

theorem TauCeti.StallingsGraph.Hom.map_mem_coreDarts {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (hS : S.IsFolded) {e : S.graph.E} (he : e ∈ S.graph.coreDarts S.base) : f.graphHom.mapE e ∈ T.graph.coreDarts T.base

A morphism out of a folded graph sends core darts to core darts.

theorem TauCeti.StallingsGraph.Hom.map_mem_coreVertices {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (hS : S.IsFolded) {a : S.graph.V} (ha : a ∈ S.graph.coreVertices S.base) : f.graphHom.mapV a ∈ T.graph.coreVertices T.base

A morphism out of a folded graph sends core vertices to core vertices, including the isolated base vertex when the accepted subgroup is trivial.

def TauCeti.StallingsGraph.Hom.core {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (hS : S.IsFolded) : S.core.Hom T.core

Restriction of a labelled morphism to based cores. Foldedness of the source prevents cancellation of the reduced loops that witness core membership.

@[simp]

theorem TauCeti.StallingsGraph.Hom.core_mapV_val {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (hS : S.IsFolded) (a : S.core.graph.V) : ↑((f.core hS).graphHom.mapV a) = f.graphHom.mapV ↑a

@[simp]

theorem TauCeti.StallingsGraph.Hom.core_mapE_val {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (hS : S.IsFolded) (e : S.core.graph.E) : ↑((f.core hS).graphHom.mapE e) = f.graphHom.mapE ↑e