Module

CleanedTau.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedTau

31 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Cleaned Tau

This module rewrites tau words on the nondegenerate Schreier-symbol alphabet and proves that the cleaned rewriting respects reduction, multiplication, and the original tau evaluation.

Imports2

Imported by2

def

cleanedTauList

L34 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList

Documentation

List-word form of Schreier rewriting after deleting degenerate finite Schreier generators. This is the computational API for concrete finite examples.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

def cleanedTauList
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (xs : List (X × Bool)) :
    FreeGroup D.NondegenerateSchreierSymbol

theorem

cleanedTauList_nil

L43 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList_nil

Documentation

The cleaned \(\tau\)-list of the empty word is the identity.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem cleanedTauList_nil
    [DecidablePred D.IsDegenerateSchreierSymbol] (q : Q) :
    D.cleanedTauList q [] = 1

theorem

cleanedTauList_cons_true

L54 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList_cons_true

Documentation

The cleaned \(\tau\)-list for a positive letter prefixes the corresponding cleaned Schreier-symbol word.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem cleanedTauList_cons_true
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (x : X) (xs : List (X × Bool)) :
    D.cleanedTauList q ((x, true) :: xs) =
      D.cleanedSchreierSymbolWord (q, x) *
        D.cleanedTauList (D.transition q x) xs

theorem

cleanedTauList_cons_false

L69 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList_cons_false

Documentation

The cleaned \(\tau\)-list for a negative letter prefixes the inverse of the corresponding cleaned Schreier-symbol word.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem cleanedTauList_cons_false
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (x : X) (xs : List (X × Bool)) :
    D.cleanedTauList q ((x, false) :: xs) =
      (D.cleanedSchreierSymbolWord (D.inverseTransition q x, x))⁻¹ *
        D.cleanedTauList (D.inverseTransition q x) xs

theorem

cleanedTauList_append

L83 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList_append

Documentation

The cleaned \(\tau\)-list rewrite of a concatenated word splits as the product of the first rewrite and the rewrite of the second word from the updated quotient element.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem cleanedTauList_append
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (xs ys : List (X × Bool)) :
    D.cleanedTauList q (xs ++ ys) =
      D.cleanedTauList q xs *
        D.cleanedTauList
          (D.quotientMap (D.quotientSection q * FreeGroup.mk xs)) ys

theorem

cleanedTauList_red

L94 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList_red

Documentation

Free-group reduction does not change the cleaned \(\tau\)-list rewrite.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem cleanedTauList_red
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) {xs ys : List (X × Bool)}
    (h : FreeGroup.Red xs ys) :
    D.cleanedTauList q xs = D.cleanedTauList q ys

theorem

cleanedTauList_eq_of_mk_eq

L103 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList_eq_of_mk_eq

Documentation

The cleaned \(\tau\)-lists agree when the corresponding quotient generators agree.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem cleanedTauList_eq_of_mk_eq
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) {xs ys : List (X × Bool)}
    (h : FreeGroup.mk xs = FreeGroup.mk ys) :
    D.cleanedTauList q xs = D.cleanedTauList q ys

def

cleanedTau

L111 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau

Documentation

Schreier rewriting after deleting degenerate finite Schreier generators.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

def cleanedTau
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (w : FreeGroup X) :
    FreeGroup D.NondegenerateSchreierSymbol

theorem

cleanedTau_eq_cleanedTauList_toWord

L121 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_eq_cleanedTauList_toWord

Documentation

Cleaned \(\tau\) of a free-group word is the cleaned \(\tau\)-list rewrite of its word representation.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_eq_cleanedTauList_toWord
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (w : FreeGroup X) :
    D.cleanedTau q w = D.cleanedTauList q w.toWord

theorem

cleanedTau_mk

L131 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_mk

Documentation

The cleaned \(\tau\)-rewrite of \(\mathrm{FreeGroup.mk}(xs)\) agrees with rewriting the list \(xs\).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_mk
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (xs : List (X × Bool)) :
    D.cleanedTau q (FreeGroup.mk xs) = D.cleanedTauList q xs

def

cleanedTauNormalWord

L141 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauNormalWord

Documentation

Reduced list-word normal form of \(\mathrm{cleanedTau}(q,w)\). This is the computation-facing output of the cleaned finite Reidemeister--Schreier rewriting map.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

