ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators

5 sections | 5 files | 106 declarations

This aggregate module exposes the relator predicates, congruence constructions, free-group lifting lemmas, word operations, and presentation-level results used by the discrete Reidemeister--Schreier development.

imports

Imported by

ProCGroups.ReidemeisterSchreier.Discrete.Presentations

Basic

1 file | 40 declarations | 38 Theorems | 2 Definitions

This module defines equality modulo a relator normal closure and proves its elementary equivalence, congruence, inversion, multiplication, and quotient characterizations.

Congruence

1 file | 17 declarations | 17 Theorems

This module transports normal-closure membership and relator equivalence through inclusions, homomorphisms, and indexed unions of relator families.

FreeGroupLift

1 file | 15 declarations | 14 Theorems | 1 Definition

This module relates reduced words and FreeGroup.mk, then proves that lifts whose generator images agree modulo a relator normal closure agree on every free-group word.

Operations

1 file | 29 declarations | 28 Theorems | 1 Definition

This module proves invariance and closure lemmas for changing relator sets, conjugating and cyclically rotating words, products of lists, and ordered finite products.

Presentation

1 file | 5 declarations | 5 Theorems

This module expands conjugated list products and promotes generatorwise normal-closure relations to all words under a free-group endomorphism.