The flower of a finite list of words

A word contributes a polygonal petal whose successive darts carry its letters. All petals meet at one base vertex. This is the finite graph from which folding constructs the Stallings graph of the subgroup generated by the words.

References

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

def TauCeti.StallingsGraph.FlowerVertex {α : Type u_1} (ws : List (List (α × Bool))) : Type

Vertices of the flower: none is the base vertex and some ⟨i, j⟩ is the (j+1)st interior vertex of petal i.

def TauCeti.StallingsGraph.FlowerDart {α : Type u_1} (ws : List (List (α × Bool))) : Type

The signed darts of the petals. The Boolean selects the forward or reverse direction.

def TauCeti.StallingsGraph.flowerPos {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (k : ℕ) : FlowerVertex ws

The vertex at position k on petal i; positions outside the interior map to the base.

def TauCeti.StallingsGraph.flower {α : Type u_1} (ws : List (List (α × Bool))) : StallingsGraph α

The based labelled flower with one polygonal petal per word. Empty words contribute no edges, and a one-letter word contributes a loop at the base vertex.

@[simp]

theorem TauCeti.StallingsGraph.flower_base {α : Type u_1} (ws : List (List (α × Bool))) : (flower ws).base = none

@[simp]

theorem TauCeti.StallingsGraph.flower_src_forward {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (j : Fin ws[i].length) : (flower ws).graph.src (⟨i, j⟩, true) = flowerPos ws i ↑j

@[simp]

theorem TauCeti.StallingsGraph.flower_src_reverse {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (j : Fin ws[i].length) : (flower ws).graph.src (⟨i, j⟩, false) = flowerPos ws i (↑j + 1)

@[simp]

theorem TauCeti.StallingsGraph.flower_label_forward {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (j : Fin ws[i].length) : (flower ws).label (⟨i, j⟩, true) = ws[i][↑j]

@[simp]

theorem TauCeti.StallingsGraph.flowerPos_zero {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) : flowerPos ws i 0 = none

@[simp]

theorem TauCeti.StallingsGraph.flowerPos_length {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) : flowerPos ws i ws[↑i].length = none

theorem TauCeti.StallingsGraph.flowerPos_of_pos_of_lt {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (k : ℕ) (h0 : 0 < k) (hk : k < ws[i].length) : flowerPos ws i k = some ⟨i, ⟨k - 1, ⋯⟩⟩

An interior position is the corresponding vertex of its petal.

@[simp]

theorem TauCeti.StallingsGraph.flower_tgt_forward {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (j : Fin ws[i].length) : (flower ws).graph.tgt (⟨i, j⟩, true) = flowerPos ws i (↑j + 1)

@[simp]

theorem TauCeti.StallingsGraph.flower_tgt_reverse {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (j : Fin ws[i].length) : (flower ws).graph.tgt (⟨i, j⟩, false) = flowerPos ws i ↑j

@[simp]

theorem TauCeti.StallingsGraph.flower_label_reverse {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (j : Fin ws[i].length) : (flower ws).label (⟨i, j⟩, false) = (ws[i][↑j].1, !ws[i][↑j].2)

def TauCeti.StallingsGraph.flowerForwardHom {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (k : ℕ) (hk : k < ws[i].length) : flowerPos ws i k ⟶ flowerPos ws i (k + 1)

The forward dart at position k on petal i.

def TauCeti.StallingsGraph.flowerForward {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (k : ℕ) (hk : k < ws[i].length) : (flower ws).graph.Path (flowerPos ws i k) (flowerPos ws i (k + 1))

The one-edge path traversing the kth letter of petal i.

@[simp]

theorem TauCeti.StallingsGraph.flower_word_forward {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (k : ℕ) (hk : k < ws[i].length) : (flower ws).word (flowerForward ws i k hk) = [ws[i][k]]

theorem TauCeti.StallingsGraph.exists_flower_prefix {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) (k : ℕ) (hk : k ≤ ws[i].length) : ∃ (p : (flower ws).graph.Path (flower ws).base (flowerPos ws i k)), (flower ws).word p = List.take k ws[i]

Each prefix of a petal is read by a path from the base to its corresponding vertex.

theorem TauCeti.StallingsGraph.mk_mem_flower_subgroup {α : Type u_1} (ws : List (List (α × Bool))) (i : Fin ws.length) : FreeGroup.mk ws[i] ∈ (flower ws).subgroup (flower ws).base

Every input word is read by a loop around its petal.

theorem TauCeti.StallingsGraph.closure_le_flower_subgroup {α : Type u_1} (ws : List (List (α × Bool))) : Subgroup.closure {g : FreeGroup α | ∃ w ∈ ws, FreeGroup.mk w = g} ≤ (flower ws).subgroup (flower ws).base

The subgroup generated by the input words is accepted by their flower.

theorem TauCeti.StallingsGraph.flower_subgroup {α : Type u_1} (ws : List (List (α × Bool))) : (flower ws).subgroup (flower ws).base = Subgroup.closure {g : FreeGroup α | ∃ w ∈ ws, FreeGroup.mk w = g}

The flower accepts exactly the subgroup generated by its input words.

instance TauCeti.StallingsGraph.flower_finite_vertex {α : Type u_1} (ws : List (List (α × Bool))) : Finite (flower ws).graph.V

The flower has finitely many vertices, regardless of the alphabet.

instance TauCeti.StallingsGraph.flower_finite_dart {α : Type u_1} (ws : List (List (α × Bool))) : Finite (flower ws).graph.E

The flower has finitely many darts, regardless of the alphabet.

theorem TauCeti.StallingsGraph.flower_reachable {α : Type u_1} (ws : List (List (α × Bool))) (v : (flower ws).graph.V) : Nonempty ((flower ws).graph.Path (flower ws).base v)

Every vertex of the flower is reachable by a path from the base vertex.

theorem TauCeti.StallingsGraph.flower_connected {α : Type u_1} (ws : List (List (α × Bool))) : (flower ws).graph.Connected

The flower is connected, even for an empty list of words.

@[simp]

theorem TauCeti.StallingsGraph.flower_nil_subgroup (α : Type u_2) : (flower []).subgroup none = ⊥

The flower of an empty list accepts only the identity.