Folding a closed set of vertices

Restricting to an edge-closed set containing the basepoint preserves all based loops. The restricted folding theorem only needs a potential on that set, so unrelated connected components impose no hypotheses. This extension was added during the AI-assisted Lean Pool port of Arthur Freitas Ramos' development.

def Stallings.InverseMultigraph.restrict {V : Type u_1} [DecidableEq V] (G : InverseMultigraph V) (vertices : Finset V) : InverseMultigraph ↥vertices

The induced inverse multigraph on a finite set of vertices.

Equations

• G.restrict vertices = { edges := fun (v : ↥vertices) (x : Stallings.Letter) => {w : ↥vertices | ↑w ∈ G.edges (↑v) x}, inverse_edges := ⋯ }

def Stallings.InverseMultigraph.IsClosed {V : Type u_1} (G : InverseMultigraph V) (vertices : Finset V) : Prop

A vertex set is closed when every edge starting in it also ends in it.

Equations

• G.IsClosed vertices = ∀ ⦃v : V⦄ ⦃x : Stallings.Letter⦄ ⦃w : V⦄, v ∈ vertices → w ∈ G.edges v x → w ∈ vertices

theorem Stallings.InverseMultigraph.Walk.of_restrict {V : Type u_1} [DecidableEq V] (G : InverseMultigraph V) {vertices : Finset V} {v z : ↥vertices} {w : Word} (h : (G.restrict vertices).Walk v w z) : G.Walk (↑v) w ↑z

A path in the induced graph is also a path in the original graph.

theorem Stallings.InverseMultigraph.Walk.restrict {V : Type u_1} [DecidableEq V] (G : InverseMultigraph V) {vertices : Finset V} (hclosed : G.IsClosed vertices) {v z : V} {w : Word} (h : G.Walk v w z) (hv : v ∈ vertices) : ∃ (hz : z ∈ vertices), (G.restrict vertices).Walk ⟨v, hv⟩ w ⟨z, hz⟩

Paths starting in a closed vertex set can be lifted to its induced graph.

theorem Stallings.InverseMultigraph.restrict_loopSubgroup_eq {V : Type u_1} [DecidableEq V] (G : InverseMultigraph V) (vertices : Finset V) (hclosed : G.IsClosed vertices) (base : ↥vertices) : (G.restrict vertices).loopSubgroup base = G.loopSubgroup ↑base

Restricting to a closed set containing the basepoint preserves its loop subgroup.

theorem Stallings.InverseMultigraph.fold_restrict_loopSubgroup_eq {V : Type u_1} [DecidableEq V] (G : InverseMultigraph V) [LinearOrder V] (vertices : Finset V) (hclosed : G.IsClosed vertices) (base : ↥vertices) (potential : ↥vertices → Free) (hpotential : HasCosetPotential (G.restrict vertices) (G.loopSubgroup ↑base) potential) (hbase : potential base = 1) : (foldAutomaton (G.restrict vertices) base).loopSubgroup = G.loopSubgroup ↑base

Folding an edge-closed set containing the basepoint preserves the original based-loop subgroup. The potential is required only on the selected vertices.