Subgroups read by labelled graphs

A labelled Serre graph assigns inverse letters to reversed darts. Reading the labels of closed paths at a vertex gives a subgroup of the free group. Based label-preserving morphisms send the accepted subgroup into that of the target. Moving the base vertex along a path conjugates the accepted subgroup. Every accepted word also has a reduced-path witness. A graph with finitely many darts accepts a finitely generated subgroup at every vertex.

References

• I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, Sections 2–3.

structure TauCeti.StallingsGraph (α : Type u) : Type (max (max u (v + 1)) (w + 1))

A based Serre graph with signed-letter dart labels, inverted by reversal.

• graph : SerreGraph

  The underlying graph.

• base : self.graph.V

  The distinguished vertex.

• label : self.graph.E → α × Bool

  The letter read along each dart.

• label_rev (e : self.graph.E) : self.label (self.graph.rev e) = ((self.label e).1, !(self.label e).2)

  Reversing a dart inverts its label.

def TauCeti.StallingsGraph.word {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} : S.graph.Path a b → List (α × Bool)

The label word of a path, in traversal order.

@[simp]

theorem TauCeti.StallingsGraph.word_nil {α : Type u_1} (S : StallingsGraph α) (a : S.graph.V) : S.word Quiver.Path.nil = []

@[simp]

theorem TauCeti.StallingsGraph.word_cons {α : Type u_1} (S : StallingsGraph α) {a b c : S.graph.V} (p : S.graph.Path a b) (e : b ⟶ c) : S.word (Quiver.Path.cons p e) = S.word p ++ [S.label ↑e]

@[simp]

