ReidemeisterSchreier.Discrete.OpenSubgroups

6 sections | 8 files | 81 declarations

This module develops Reidemeister--Schreier rewriting, Schreier generators, finite quotient transversals, and presentation transformations.

ClassicalGeneratorBasis

1 files | 4 declarations | 3 Theorem | 1 Definition

A strengthened Schreier-basis existence statement exposing the value of the chosen basis map on free generators. This inverse-valued statement records the internal basis orienta...

FreeBasis

1 files | 15 declarations | 8 Theorem | 6 Definition | 1 Abbreviation

The total generator arrows in the action groupoid attached to a chosen free basis are indexed by a pair consisting of a vertex and a basis element.

Generators

1 files | 24 declarations | 18 Theorem | 5 Definition | 1 Abbreviation

The Schreier transversal itself carries the same right-coset action, transported along the equivalence with right cosets.

PrefixTree

The parent vertex of a nontrivial prefix-parent edge of a Schreier transversal again lies in the transversal.

Transversals

1 files | 16 declarations | 13 Theorem | 2 Definition | 1 Instance

A right Schreier transversal is a right transversal containing every initial segment of each of its elements.

Words

3 files | 3 declarations | 1 Lemma | 2 Definition

Wrapper for the `ReidemeisterSchreier.Discrete.OpenSubgroups.Words` folder.