def cleanedTauNormalWord
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    (q : Q) (w : FreeGroup X) :
    List (D.NondegenerateSchreierSymbol × Bool)

def

cleanedTauListNormalWord

L149 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauListNormalWord

Documentation

Reduced list-word normal form of \(\mathrm{cleanedTauList}(q,xs)\).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

def cleanedTauListNormalWord
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    (q : Q) (xs : List (X × Bool)) :
    List (D.NondegenerateSchreierSymbol × Bool)

theorem

mk_cleanedTauNormalWord

L157 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mk_cleanedTauNormalWord

Documentation

The reduced normal word reconstructs the cleaned \(\tau\)-rewrite.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem mk_cleanedTauNormalWord
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    (q : Q) (w : FreeGroup X) :
    FreeGroup.mk (D.cleanedTauNormalWord q w) = D.cleanedTau q w

theorem

mk_cleanedTauListNormalWord

L167 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mk_cleanedTauListNormalWord

Documentation

The reduced normal word reconstructs the cleaned \(\tau\)-list rewrite.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem mk_cleanedTauListNormalWord
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    (q : Q) (xs : List (X × Bool)) :
    FreeGroup.mk (D.cleanedTauListNormalWord q xs) =
      D.cleanedTauList q xs

theorem

cleanedTauNormalWord_mk

L180 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauNormalWord_mk

Documentation

The normal word of the cleaned \(\tau\)-rewrite of FreeGroup.mk xs is the normal word obtained by cleaning the list xs directly.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTauNormalWord_mk
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    (q : Q) (xs : List (X × Bool)) :
    D.cleanedTauNormalWord q (FreeGroup.mk xs) =
      D.cleanedTauListNormalWord q xs

theorem

cleanedTau_eq_mk_iff_cleanedTauNormalWord_eq_reduce

L192 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_eq_mk_iff_cleanedTauNormalWord_eq_reduce

Documentation

A cleaned \(\tau\)-rewrite equals FreeGroup.mk ys exactly when its normal word is FreeGroup.reduce ys.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_eq_mk_iff_cleanedTauNormalWord_eq_reduce
    {D : FiniteQuotientSchreierData X Q}
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    {q : Q} {w : FreeGroup X}
    {ys : List (D.NondegenerateSchreierSymbol × Bool)} :
    D.cleanedTau q w = FreeGroup.mk ys ↔
      D.cleanedTauNormalWord q w = FreeGroup.reduce ys

theorem

cleanedTauList_eq_mk_iff_cleanedTauListNormalWord_eq_reduce

L213 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTauList_eq_mk_iff_cleanedTauListNormalWord_eq_reduce

Documentation

The cleaned \(\tau\)-list normal word records the reduced list form of the cleaned \(\tau\)-list rewrite.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem cleanedTauList_eq_mk_iff_cleanedTauListNormalWord_eq_reduce
    {D : FiniteQuotientSchreierData X Q}
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    {q : Q} {xs : List (X × Bool)}
    {ys : List (D.NondegenerateSchreierSymbol × Bool)} :
    D.cleanedTauList q xs = FreeGroup.mk ys ↔
      D.cleanedTauListNormalWord q xs = FreeGroup.reduce ys

theorem

targetLift_cleanedTau_eq_mk_of_substitutionWord_reduce_eq

L233 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.targetLift_cleanedTau_eq_mk_of_substitutionWord_reduce_eq

Documentation

If the substituted cleaned \(\tau\)-normal word reduces to \(ys\), then the target lift of the cleaned \(\tau\)-word is \(\mathrm{FreeGroup.mk}(ys)\).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem targetLift_cleanedTau_eq_mk_of_substitutionWord_reduce_eq
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    {Y : Type*} [DecidableEq Y]
    {toTargetGenerator : D.NondegenerateSchreierSymbol → FreeGroup Y}
    (q : Q) (w : FreeGroup X) {ys : List (Y × Bool)}
    (h :
      FreeGroup.reduce
          (freeGroupSubstitutionWord toTargetGenerator
            (D.cleanedTauNormalWord q w)) =
        FreeGroup.reduce ys) :
    FreeGroup.lift toTargetGenerator (D.cleanedTau q w) =
      FreeGroup.mk ys

theorem

targetLift_cleanedTau_relatorEquivalent_one_of_substitutionWord_reduce_eq

L253 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.targetLift_cleanedTau_relatorEquivalent_one_of_substitutionWord_reduce_eq

