ReidemeisterSchreier.Discrete.Presentations.Tietze.Script

25 Definition

This module studies script for reidemeister schreier. This Tietze script step replaces a family of relators by equivalent relators. This Tietze script step replaces one relator by an equivalent relator.

Open this file on GitHub

import

ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion

Imported by

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.replaceRelators GitHub

def replaceRelators
    {R S : Set (FreeGroup X)}
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=
  (Presented.replaceRelatorsTietzeEquiv hR_to_S hS_to_R).toScript

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

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.replaceRelator GitHub

def replaceRelator
    {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
    (holdRelator :
      RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
    (hnewRelator : RelatorEquivalent R newRelator 1) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (insert newRelator (R \ {oldRelator}))) :=
  (Presented.replaceRelatorTietzeEquiv holdRelator hnewRelator).toScript

This Tietze script step replaces one relator by an equivalent relator.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.addRedundantRelator GitHub

def addRedundantRelator
    {R : Set (FreeGroup X)} {r : FreeGroup X}
    (hr : r ∈ Subgroup.normalClosure R) :
    TietzeScript (Presentation.ofRelators (insert r R))
      (Presentation.ofRelators R) :=
  (Presented.addRedundantRelatorTietzeEquiv hr).toScript

This Tietze script step adds one redundant relator.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.addRedundantRelatorInverse GitHub

def addRedundantRelatorInverse
    {R : Set (FreeGroup X)} {r : FreeGroup X}
    (hr : r ∈ Subgroup.normalClosure R) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (insert r R)) :=
  (Presented.addRedundantRelatorTietzeEquiv hr).symm.toScript

This inverse Tietze script step removes a previously added redundant relator.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.removeRedundantRelator GitHub

def removeRedundantRelator
    {R : Set (FreeGroup X)} {r : FreeGroup X}
    (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (R \ {r})) :=
  (Presented.removeRedundantRelatorTietzeEquiv hr).toScript

This Tietze script step removes one redundant relator.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.addRedundantRelators GitHub

def addRedundantRelators
    {R S : Set (FreeGroup X)}
    (hS : S ⊆ Subgroup.normalClosure R) :
    TietzeScript (Presentation.ofRelators (R ∪ S))
      (Presentation.ofRelators R) :=
  (Presented.addRedundantRelatorsTietzeEquiv hS).toScript

This Tietze script step adds a family of redundant relators.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.addRedundantRelatorsRelatorEquivalent GitHub

def addRedundantRelatorsRelatorEquivalent
    {R S : Set (FreeGroup X)}
    (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
    TietzeScript (Presentation.ofRelators (R ∪ S))
      (Presentation.ofRelators R) :=
  (Presented.addRedundantRelatorsRelatorEquivalentTietzeEquiv hS).toScript

The scripted addition of redundant relators preserves relator equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.addRedundantRelatorsInverse GitHub

def addRedundantRelatorsInverse
    {R S : Set (FreeGroup X)}
    (hS : S ⊆ Subgroup.normalClosure R) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (R ∪ S)) :=
  (Presented.addRedundantRelatorsTietzeEquiv hS).symm.toScript

This inverse Tietze script step removes a previously added family of redundant relators.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.addRedundantRelatorsRelatorEquivalentInverse GitHub

def addRedundantRelatorsRelatorEquivalentInverse
    {R S : Set (FreeGroup X)}
    (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (R ∪ S)) :=
  (Presented.addRedundantRelatorsRelatorEquivalentTietzeEquiv hS).symm.toScript

The scripted inverse direction after adding redundant relators preserves relator equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.removeRelatorSubset GitHub

def removeRelatorSubset
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (R \ D)) :=
  (Presented.removeRelatorSubsetTietzeEquiv hD).toScript

This Tietze script step removes a subset of redundant relators.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.removeRelatorSubsetRelatorEquivalent GitHub

def removeRelatorSubsetRelatorEquivalent
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (R \ D)) :=
  (Presented.removeRelatorSubsetRelatorEquivalentTietzeEquiv hD).toScript

The scripted removal of a redundant relator subset preserves relator equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.removeRelatorSubsetInverse GitHub

def removeRelatorSubsetInverse
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
    TietzeScript (Presentation.ofRelators (R \ D))
      (Presentation.ofRelators R) :=
  (Presented.removeRelatorSubsetTietzeEquiv hD).symm.toScript

This inverse Tietze script step adds back a removed relator subset.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.removeRelatorSubsetRelatorEquivalentInverse GitHub

def removeRelatorSubsetRelatorEquivalentInverse
    {R D : Set (FreeGroup X)}
    (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
    TietzeScript (Presentation.ofRelators (R \ D))
      (Presentation.ofRelators R) :=
  (Presented.removeRelatorSubsetRelatorEquivalentTietzeEquiv hD).symm.toScript

The scripted inverse direction after removing a relator subset preserves relator equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.replaceRelatorSubset GitHub

def replaceRelatorSubset
    {R D E : Set (FreeGroup X)}
    (hD :
      ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
    (hE : E ⊆ Subgroup.normalClosure R) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators ((R \ D) ∪ E)) :=
  (Presented.replaceRelatorSubsetTietzeEquiv hD hE).toScript

Replace a whole subfamily \(D\) of relators by a new family \(E\). Relators outside \(D\) are kept unchanged.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.replaceRelatorSubsetRelatorEquivalent GitHub

def replaceRelatorSubsetRelatorEquivalent
    {R D E : Set (FreeGroup X)}
    (hD :
      ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
    (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators ((R \ D) ∪ E)) :=
  (Presented.replaceRelatorSubsetRelatorEquivalentTietzeEquiv hD hE).toScript

The scripted replacement of a relator subset preserves relator equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.renameGenerators GitHub

def renameGenerators
    (R : Set (FreeGroup X)) (e : X ≃ Y) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R)) :=
  (Presented.renameGeneratorsTietzeEquiv R e).toScript

