ReidemeisterSchreier.Discrete.Presentations.Tietze

7 sections | 7 files | 174 declarations

This module re-exports the generic presentation certificates: RelatorQuotientMutualMapData, TietzeEquiv, Presentation, and TietzeScript, together with relator replacement and generator addition/deletion constructors.

Core

1 files | 25 declarations | 22 Definition | 3 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.

GeneratorAddition

1 files | 22 declarations | 10 Theorem | 12 Definition

Include the old free group into the free group with a family of new generators.

GeneratorDeletion

1 files | 46 declarations | 16 Theorem | 30 Definition

The substitution map sends the generators in \(Y\) to \(1\), while keeping the old generators \(X\). It is used by the Tietze move deleting generators with relators \(y = 1\).

GeneratorMap

1 files | 9 declarations | 1 Theorem | 8 Definition

The relator membership follows from the corresponding relator-equivalence criterion.

RelatorQuotientMutualMapData

1 files | 11 declarations | 1 Theorem | 8 Definition | 2 Structure

Mutual homomorphisms respecting relators induce an isomorphism between the corresponding relator quotients.

RelatorReplacement

1 files | 36 declarations | 2 Theorem | 34 Definition

The Tietze presentation identity follows from the prescribed generator and relator replacement maps.

Script

1 files | 25 declarations | 25 Definition

This Tietze script step replaces a family of relators by equivalent relators.