ReidemeisterSchreier.Discrete.Presentations

4 sections | 11 files | 304 declarations

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

Automation

1 files | 0 declarations

KernelQuotient

1 files | 23 declarations | 17 Theorem | 6 Definition

The presented-kernel quotient is identified with the Reidemeister--Schreier relator quotient.

Relators

1 files | 107 declarations | 103 Theorem | 4 Definition

Equality modulo the normal closure generated by R.

Tietze

8 files | 174 declarations | 30 Theorem | 139 Definition | 5 Structure

A reusable Tietze certificate between two presentations. This is the scriptable layer: certificates can be reversed and composed while retaining the underlying normal-closure data.