This Tietze script step renames the generators of the presentation.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.ofGeneratorMaps GitHub

def ofGeneratorMaps
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ r ∈ R,
        FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
    (hS :
      ∀ s ∈ S,
        FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent R
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent S
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=
  (TietzeEquiv.ofGeneratorMaps
    toGenerator invGenerator hR hS hinv_to hto_inv).toScript

Compatible generator maps define a Tietze script between the two presentations.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.ofGeneratorMapsRelatorEquivalent GitHub

def ofGeneratorMapsRelatorEquivalent
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    (toGenerator : X → FreeGroup Y)
    (invGenerator : Y → FreeGroup X)
    (hR :
      ∀ r ∈ R,
        RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
    (hS :
      ∀ s ∈ S,
        RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
    (hinv_to :
      ∀ x : X,
        RelatorEquivalent R
          (FreeGroup.lift invGenerator (toGenerator x))
          (FreeGroup.of x))
    (hto_inv :
      ∀ y : Y,
        RelatorEquivalent S
          (FreeGroup.lift toGenerator (invGenerator y))
          (FreeGroup.of y)) :
    TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=
  (TietzeEquiv.ofGeneratorMapsRelatorEquivalent
    toGenerator invGenerator hR hS hinv_to hto_inv).toScript

A Tietze script step from generator maps preserves relators up to relator equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.adjoinGenerators GitHub

def adjoinGenerators
    (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
    TietzeScript (Presentation.ofRelators R)
      (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word)) :=
  (Presented.adjoinGeneratorsTietzeEquiv R word).toScript

Tietze move: adding a family of generators \(y : Y\) with relations \(y = \mathrm{word}(y)\).

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.substituteDefinedGenerators GitHub

def substituteDefinedGenerators
    (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
    TietzeScript
      (Presentation.ofRelators (Presented.relatorsWithDefinedGenerators R word))
      (Presentation.ofRelators
        (Presented.relatorsAfterSubstitutingDefinedGenerators R word)) :=
  (Presented.substituteDefinedGeneratorsTietzeEquiv R word).toScript

Tietze move eliminating generators \(y : Y\) using relations \(y = \mathrm{word}(y)\), while substituting \(\mathrm{word}(y)\) into all remaining relators.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.deleteTrivialGenerators GitHub

def deleteTrivialGenerators
    (R : Set (FreeGroup (Sum X Y))) :
    TietzeScript
      (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
      (Presentation.ofRelators
        (Presented.relatorsAfterDeletingTrivialGenerators R)) :=
  (Presented.deleteTrivialGeneratorsTietzeEquiv R).toScript

Tietze move deleting a family of generators that have relators y = 1. Every remaining relator is pushed forward by substituting those deleted generators with 1.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.substituteDefinedGeneratorsAlongEquiv GitHub

def substituteDefinedGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    TietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
      (Presentation.ofRelators
        (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv
          R e word)) :=
  (Presented.substituteDefinedGeneratorsAlongEquivTietzeEquiv R e word).toScript

Scriptable Tietze step substituting defined generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.deleteTrivialGeneratorsAlongEquiv GitHub

def deleteTrivialGeneratorsAlongEquiv
    (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    TietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
      (Presentation.ofRelators
        (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e)) :=
  (Presented.deleteTrivialGeneratorsAlongEquivTietzeEquiv R e).toScript

Scriptable Tietze step deleting trivial generators after splitting the generator type by an equivalence \(Z \simeq X \oplus Y\).

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.substituteDefinedGeneratorsOfPredicate GitHub

def substituteDefinedGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
    (word :
      Presented.GeneratorPartition.Deleted delete →
        FreeGroup (Presented.GeneratorPartition.Kept delete)) :
    TietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithDefinedGeneratorsOfPredicate R delete word))
      (Presentation.ofRelators
        (Presented.relatorsAfterSubstitutingDefinedGeneratorsOfPredicate
          R delete word)) :=
  (Presented.substituteDefinedGeneratorsOfPredicateTietzeEquiv R delete word).toScript

This Tietze script step substitutes generators defined by words satisfying the given predicate.

Definition ReidemeisterSchreier.Discrete.Presentations.TietzeScript.deleteTrivialGeneratorsOfPredicate GitHub

def deleteTrivialGeneratorsOfPredicate
    (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
    TietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithTrivialGeneratorsOfPredicate R delete))
      (Presentation.ofRelators
        (Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate
          R delete)) :=
  (Presented.deleteTrivialGeneratorsOfPredicateTietzeEquiv R delete).toScript

This Tietze script step deletes generators proved trivial by the given predicate.

ReidemeisterSchreier.Discrete.Presentations.Tietze.Script

Declarations