ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze

7 sections | 7 files | 176 declarations

This aggregate separates semantic presentation equivalence from syntactic transformations. The core and generator/relator operation modules construct certificates; Tietze.Script records well-typed elementary move sequences and their trace and cost.

imports

Imported by

ProCGroups.ReidemeisterSchreier.Discrete.Presentations

Core

1 file | 25 declarations | 22 Definitions | 3 Structures

This module packages the algebraic content of a Tietze equivalence: mutually inverse maps between groups presented by relators. `Presentation` remembers the generator type, whil...

GeneratorAddition

1 file | 22 declarations | 10 Theorems | 12 Definitions

This module formalizes adjoining generators with defining words. It builds the inclusion and elimination homomorphisms, transforms the relators, and packages the resulting prese...

GeneratorDeletion

1 file | 46 declarations | 16 Theorems | 30 Definitions

This module formalizes deletion of generators forced to be trivial. It defines the elimination homomorphism and relator transformations and packages the induced equivalence of p...

GeneratorMap

1 file | 9 declarations | 1 Theorem | 8 Definitions

This module builds relator-quotient equivalences from maps on generators, including indexed relator families, and proves the normal-closure properties of the associated free-gro...

RelatorQuotientMutualMapData

1 file | 9 declarations | 1 Theorem | 7 Definitions | 1 Structure

This module packages mutually inverse maps between relator quotients. It provides reflexive, symmetric, and transitive composition together with a one-sided constructor when the...

RelatorReplacement

1 file | 36 declarations | 2 Theorems | 34 Definitions

This module supplies semantic presented-group equivalences for replacing relators: equal normal closures, mutual relator maps, generator maps, and compositions of these transfor...

Script

1 file | 29 declarations | 10 Theorems | 16 Definitions | 3 Inductive types

`ElementaryTietzeMove` records genuine presentation transformations with indexed source and target presentations. `VerifiedTietzeScript` is the typed sequence of those moves; it...