ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups

6 sections | 8 files | 78 declarations

This aggregate exposes the discrete open-subgroup development: reduced-word utilities, right Schreier transversals and generators, prefix trees, and the resulting free bases.

imports

Imported by

ProCGroups.ReidemeisterSchreier.Discrete

ClassicalGeneratorBasis

1 file | 3 declarations | 2 Theorems | 1 Definition

This module identifies the classical Schreier generators with the free basis obtained from complement edges, including the inverse-basis convention needed for the standard gener...

FreeBasis

1 file | 13 declarations | 7 Theorems | 5 Definitions | 1 Abbreviation

Using the action groupoid and Schreier prefix tree, this module constructs a free basis indexed by complement edges and transports it to the canonical type of nontrivial Schreie...

Generators

1 file | 24 declarations | 18 Theorems | 5 Definitions | 1 Abbreviation

From a right Schreier transversal, this module constructs canonical representatives and Schreier generators, identifies the nontrivial representative-generator pairs, and proves...

PrefixTree

This module constructs the Schreier prefix tree from a right transversal, proves its positive and negative edge criteria, and relates its complement edges to the nontrivial Schr...

Transversals

1 file | 16 declarations | 13 Theorems | 2 Definitions | 1 Instance

This module defines full and partial right Schreier transversals in free groups, proves their complement and prefix-closure properties, and supplies the existence and extension ...

Words

3 files | 3 declarations | 1 Lemma | 2 Definitions

This aggregate exposes prefix operations on reduced free-group words and the compatibility layer connecting them to the Nielsen--Schreier action-groupoid construction.