Folded labelled graphs

A labelled graph is folded when the label and initial vertex determine a dart. This makes the word and endpoints determine a path and ensures that a reduced path has a freely reduced label. These are the local facts behind the Stallings subgroup criterion.

References

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

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

Outgoing darts with the same label coincide.

theorem TauCeti.StallingsGraph.isFolded_def {α : Type u_1} (S : StallingsGraph α) : S.IsFolded ↔ ∀ (e f : S.graph.E), S.graph.src e = S.graph.src f → S.label e = S.label f → e = f

Foldedness is uniqueness of an outgoing dart with a given label.

theorem TauCeti.StallingsGraph.IsFolded.eq_of_tgt_label {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {e f : S.graph.E} (ht : S.graph.tgt e = S.graph.tgt f) (hl : S.label e = S.label f) : e = f

In a folded graph, the target and label also determine a dart.

theorem TauCeti.StallingsGraph.rose_isFolded (α : Type u_2) : (rose α).IsFolded

The rose is folded: each signed generator specifies its unique outgoing dart.

theorem TauCeti.StallingsGraph.IsFolded.labels_not_inverse {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {e f : S.graph.E} (hsrc : S.graph.src f = S.graph.tgt e) (hne : f ≠ S.graph.rev e) : S.label f ≠ ((S.label e).1, !(S.label e).2)

Two consecutive darts of a reduced path cannot carry inverse labels in a folded graph.

theorem TauCeti.StallingsGraph.IsFolded.isReduced_word {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {a b : S.graph.V} (p : S.graph.Path a b) (hp : SerreGraph.Path.IsReduced S.graph p) : FreeGroup.IsReduced (S.word p)

A reduced path in a folded graph reads a freely reduced word.

theorem TauCeti.StallingsGraph.IsFolded.path_eq_of_word_eq {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {a b : S.graph.V} (p q : S.graph.Path a b) (h : S.word p = S.word q) : p = q

In a folded graph, endpoints and the label word determine a path.

theorem TauCeti.StallingsGraph.IsFolded.eq_tgt_of_word_eq {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {a b c : S.graph.V} (p : S.graph.Path a b) (q : S.graph.Path a c) (h : S.word p = S.word q) : b = c

Paths with the same initial vertex and label word have the same terminal vertex in a folded graph. The terminal vertices are not assumed equal.

@[simp]

theorem TauCeti.StallingsGraph.IsFolded.toWord_read_eq_word {α : Type u_1} (S : StallingsGraph α) [DecidableEq α] (hS : S.IsFolded) {a b : S.graph.V} (p : S.graph.Path a b) (hp : SerreGraph.Path.IsReduced S.graph p) : (S.read p).toWord = S.word p

The reduced word of a reduced path's reading is its actual label word.

theorem TauCeti.StallingsGraph.IsFolded.path_eq_of_read_eq {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {a b : S.graph.V} (p q : S.graph.Path a b) (hp : SerreGraph.Path.IsReduced S.graph p) (hq : SerreGraph.Path.IsReduced S.graph q) (h : S.read p = S.read q) : p = q

A folded graph's reduced paths with fixed endpoints have distinct free-group readings.

theorem TauCeti.StallingsGraph.IsFolded.eq_tgt_of_read_eq {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {a b c : S.graph.V} (p : S.graph.Path a b) (q : S.graph.Path a c) (h : S.read p = S.read q) : b = c

Paths with the same initial vertex and free-group reading have the same terminal vertex in a folded graph, even when the paths are not reduced.

theorem TauCeti.StallingsGraph.IsFolded.eq_tgt_iff_read_mul_inv_mem {α : Type u_1} (S : StallingsGraph α) (hS : S.IsFolded) {a b c : S.graph.V} (p : S.graph.Path a b) (q : S.graph.Path a c) : b = c ↔ S.read p * (S.read q)⁻¹ ∈ S.subgroup a

The endpoint of a based path in a folded graph is determined by the coset of its reading. No reducedness assumption on the paths is necessary.