The flower graph of a finite list of words

The flower graph has one common basepoint and one loop spelling each input word. Its vertices are indexed by generator and letter position, so the construction is finite and the input words remain visible in the definition.

@[reducible, inline]

abbrev Stallings.FlowerVertex (S : List Word) : Type

A finite vertex type for the flower of S. none is the common basepoint; some ⟨i,k⟩ is the vertex after k + 1 letters of the ith generator. Only internal positions are retained; empty and singleton words add no vertices.

Equations

• Stallings.FlowerVertex S = Option ((i : Fin S.length) × Fin (List.length (S.get i) - 1))

def Stallings.flowerVertexOrderCode {S : List Word} : FlowerVertex S → Unit ⊕ₗ Σₗ (i : Fin S.length), Fin (List.length (S.get i) - 1)

Encode flower vertices in a finite lexicographic order.

Equations

• Stallings.flowerVertexOrderCode none = toLex (Sum.inl ())
• Stallings.flowerVertexOrderCode (some p) = toLex (Sum.inr (toLex p))

theorem Stallings.flowerVertexOrderCode_injective {S : List Word} : Function.Injective flowerVertexOrderCode

@[instance_reducible]

instance Stallings.flowerVertexLinearOrder (S : List Word) : LinearOrder (FlowerVertex S)

Equations

• Stallings.flowerVertexLinearOrder S = LinearOrder.lift' Stallings.flowerVertexOrderCode ⋯

def Stallings.flowerPos (S : List Word) (i : Fin S.length) (k : ℕ) (hk : k ≤ List.length (S.get i)) : FlowerVertex S

The vertex at position k while reading generator i, with both endpoints of the generator loop identified with the common basepoint.

Equations

• Stallings.flowerPos S i k hk = if hk0 : k = 0 then none else if hkend : k = List.length (S.get i) then none else some ⟨i, ⟨k - 1, ⋯⟩⟩

def Stallings.flowerSource (S : List Word) (i : Fin S.length) (j : Fin (List.length (S.get i))) : FlowerVertex S

The source vertex of the edge in position j of a generator.

Equations

• Stallings.flowerSource S i j = Stallings.flowerPos S i ↑j ⋯

def Stallings.flowerTarget (S : List Word) (i : Fin S.length) (j : Fin (List.length (S.get i))) : FlowerVertex S

The target vertex of the edge in position j of a generator.

Equations

• Stallings.flowerTarget S i j = Stallings.flowerPos S i (↑j + 1) ⋯

def Stallings.flowerLabel (S : List Word) (i : Fin S.length) (j : Fin (List.length (S.get i))) : Letter

The signed letter at position j of input generator i.

Equations

• Stallings.flowerLabel S i j = List.get (S.get i) j

def Stallings.flowerEdge (S : List Word) (v : FlowerVertex S) (x : Letter) (w : FlowerVertex S) : Prop

A directed edge, allowing either the forward letter in an input word or its inverse orientation.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Stallings.flowerEdgeDecidable (S : List Word) (v : FlowerVertex S) (x : Letter) : DecidablePred (flowerEdge S v x)

Equations

• Stallings.flowerEdgeDecidable S v x w = id inferInstance

theorem Stallings.flowerEdge_inv {S : List Word} {v w : FlowerVertex S} {x : Letter} (h : flowerEdge S v x w) : flowerEdge S w (letterInv x) v

theorem Stallings.flowerEdge_inv_iff {S : List Word} (v w : FlowerVertex S) (x : Letter) : flowerEdge S v x w ↔ flowerEdge S w (letterInv x) v

def Stallings.flowerGraph (S : List Word) : InverseMultigraph (FlowerVertex S)

The initial bouquet of loops spelling the words in S.

Equations

• Stallings.flowerGraph S = { edges := fun (v : Stallings.FlowerVertex S) (x : Stallings.Letter) => Finset.filter (Stallings.flowerEdge S v x) Finset.univ, inverse_edges := ⋯ }

def Stallings.generatorSubgroup (S : List Word) : Subgroup Free

The subgroup generated by the words in the input list.

Equations

• Stallings.generatorSubgroup S = Subgroup.closure (Set.range fun (i : Fin S.length) => Stallings.wordEval (S.get i))

def Stallings.flowerPotential (S : List Word) : FlowerVertex S → Free

The word prefix reaching an internal flower vertex, with 1 at the basepoint.

Equations

• Stallings.flowerPotential S none = 1
• Stallings.flowerPotential S (some ⟨i, k⟩) = Stallings.wordEval (List.take (↑k + 1) (S.get i))

theorem Stallings.flower_hasCosetPotential (S : List Word) : HasCosetPotential (flowerGraph S) (generatorSubgroup S) (flowerPotential S)

The input flower has a coset potential for the subgroup generated by its loop labels.

theorem Stallings.flowerWalk (S : List Word) (i : Fin S.length) : (flowerGraph S).Walk none (S.get i) none

Each input word labels a closed path in the flower graph.

theorem Stallings.flowerGraph_loopSubgroup_eq_generatorSubgroup (S : List Word) : (flowerGraph S).loopSubgroup none = generatorSubgroup S

The loop subgroup of the initial flower is exactly the subgroup generated by the input words.

def Stallings.foldWords (S : List Word) : InverseAutomaton (FlowerVertex S)

The folded automaton constructed from a finite generator list.

Equations

• Stallings.foldWords S = Stallings.foldAutomaton (Stallings.flowerGraph S) none

theorem Stallings.foldWords_loopSubgroup_eq_generatorSubgroup (S : List Word) : (foldWords S).loopSubgroup = generatorSubgroup S

The folded automaton's based-loop subgroup is exactly the subgroup generated by the input words.

def Stallings.foldedMembershipTest (S : List Word) (g : Free) : Bool

Execute the Stallings membership test for the subgroup generated by S.

Equations

• Stallings.foldedMembershipTest S g = (Stallings.foldWords S).membershipTest g

theorem Stallings.foldedMembershipTest_eq_true_iff (S : List Word) (g : Free) : foldedMembershipTest S g = true ↔ g ∈ generatorSubgroup S

The executable folded-graph traversal accepts exactly the elements of the subgroup generated by the supplied words.