Documentation

If the substituted cleaned \(\tau\)-normal word reduces to a word relator-equivalent to \(1\), then the target lift of the cleaned \(\tau\)-word is relator-equivalent to \(1\).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem targetLift_cleanedTau_relatorEquivalent_one_of_substitutionWord_reduce_eq
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    {Y : Type*} [DecidableEq Y]
    {S : Set (FreeGroup Y)}
    {toTargetGenerator : D.NondegenerateSchreierSymbol → FreeGroup Y}
    (q : Q) (w : FreeGroup X) {ys : List (Y × Bool)}
    (h :
      FreeGroup.reduce
          (freeGroupSubstitutionWord toTargetGenerator
            (D.cleanedTauNormalWord q w)) =
        FreeGroup.reduce ys)
    (hy : RelatorEquivalent S (FreeGroup.mk ys) 1) :
    RelatorEquivalent S
      (FreeGroup.lift toTargetGenerator (D.cleanedTau q w)) 1

theorem

targetLift_cleanedTau_relatorEquivalent_one_of_substitutionWord_reduce_mem

L276 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.targetLift_cleanedTau_relatorEquivalent_one_of_substitutionWord_reduce_mem

Documentation

If the substituted cleaned \(\tau\)-normal word reduces to a target relator, then the target lift of the cleaned \(\tau\)-word is relator-equivalent to \(1\).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem targetLift_cleanedTau_relatorEquivalent_one_of_substitutionWord_reduce_mem
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    {Y : Type*} [DecidableEq Y]
    {S : Set (FreeGroup Y)}
    {toTargetGenerator : D.NondegenerateSchreierSymbol → FreeGroup Y}
    (q : Q) (w : FreeGroup X) {ys : List (Y × Bool)}
    (h :
      FreeGroup.reduce
          (freeGroupSubstitutionWord toTargetGenerator
            (D.cleanedTauNormalWord q w)) =
        FreeGroup.reduce ys)
    (hy : FreeGroup.mk ys ∈ S) :
    RelatorEquivalent S
      (FreeGroup.lift toTargetGenerator (D.cleanedTau q w)) 1

theorem

mapsCleanedRelators_of_cleanedTauNormalWord_reduce

L300 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mapsCleanedRelators_of_cleanedTauNormalWord_reduce

Documentation

If substitution reduces every cleaned source relator to a target word relator-equivalent to \(1\), then the induced generator map sends every cleaned relator to a word relator-equivalent to \(1\).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem mapsCleanedRelators_of_cleanedTauNormalWord_reduce
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    {Y : Type*} [DecidableEq Y]
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    {toTargetGenerator : D.NondegenerateSchreierSymbol → FreeGroup Y}
    (targetWord : Q → FreeGroup X → List (Y × Bool))
    (hword :
      ∀ q : Q, ∀ r ∈ R,
        FreeGroup.reduce
            (freeGroupSubstitutionWord toTargetGenerator
              (D.cleanedTauNormalWord q r)) =
          FreeGroup.reduce (targetWord q r))
    (hrel :
      ∀ q : Q, ∀ r ∈ R,
        RelatorEquivalent S (FreeGroup.mk (targetWord q r)) 1) :
    ∀ q : Q, ∀ r ∈ R,
      RelatorEquivalent S
        (FreeGroup.lift toTargetGenerator (D.cleanedTau q r)) 1

theorem

mapsCleanedRelators_of_cleanedTauNormalWord_reduce_mem

L329 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mapsCleanedRelators_of_cleanedTauNormalWord_reduce_mem

Documentation

