Bouquet graphs for basis subsets

This file gives the basic rose graph for a chosen subset of the two free basis letters and proves that its loop subgroup is exactly the subgroup generated by those letters.

def Stallings.basisRose (S : Finset (Fin 2)) : InverseAutomaton (Fin 1)

The one-vertex rose with one loop for each generator in S.

Equations

• Stallings.basisRose S = { base := 0, next := fun (x : Fin 1) (x_1 : Stallings.Letter) => if x_1.1 ∈ S then some 0 else none, inverse_next := ⋯ }

def Stallings.basisSubgroup (S : Finset (Fin 2)) : Subgroup Free

The subgroup generated by the basis letters selected by S.

Equations

• Stallings.basisSubgroup S = Subgroup.closure (FreeGroup.of '' ↑S)

theorem Stallings.basisRose_loopSubgroup (S : Finset (Fin 2)) : (basisRose S).loopSubgroup = basisSubgroup S

The subgroup read from the subset rose is generated by precisely its loop labels.