NYLL
Module

Tau.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Tau
20 declarations indexed from sourceView source ↗

Module documentation

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

This module defines the finite-state tau rewriting of signed words into Schreier symbols and proves compatibility with concatenation, cancellation, reduction, and free-group multiplication.

Imports1
Imported by2

Declarations

def

tauList

L29 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList
Documentation

Schreier rewriting of a raw word list, indexed by quotient states.

Source context 5 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)
Lean source · full declaration
def tauList : Q → List (X × Bool) → FreeGroup (FiniteSchreierSymbol X Q)
  | _q, [] => 1
  | q, (x, true) :: xs =>
      FreeGroup.of (q, x) * tauList (D.transition q x) xs
  | q, (x, false) :: xs =>
      (FreeGroup.of (D.inverseTransition q x, x))⁻¹ *
        tauList (D.inverseTransition q x) xs
theorem

tauList_cons_true_false

L39 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_cons_true_false
Documentation

The \(\tau\)-list rewrite is unchanged when adjacent inverse letters cancel.

Source context 5 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)
Lean source · statement
theorem tauList_cons_true_false
    (q : Q) (x : X) (xs : List (X × Bool)) :
    D.tauList q ((x, true) :: (x, false) :: xs) =
      D.tauList q xs
theorem

tauList_cons_false_true

L48 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_cons_false_true
Documentation

The \(\tau\)-list rewrite is unchanged when adjacent inverse letters cancel.

Source context 5 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)
Lean source · statement
theorem tauList_cons_false_true
    (q : Q) (x : X) (xs : List (X × Bool)) :
    D.tauList q ((x, false) :: (x, true) :: xs) =
      D.tauList q xs
theorem

tauList_cons_cancel

L57 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_cons_cancel
Documentation

The \(\tau\)-list rewrite is unchanged when adjacent inverse letters cancel.

Source context 5 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)
Lean source · statement
theorem tauList_cons_cancel
    (q : Q) (x : X) (b : Bool) (xs : List (X × Bool)) :
    D.tauList q ((x, b) :: (x, !b) :: xs) =
      D.tauList q xs
theorem

tauList_append

L69 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_append
Documentation

The \(\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 5 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)
Lean source · statement
theorem tauList_append
    (q : Q) (xs ys : List (X × Bool)) :
    D.tauList q (xs ++ ys) =
      D.tauList q xs *
        D.tauList
          (D.quotientMap (D.quotientSection q * FreeGroup.mk xs)) ys
theorem

tauList_redStep

L90 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_redStep
Documentation

A single free-group reduction step does not change the \(\tau\)-list rewrite.

Source context 5 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)
Lean source · statement
theorem tauList_redStep
    (q : Q) {xs ys : List (X × Bool)}
    (h : FreeGroup.Red.Step xs ys) :
    D.tauList q xs = D.tauList q ys
theorem

tauList_red

L100 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_red
Documentation

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

Source context 5 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)
Lean source · statement
theorem tauList_red
    (q : Q) {xs ys : List (X × Bool)}
    (h : FreeGroup.Red xs ys) :
    D.tauList q xs = D.tauList q ys
theorem

tauList_eq_of_mk_eq

L111 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_eq_of_mk_eq
Documentation

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

Source context 5 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)
Lean source · statement
theorem tauList_eq_of_mk_eq
    (q : Q) {xs ys : List (X × Bool)}
    (h : FreeGroup.mk xs = FreeGroup.mk ys) :
    D.tauList q xs = D.tauList q ys
theorem

symbolEvalHom_tauList

L120 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalHom_tauList
Documentation

Evaluating a \(\tau\)-list gives the quotient-section conjugate of the represented word.

Source context 5 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)
Lean source · statement
theorem symbolEvalHom_tauList
    (q : Q) (xs : List (X × Bool)) :
    D.symbolEvalHom (D.tauList q xs) =
      D.quotientSection q * FreeGroup.mk xs *
        (D.quotientSection
          (D.quotientMap (D.quotientSection q * FreeGroup.mk xs)))⁻¹
def

tau

L144 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau
Documentation

Finite-quotient Schreier rewriting of a free-group 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
def tau (q : Q) (w : FreeGroup X) : FreeGroup (FiniteSchreierSymbol X Q)
theorem

tau_one

L149 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_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 tau_one (q : Q) :
    D.tau q 1 = 1
theorem

tau_of

L155 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_of
Documentation

\(\tau\)-rewriting of a single generator gives the corresponding finite Schreier symbol.

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 tau_of (q : Q) (x : X) :
    D.tau q (FreeGroup.of x) = FreeGroup.of (q, x)
theorem

tau_mk

L160 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_mk
Documentation

The \(\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 tau_mk (q : Q) (xs : List (X × Bool)) :
    D.tau q (FreeGroup.mk xs) = D.tauList q xs
theorem

symbolEvalHom_tau

L166 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalHom_tau
Documentation

Evaluating a \(\tau\)-word gives the quotient-section conjugate of the rewritten 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 symbolEvalHom_tau (q : Q) (w : FreeGroup X) :
    D.symbolEvalHom (D.tau q w) =
      D.quotientSection q * w *
        (D.quotientSection (D.quotientMap (D.quotientSection q * w)))⁻¹
theorem

tau_mul

L177 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_mul
Documentation

The \(\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 tau_mul (q : Q) (u v : FreeGroup X) :
    D.tau q (u * v) =
      D.tau q u *
        D.tau (D.quotientMap (D.quotientSection q * u)) v
theorem

tau_mul_of_mem_kernel

L199 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_mul_of_mem_kernel
Documentation

For a kernel word, the \(\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 tau_mul_of_mem_kernel
    {u v : FreeGroup X} (hu : u ∈ D.kernel) :
    D.tau 1 (u * v) = D.tau 1 u * D.tau 1 v
theorem

tau_inv

L210 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_inv
Documentation

The \(\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 tau_inv (q : Q) (u : FreeGroup X) :
    D.tau (D.quotientMap (D.quotientSection q * u)) u⁻¹ =
      (D.tau q u)⁻¹
theorem

tau_inv_of_mem_kernel

L238 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_inv_of_mem_kernel
Documentation

For a kernel word, the \(\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 tau_inv_of_mem_kernel
    {u : FreeGroup X} (hu : u ∈ D.kernel) :
    D.tau 1 u⁻¹ = (D.tau 1 u)⁻¹
theorem

symbolEvalHom_tau_of_mem_kernel

L249 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalHom_tau_of_mem_kernel
Documentation

For a kernel word, evaluating its \(\tau\)-rewrite from the identity quotient state recovers the original 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 symbolEvalHom_tau_of_mem_kernel
    {w : FreeGroup X} (hw : w ∈ D.kernel) :
    D.symbolEvalHom (D.tau 1 w) = w
def

schreierRelators

L261 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.schreierRelators
Documentation

The finite-quotient Schreier relator set consists of the \(\tau\)-rewrites of the original relators at all quotient states.

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 schreierRelators (R : Set (FreeGroup X)) :
    Set (FreeGroup (FiniteSchreierSymbol X Q))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.