ProCGroups.ReidemeisterSchreier

7 sections | 59 files | 948 declarations

Discrete and profinite forms of the Reidemeister--Schreier theorem, together with free-group word rewriting, presentation equivalence certificates, verified Tietze scripts, Schreier cocycles, and open-subgroup rank formulas.

This is the public aggregate. For a smaller dependency surface, import ProCGroups.ReidemeisterSchreier.Discrete, ProCGroups.ReidemeisterSchreier.Profinite, or a focused submodule.

imports

Imported by

ProCGroups

Discrete

This module formalizes the classical discrete Reidemeister--Schreier theorem.

FreeGroup

This module formalizes free-group tools used in Reidemeister--Schreier rewriting.

Groupoid

This module rebuilds the spanning-tree loop construction using public conversion functions between mathlib's vertex type synonyms. No private-root declaration or backward elabor...

Profinite

This aggregate exports open-subgroup right-coset cocycles, exact generation, and the proved finite-rank basis theorems for free pro-\(C\) groups.

Quiver

1 file | 2 declarations | 2 Definitions

This module formalizes the quiver and arborescence tools used by the groupoid construction.

RightQuotient

1 file | 6 declarations | 3 Theorems | 2 Definitions | 1 Abbreviation

This module exposes the right-coset quotient of a group by a subgroup and its natural action `g • [a] = [a * g⁻¹]`. The quotient is intentionally only a coset space: for a non-n...

Schreier

1 file | 7 declarations | 6 Theorems | 1 Definition

This module formalizes Schreier generators and rewriting.