theorem TauCeti.StallingsGraph.word_toPath {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (e : a ⟶ b) : S.word e.toPath = [S.label ↑e]

@[simp]

theorem TauCeti.StallingsGraph.word_comp {α : Type u_1} (S : StallingsGraph α) {a b c : S.graph.V} (p : S.graph.Path a b) (q : S.graph.Path b c) : S.word (Quiver.Path.comp p q) = S.word p ++ S.word q

def TauCeti.StallingsGraph.read {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (p : S.graph.Path a b) : FreeGroup α

The free-group element represented by the word of a path.

theorem TauCeti.StallingsGraph.read_eq_weight {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (p : S.graph.Path a b) : S.read p = Quiver.Path.weight (fun {i j : S.graph.V} (e : i ⟶ j) => FreeGroup.mk [S.label ↑e]) p

Reading a path is its weight under the signed-letter labelling.

@[simp]

theorem TauCeti.StallingsGraph.read_cons {α : Type u_1} (S : StallingsGraph α) {a b c : S.graph.V} (p : S.graph.Path a b) (e : b ⟶ c) : S.read (Quiver.Path.cons p e) = S.read p * FreeGroup.mk [S.label ↑e]

theorem TauCeti.StallingsGraph.read_eq_mk_word {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (p : S.graph.Path a b) : S.read p = FreeGroup.mk (S.word p)

@[simp]

theorem TauCeti.StallingsGraph.read_toPath {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (e : a ⟶ b) : S.read e.toPath = FreeGroup.mk [S.label ↑e]

@[simp]

theorem TauCeti.StallingsGraph.read_nil {α : Type u_1} (S : StallingsGraph α) (a : S.graph.V) : S.read Quiver.Path.nil = 1

@[simp]

theorem TauCeti.StallingsGraph.read_comp {α : Type u_1} (S : StallingsGraph α) {a b c : S.graph.V} (p : S.graph.Path a b) (q : S.graph.Path b c) : S.read (Quiver.Path.comp p q) = S.read p * S.read q

@[simp]

theorem TauCeti.StallingsGraph.word_reverse {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (p : S.graph.Path a b) : S.word (Quiver.Path.reverse p) = FreeGroup.invRev (S.word p)

@[simp]

theorem TauCeti.StallingsGraph.read_reverse {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (p : S.graph.Path a b) : S.read (Quiver.Path.reverse p) = (S.read p)⁻¹

def TauCeti.StallingsGraph.subgroup {α : Type u_1} (S : StallingsGraph α) (a : S.graph.V) : Subgroup (FreeGroup α)

The subgroup of the free group read by closed paths at a vertex.

@[simp]

theorem TauCeti.StallingsGraph.mem_subgroup_iff {α : Type u_1} (S : StallingsGraph α) {a : S.graph.V} {g : FreeGroup α} : g ∈ S.subgroup a ↔ ∃ (p : S.graph.Path a a), S.read p = g

theorem TauCeti.StallingsGraph.read_mem_subgroup {α : Type u_1} (S : StallingsGraph α) {a : S.graph.V} (p : S.graph.Path a a) : S.read p ∈ S.subgroup a

theorem TauCeti.StallingsGraph.exists_reduced_path_read_eq {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (p : S.graph.Path a b) : ∃ (q : S.graph.Path a b), SerreGraph.Path.IsReduced S.graph q ∧ S.read q = S.read p

Every path has a reduced path with the same endpoints and free-group reading.

theorem TauCeti.StallingsGraph.mem_subgroup_iff_exists_reduced_path {α : Type u_1} (S : StallingsGraph α) {a : S.graph.V} {g : FreeGroup α} : g ∈ S.subgroup a ↔ ∃ (p : S.graph.Path a a), SerreGraph.Path.IsReduced S.graph p ∧ S.read p = g

Membership in the accepted subgroup can be witnessed by a reduced closed path.

theorem TauCeti.StallingsGraph.subgroup_conj {α : Type u_1} (S : StallingsGraph α) {a b : S.graph.V} (p : S.graph.Path a b) : S.subgroup b = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (S.read p)⁻¹)) (S.subgroup a)

Moving the base vertex along a path conjugates the accepted subgroup by its label.

theorem TauCeti.StallingsGraph.subgroup_fg {α : Type u_1} (S : StallingsGraph α) [Finite S.graph.E] (a : S.graph.V) : (S.subgroup a).FG

A labelled graph with finitely many darts accepts a finitely generated subgroup at each vertex.

structure TauCeti.StallingsGraph.Hom {α : Type u_1} (S : StallingsGraph α) (T : StallingsGraph α) : Type (max (max (max u_2 u_3) u_4) u_5)

A based Serre-graph morphism preserving dart labels.

• graphHom : S.graph.Hom T.graph

  The map of underlying Serre graphs.

• map_base : self.graphHom.mapV S.base = T.base

  The distinguished vertex is preserved.

• map_label (e : S.graph.E) : T.label (self.graphHom.mapE e) = S.label e

  Labels are preserved.

theorem TauCeti.StallingsGraph.Hom.ext {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} {f g : S.Hom T} (h : f.graphHom = g.graphHom) : f = g

theorem TauCeti.StallingsGraph.Hom.ext_iff {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} {f g : S.Hom T} : f = g ↔ f.graphHom = g.graphHom

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

Identity morphism of a based labelled graph.

def TauCeti.StallingsGraph.Hom.comp {α : Type u_1} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (g : S.Hom T) (f : R.Hom S) : R.Hom T

Composition of based labelled-graph morphisms.

@[simp]

theorem TauCeti.StallingsGraph.Hom.id_graphHom {α : Type u_1} (S : StallingsGraph α) : (id S).graphHom = SerreGraph.Hom.id S.graph

@[simp]

theorem TauCeti.StallingsGraph.Hom.comp_graphHom {α : Type u_1} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} (g : S.Hom T) (f : R.Hom S) : (g.comp f).graphHom = g.graphHom.comp f.graphHom

@[simp]

theorem TauCeti.StallingsGraph.Hom.id_comp {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) : (id T).comp f = f

@[simp]

theorem TauCeti.StallingsGraph.Hom.comp_id {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) : f.comp (id S) = f

theorem TauCeti.StallingsGraph.Hom.comp_assoc {α : Type u_1} {R : StallingsGraph α} {S : StallingsGraph α} {T : StallingsGraph α} {U : StallingsGraph α} (f : R.Hom S) (g : S.Hom T) (h : T.Hom U) : h.comp (g.comp f) = (h.comp g).comp f

@[simp]

theorem TauCeti.StallingsGraph.Hom.word_mapPath {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) {a b : S.graph.V} (p : S.graph.Path a b) : T.word (f.graphHom.toPrefunctor.mapPath p) = S.word p

@[simp]

theorem TauCeti.StallingsGraph.Hom.read_mapPath {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) {a b : S.graph.V} (p : S.graph.Path a b) : T.read (f.graphHom.toPrefunctor.mapPath p) = S.read p

theorem TauCeti.StallingsGraph.Hom.subgroup_le_subgroup_mapV {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) (a : S.graph.V) : S.subgroup a ≤ T.subgroup (f.graphHom.mapV a)

A labelled morphism sends loops at any vertex to loops with the same reading.

theorem TauCeti.StallingsGraph.Hom.subgroup_le {α : Type u_1} {S : StallingsGraph α} {T : StallingsGraph α} (f : S.Hom T) : S.subgroup S.base ≤ T.subgroup T.base

A based label-preserving morphism sends every accepted word to an accepted word.

def TauCeti.StallingsGraph.rose (α : Type u_2) : StallingsGraph α

The rose with one petal for each generator, labelled by those generators.

@[simp]

theorem TauCeti.StallingsGraph.rose_graph (α : Type u_2) : (rose α).graph = SerreGraph.rose α

@[simp]

theorem TauCeti.StallingsGraph.rose_base (α : Type u_2) : (rose α).base = PUnit.unit

@[simp]

theorem TauCeti.StallingsGraph.rose_label (α : Type u_2) (e : (rose α).graph.E) : (rose α).label e = e

def TauCeti.StallingsGraph.toRose {α : Type u_1} (S : StallingsGraph α) : S.Hom (rose α)

The labels give the canonical morphism from any labelled graph to the rose.

@[simp]

theorem TauCeti.StallingsGraph.toRose_mapV {α : Type u_1} (S : StallingsGraph α) (a : S.graph.V) : S.toRose.graphHom.mapV a = PUnit.unit

@[simp]

theorem TauCeti.StallingsGraph.toRose_mapE {α : Type u_1} (S : StallingsGraph α) (e : S.graph.E) : S.toRose.graphHom.mapE e = S.label e

theorem TauCeti.StallingsGraph.Hom.eq_toRose {α : Type u_1} (S : StallingsGraph α) (f : S.Hom (rose α)) : f = S.toRose

The rose admits exactly one labelled morphism from each labelled graph.

theorem TauCeti.StallingsGraph.rose_subgroup_top (α : Type u_2) : (rose α).subgroup PUnit.unit = ⊤

Every free-group element is read by a loop in the rose.