Source: ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic
1import ProCGroups.ReidemeisterSchreier.FreeGroup.PrefixParent
3/-!
4# Reidemeister Schreier / Discrete / Open Subgroups / Words / Basic
6This module defines the initial reduced-word segments of a free-group element
7and proves the membership and prefix-parent facts used by discrete Schreier
8transversals.
9-/
11namespace ReidemeisterSchreier.Discrete.OpenSubgroups
14/--
15This list consists of the initial segments (prefixes) of the reduced word representing a
16free-group element, as used in Reidemeister--Schreier rewriting.
17-/
18def freeGroupInitialSegments {X : Type u} [DecidableEq X] (t : FreeGroup X) :
19 Set (FreeGroup X) := by
20 exact
21 {u | ∃ n ≤ (FreeGroup.toWord t).length, u = FreeGroup.mk (List.take n (FreeGroup.toWord t))}
24end ReidemeisterSchreier.Discrete.OpenSubgroups