If substitution reduces every cleaned source relator to a word in the target relator set, then the induced generator map sends every cleaned relator to a word relator-equivalent to \(1\).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem mapsCleanedRelators_of_cleanedTauNormalWord_reduce_mem
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq D.NondegenerateSchreierSymbol]
    {Y : Type*} [DecidableEq Y]
    {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
    {toTargetGenerator : D.NondegenerateSchreierSymbol → FreeGroup Y}
    (targetWord : Q → FreeGroup X → List (Y × Bool))
    (hword :
      ∀ q : Q, ∀ r ∈ R,
        FreeGroup.reduce
            (freeGroupSubstitutionWord toTargetGenerator
              (D.cleanedTauNormalWord q r)) =
          FreeGroup.reduce (targetWord q r))
    (hmem :
      ∀ q : Q, ∀ r ∈ R, FreeGroup.mk (targetWord q r) ∈ S) :
    ∀ q : Q, ∀ r ∈ R,
      RelatorEquivalent S
        (FreeGroup.lift toTargetGenerator (D.cleanedTau q r)) 1

theorem

cleanedTau_one

L352 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_one

Documentation

The \(\tau\)-word for the identity case evaluates to the identity.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_one
    [DecidablePred D.IsDegenerateSchreierSymbol] (q : Q) :
    D.cleanedTau q 1 = 1

theorem

cleanedTau_mul

L361 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_mul

Documentation

The cleaned \(\tau\)-rewrite of a product factors into the rewrite of the first word and the rewrite of the second word from the updated quotient element.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_mul
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (u v : FreeGroup X) :
    D.cleanedTau q (u * v) =
      D.cleanedTau q u *
        D.cleanedTau (D.quotientMap (D.quotientSection q * u)) v

theorem

cleanedTau_mul_of_mem_kernel

L373 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_mul_of_mem_kernel

Documentation

For a kernel word, the cleaned \(\tau\)-rewriting preserves products from the identity quotient element.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_mul_of_mem_kernel
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {u : FreeGroup X} (hu : u ∈ D.kernel) (v : FreeGroup X) :
    D.cleanedTau 1 (u * v) = D.cleanedTau 1 u * D.cleanedTau 1 v

theorem

cleanedTau_inv

L384 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_inv

Documentation

The cleaned \(\tau\)-rewrite of an inverse is the inverse of the \(\tau\)-rewrite from the updated quotient element.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_inv
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (u : FreeGroup X) :
    D.cleanedTau (D.quotientMap (D.quotientSection q * u)) u⁻¹ =
      (D.cleanedTau q u)⁻¹

theorem

cleanedTau_inv_of_mem_kernel

L397 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_inv_of_mem_kernel

Documentation

For a kernel word, the cleaned \(\tau\)-rewriting commutes with inversion from the identity quotient element.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_inv_of_mem_kernel
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {u : FreeGroup X} (hu : u ∈ D.kernel) :
    D.cleanedTau 1 u⁻¹ = (D.cleanedTau 1 u)⁻¹

theorem

nondegenerateSymbolEvalHom_cleanedTau

L408 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.nondegenerateSymbolEvalHom_cleanedTau

Documentation

Evaluating a cleaned \(\tau\)-word through nondegenerate symbols gives the same quotient-section conjugate as the uncleaned \(\tau\)-word.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem nondegenerateSymbolEvalHom_cleanedTau
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) (w : FreeGroup X) :
    D.nondegenerateSymbolEvalHom (D.cleanedTau q w) =
      D.quotientSection q * w *
        (D.quotientSection
          (D.quotientMap (D.quotientSection q * w)))⁻¹

theorem

cleanedTau_pow_of_mem_kernel

L421 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_pow_of_mem_kernel

Documentation

For a kernel word, cleaned \(\tau\) sends natural powers to powers of the cleaned \(\tau\)-word.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_pow_of_mem_kernel
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {u : FreeGroup X} (hu : u ∈ D.kernel) (n : ℕ) :
    D.cleanedTau 1 (u ^ n) = (D.cleanedTau 1 u) ^ n

theorem

cleanedTau_zpow_of_mem_kernel

L436 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_zpow_of_mem_kernel

Documentation

For a kernel word, cleaned \(\tau\) sends integer powers to powers of the cleaned \(\tau\)-word.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_zpow_of_mem_kernel
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {u : FreeGroup X} (hu : u ∈ D.kernel) (n : ℤ) :
    D.cleanedTau 1 (u ^ n) = (D.cleanedTau 1 u) ^ n

theorem

cleanedTau_conj_of_mem_kernel

L459 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedTau_conj_of_mem_kernel

Documentation

For kernel words, cleaned \(\tau\) sends a conjugate to the conjugate of the cleaned \(\tau\)-words.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]

Lean source · statement

theorem cleanedTau_conj_of_mem_kernel
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {a u : FreeGroup X} (ha : a ∈ D.kernel) (hu : u ∈ D.kernel) :
    D.cleanedTau 1 (a * u * a⁻¹) =
      D.cleanedTau 1 a * D.cleanedTau 1 u * (D.cleanedTau 1 a)⁻¹

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Cleaned Tau

Declarations