NYLL
Module

Rewriting.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.Rewriting
136 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Rewriting

This module defines abstract right Schreier representatives, their associated symbols and generators, and the rewriting maps that turn kernel words into words on Schreier symbols.

Imports3
Imported by2

Declarations

structure

RightSchreierRepresentative

L31 ↗
ReidemeisterSchreier.Discrete.RightSchreierRepresentative
Documentation

A normalized representative function for right cosets of \(L\) in a free group. The condition \(g(\operatorname{rep}(g))^{-1}\in L\) says that \(\operatorname{rep}(g)\) represents the same right coset as \(g\).

Source context 3 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
Lean source · full declaration
structure RightSchreierRepresentative (L : Subgroup (FreeGroup X)) where
  /-- The chosen representative of the right coset of each free-group element. -/
  representative : FreeGroup X → FreeGroup X
  /-- Every element and its chosen representative belong to the same right coset of \(L\). -/
  sameRightCoset : ∀ g, g * (representative g)⁻¹ ∈ L
  /-- Elements in the same right coset receive the same representative. -/
  representative_eq_of_sameRightCoset :
    ∀ {g h}, g * h⁻¹ ∈ L → representative g = representative h
  /-- The identity coset is represented by the identity. -/
  representative_one : representative 1 = 1
theorem

representative_mul_inv_mem

L47 ↗
ReidemeisterSchreier.Discrete.RightSchreierRepresentative.representative_mul_inv_mem
Documentation

A representative differs from the original element by an element of the subgroup.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace RightSchreierRepresentative
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem representative_mul_inv_mem (g : FreeGroup X) :
    S.representative g * g⁻¹ ∈ L
theorem

representative_eq_one_of_mem

L52 ↗
ReidemeisterSchreier.Discrete.RightSchreierRepresentative.representative_eq_one_of_mem
Documentation

The right Schreier representative is the identity exactly in the subgroup-membership case.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace RightSchreierRepresentative
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem representative_eq_one_of_mem {g : FreeGroup X} (hg : g ∈ L) :
    S.representative g = 1
theorem

representative_mul_generator_eq

L63 ↗
ReidemeisterSchreier.Discrete.RightSchreierRepresentative.representative_mul_generator_eq
Documentation

Replacing a word by its chosen right Schreier representative does not change the representative selected after multiplying by a generator.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace RightSchreierRepresentative
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem representative_mul_generator_eq (p : FreeGroup X) (x : X) :
    S.representative (S.representative p * FreeGroup.of x) =
      S.representative (p * FreeGroup.of x)
theorem

representative_inv_generator_mul_generator_eq

L75 ↗
ReidemeisterSchreier.Discrete.RightSchreierRepresentative.representative_inv_generator_mul_generator_eq
Documentation

After moving backward by a generator, replacing the resulting word by its representative and then moving forward selects the original word's representative.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace RightSchreierRepresentative
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem representative_inv_generator_mul_generator_eq (p : FreeGroup X) (x : X) :
    S.representative (S.representative (p * (FreeGroup.of x)⁻¹) * FreeGroup.of x) =
      S.representative p
abbrev

SchreierSymbol

L89 ↗
ReidemeisterSchreier.Discrete.SchreierSymbol
Documentation

Labels for Schreier generators. A label \((t,x)\) represents the generator \(t x\overline{t x}^{-1}\).

Source context 3 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
Lean source · statement
abbrev SchreierSymbol (X : Type*)
def

schreierGenerator

L99 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.schreierGenerator
Documentation

The Schreier generator is the correction term \(t x \overline{t x}^{-1}\) attached to a representative and a generator.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
def schreierGenerator (t : FreeGroup X) (x : X) : FreeGroup X
def

symbolEval

L103 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEval
Documentation

Evaluation of one Schreier symbol as its Schreier generator in the free group.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
def symbolEval (z : SchreierSymbol X) : FreeGroup X
theorem

symbolEval_mem

L107 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEval_mem
Documentation

Each evaluated Schreier symbol lies in the subgroup being rewritten.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEval_mem (z : SchreierSymbol X) :
    symbolEval S z ∈ L
def

symbolEvalHom

L113 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom
Documentation

The homomorphism extending Schreier-symbol evaluation to the free group on Schreier symbols.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
def symbolEvalHom : FreeGroup (SchreierSymbol X) →* FreeGroup X
theorem

symbolEvalHom_of

L118 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom_of
Documentation

The evaluation homomorphism sends a Schreier-symbol generator to its symbol evaluation.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEvalHom_of (z : SchreierSymbol X) :
    symbolEvalHom S (FreeGroup.of z) = symbolEval S z
theorem

symbolEvalHom_mem

L125 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom_mem
Documentation

The image of the Schreier-symbol evaluation homomorphism lies in the subgroup being rewritten.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEvalHom_mem (q : FreeGroup (SchreierSymbol X)) :
    symbolEvalHom S q ∈ L
def

symbolEvalSubgroupHom

L136 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalSubgroupHom
Documentation

Evaluation as a homomorphism into the subgroup being rewritten.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · full declaration
def symbolEvalSubgroupHom : FreeGroup (SchreierSymbol X) →* L where
  toFun q := ⟨symbolEvalHom S q, symbolEvalHom_mem (S := S) q⟩
  map_one' := Subtype.ext (symbolEvalHom S).map_one
  map_mul' q r := Subtype.ext ((symbolEvalHom S).map_mul q r)
theorem

symbolEvalSubgroupHom_apply

L146 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalSubgroupHom_apply
Documentation

Forgetting the subgroup target of \(\mathrm{symbolEvalSubgroupHom}\) gives the ordinary evaluation homomorphism.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEvalSubgroupHom_apply (q : FreeGroup (SchreierSymbol X)) :
    (symbolEvalSubgroupHom S q : FreeGroup X) = symbolEvalHom S q
theorem

symbolEval_representative_mul_generator

L155 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEval_representative_mul_generator
Documentation

Evaluation of the Schreier symbol starting at a chosen representative has the expected positive-letter formula.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEval_representative_mul_generator (p : FreeGroup X) (x : X) :
    symbolEval S (S.representative p, x) =
      S.representative p * FreeGroup.of x * (S.representative (p * FreeGroup.of x))⁻¹
theorem

symbolEval_representative_inv_generator

L166 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEval_representative_inv_generator
Documentation

Evaluation of the Schreier symbol for an inverse-letter step has the expected representative formula.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEval_representative_inv_generator (p : FreeGroup X) (x : X) :
    symbolEval S (S.representative (p * (FreeGroup.of x)⁻¹), x) =
      S.representative (p * (FreeGroup.of x)⁻¹) *
        FreeGroup.of x * (S.representative p)⁻¹
theorem

mk_cons_true

L178 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.mk_cons_true
Documentation

A word list beginning with a positive letter represents that generator multiplied by the word represented by the tail.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem mk_cons_true (x : X) (xs : List (X × Bool)) :
    FreeGroup.mk ((x, true) :: xs) =
      FreeGroup.of x * FreeGroup.mk xs
theorem

mk_cons_false

L191 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.mk_cons_false
Documentation

A word list beginning with a negative letter represents the inverse generator multiplied by the word represented by the tail.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem mk_cons_false (x : X) (xs : List (X × Bool)) :
    FreeGroup.mk ((x, false) :: xs) =
      (FreeGroup.of x)⁻¹ * FreeGroup.mk xs
def

tauList

L200 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.tauList
Documentation

Schreier rewriting of a raw word list, starting from prefix \(p\).

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · full declaration
def tauList : FreeGroup X → List (X × Bool) → FreeGroup (SchreierSymbol X)
  | _p, [] => 1
  | p, (x, true) :: xs =>
      FreeGroup.of (S.representative p, x) *
        tauList (p * FreeGroup.of x) xs
  | p, (x, false) :: xs =>
      (FreeGroup.of (S.representative (p * (FreeGroup.of x)⁻¹), x))⁻¹ *
        tauList (p * (FreeGroup.of x)⁻¹) xs
theorem

symbolEvalHom_tauList

L211 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEvalHom_tauList
    (p : FreeGroup X) (xs : List (X × Bool)) :
    symbolEvalHom S (tauList S p xs) =
      S.representative p * FreeGroup.mk xs *
        (S.representative (p * FreeGroup.mk xs))⁻¹
theorem

tauList_append

L235 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem tauList_append
    (p : FreeGroup X) (xs ys : List (X × Bool)) :
    tauList S p (xs ++ ys) =
      tauList S p xs * tauList S (p * FreeGroup.mk xs) ys
theorem

symbolEvalHom_tauList_mem

L251 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom_tauList_mem
Documentation

The symbol evaluation of the \(\tau\)-rewrite lies in the Schreier subgroup kernel.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
Lean source · statement
theorem symbolEvalHom_tauList_mem
    (p : FreeGroup X) (xs : List (X × Bool)) :
    symbolEvalHom S (tauList S p xs) ∈ L
def

tau

L264 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.tau
Documentation

Explicit 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def tau (t w : FreeGroup X) : FreeGroup (SchreierSymbol X)
theorem

symbolEvalHom_tau

L268 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalHom_tau
    (t w : FreeGroup X) :
    symbolEvalHom S (tau S t w) =
      S.representative t * w * (S.representative (t * w))⁻¹
theorem

symbolEvalHom_tau_mem

L275 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom_tau_mem
Documentation

The symbol evaluation of the \(\tau\)-rewrite lies in the Schreier subgroup kernel.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalHom_tau_mem
    (t w : FreeGroup X) :
    symbolEvalHom S (tau S t w) ∈ L
theorem

symbolEvalHom_tau_of_representative

L284 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom_tau_of_representative
Documentation

When the starting word is already the chosen representative, evaluating \(\tau\) gives that representative times the word and the inverse of the next representative.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalHom_tau_of_representative
    {t w : FreeGroup X} (ht : S.representative t = t) :
    symbolEvalHom S (tau S t w) =
      t * w * (S.representative (t * w))⁻¹
theorem

symbolEvalHom_tau_one_of_mem

L294 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom_tau_one_of_mem
Documentation

For a word in the Schreier subgroup, evaluating its \(\tau\)-rewrite from the identity representative recovers that word.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalHom_tau_one_of_mem
    {w : FreeGroup X} (hw : w ∈ L) :
    symbolEvalHom S (tau S 1 w) = w
def

representativeSet

L302 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSet
Documentation

The set of representatives selected by a normalized Schreier representative function.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeSet : Set (FreeGroup X)
def

schreierRelatorsOn

L309 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.schreierRelatorsOn
Documentation

The Schreier relators attached to a relator set \(R\) and an explicit transversal \(T\): all rewrites \(\tau(t,r)\) with \(t \in T\).

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def schreierRelatorsOn
    (T : Set (FreeGroup X)) (R : Set (FreeGroup X)) :
    Set (FreeGroup (SchreierSymbol X))
def

schreierRelators

L318 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.schreierRelators
Documentation

The default Schreier relator set is formed by rewriting relators with the range of the representative function as the transversal.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def schreierRelators (R : Set (FreeGroup X)) :
    Set (FreeGroup (SchreierSymbol X))
def

degenerateSchreierRelatorsOn

L326 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.degenerateSchreierRelatorsOn
Documentation

Degenerate Schreier generators \(s(t,x)\) whose evaluation is already \(1\). These are the Tietze-removable generators in the raw Reidemeister--Schreier presentation.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def degenerateSchreierRelatorsOn
    (T : Set (FreeGroup X)) :
    Set (FreeGroup (SchreierSymbol X))
def

degenerateSchreierRelators

L334 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.degenerateSchreierRelators
Documentation

The set of degenerate Schreier relators for the default representative set.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def degenerateSchreierRelators :
    Set (FreeGroup (SchreierSymbol X))
def

presentationRelatorsOn

L342 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.presentationRelatorsOn
Documentation

The raw relator set for the Reidemeister--Schreier presentation: rewritten original relators plus degenerate 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def presentationRelatorsOn
    (T : Set (FreeGroup X)) (R : Set (FreeGroup X)) :
    Set (FreeGroup (SchreierSymbol X))
def

presentationRelators

L351 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.presentationRelators
Documentation

The Reidemeister--Schreier presentation relators are the Schreier relators together with the degenerate Schreier-generator relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def presentationRelators
    (R : Set (FreeGroup X)) :
    Set (FreeGroup (SchreierSymbol X))
theorem

tau_mem_schreierRelatorsOn

L360 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.tau_mem_schreierRelatorsOn
Documentation

The \(\tau\)-rewrite of an original relator at a chosen representative belongs to the Schreier relator set on that representative set.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem tau_mem_schreierRelatorsOn
    {T R : Set (FreeGroup X)} {t : FreeGroup X} (ht : t ∈ T)
    {r : FreeGroup X} (hr : r ∈ R) :
    tau S t r ∈ schreierRelatorsOn S T R
theorem

tau_representative_mem_schreierRelators

L370 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.tau_representative_mem_schreierRelators
Documentation

The \(\tau\)-rewrite at the canonical representative of an original relator belongs to the default Schreier relator set.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem tau_representative_mem_schreierRelators
    {R : Set (FreeGroup X)} (t : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    tau S (S.representative t) r ∈ schreierRelators S R
theorem

degenerateSchreierRelator_eval_eq_one

L380 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.degenerateSchreierRelator_eval_eq_one
Documentation

Every degenerate Schreier relator evaluates to the identity under the Schreier evaluation map.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem degenerateSchreierRelator_eval_eq_one
    {T : Set (FreeGroup X)}
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ degenerateSchreierRelatorsOn S T) :
    symbolEvalHom S q = 1
theorem

eval_degenerateSchreierRelator_mem_normalClosure

L394 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_degenerateSchreierRelator_mem_normalClosure
Documentation

The evaluation of a degenerate Schreier relator lies in the normal closure of the defining source relators.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem eval_degenerateSchreierRelator_mem_normalClosure
    {T R : Set (FreeGroup X)}
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ degenerateSchreierRelatorsOn S T) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

representative_mul_relator_eq

L406 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representative_mul_relator_eq
Documentation

Multiplying a chosen representative by an original relator does not change the chosen representative when the relators lie in the subgroup.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representative_mul_relator_eq
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (t : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    S.representative (t * r) = S.representative t
theorem

symbolEvalHom_tau_relator_mem_normalClosure

L420 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalHom_tau_relator_mem_normalClosure
Documentation

The symbol evaluation of the \(\tau\)-rewrite of a defining relator lies in the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalHom_tau_relator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (t : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    symbolEvalHom S (tau S t r) ∈ Subgroup.normalClosure R
theorem

eval_schreierRelatorOn_mem_normalClosure

L436 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_schreierRelatorOn_mem_normalClosure
Documentation

Evaluating a Schreier relator on a specified representative set gives an element of the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_schreierRelatorOn_mem_normalClosure
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ schreierRelatorsOn S T R) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

eval_schreierRelator_mem_normalClosure

L449 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_schreierRelator_mem_normalClosure
Documentation

Evaluating a default Schreier relator gives an element of the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_schreierRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ schreierRelators S R) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

eval_mem_normalClosure_of_mem_normalClosure_schreierRelatorsOn

L461 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_mem_normalClosure_of_mem_normalClosure_schreierRelatorsOn
Documentation

Membership in the source relator normal closure is preserved by the Reidemeister--Schreier evaluation map.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_mem_normalClosure_of_mem_normalClosure_schreierRelatorsOn
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ Subgroup.normalClosure (schreierRelatorsOn S T R)) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

eval_mem_normalClosure_of_mem_normalClosure_schreierRelators

L474 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_mem_normalClosure_of_mem_normalClosure_schreierRelators
Documentation

Membership in the source relator normal closure is preserved by the Reidemeister--Schreier evaluation map.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_mem_normalClosure_of_mem_normalClosure_schreierRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ Subgroup.normalClosure (schreierRelators S R)) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

eval_presentationRelatorOn_mem_normalClosure

L486 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_presentationRelatorOn_mem_normalClosure
Documentation

Evaluating a presentation relator on a specified representative set gives an element of the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_presentationRelatorOn_mem_normalClosure
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ presentationRelatorsOn S T R) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

eval_mem_normalClosure_of_mem_normalClosure_presentationRelatorsOn

L500 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_mem_normalClosure_of_mem_normalClosure_presentationRelatorsOn
Documentation

Membership in the source relator normal closure is preserved by the Reidemeister--Schreier evaluation map.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_mem_normalClosure_of_mem_normalClosure_presentationRelatorsOn
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ Subgroup.normalClosure (presentationRelatorsOn S T R)) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

eval_mem_normalClosure_of_mem_normalClosure_presentationRelators

L513 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_mem_normalClosure_of_mem_normalClosure_presentationRelators
Documentation

Membership in the source relator normal closure is preserved by the Reidemeister--Schreier evaluation map.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_mem_normalClosure_of_mem_normalClosure_presentationRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ Subgroup.normalClosure (presentationRelators S R)) :
    symbolEvalHom S q ∈ Subgroup.normalClosure R
def

relatorSubgroup

L522 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.relatorSubgroup
Documentation

The subgroup of \(L\) induced by the ambient normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · full declaration
def relatorSubgroup
    (R : Set (FreeGroup X)) :
    Subgroup L where
  carrier := {g | (g : FreeGroup X) ∈ Subgroup.normalClosure R}
  one_mem' := by
    simp only [Set.mem_ofPred_eq, OneMemClass.coe_one, one_mem]
  mul_mem' := by
    intro a b ha hb
    exact Subgroup.mul_mem (Subgroup.normalClosure R) ha hb
  inv_mem' := by
    intro a ha
    exact Subgroup.inv_mem (Subgroup.normalClosure R) ha
instance

relatorSubgroup_normal

L536 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.relatorSubgroup_normal
Documentation

The subgroup generated by the relators of the presented group is normal.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · full declaration
instance relatorSubgroup_normal
    (R : Set (FreeGroup X)) :
    (relatorSubgroup (L := L) R).Normal where
  conj_mem n hn g := by
    change ((g : FreeGroup X) * (n : FreeGroup X) * (g : FreeGroup X)⁻¹) ∈
      Subgroup.normalClosure R
    simpa [mul_assoc] using
      (Subgroup.normalClosure_normal.conj_mem
        (n : FreeGroup X) hn (g : FreeGroup X))
theorem

symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_schreierRelatorsOn

L550 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_schreierRelatorsOn
Documentation

The symbol-evaluation subgroup homomorphism sends the indicated normal-closure element into the relator subgroup.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_schreierRelatorsOn
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (SchreierSymbol X)}
    (hq : q ∈ Subgroup.normalClosure (schreierRelatorsOn S T R)) :
    symbolEvalSubgroupHom S q ∈ relatorSubgroup (L := L) R
def

symbolEvalQuotientHomOn

L562 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalQuotientHomOn
Documentation

The canonical map from the raw Schreier-relator quotient to the subgroup quotient \(L/(L \cap \langle\!\langle R \rangle\!\rangle)\).

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def symbolEvalQuotientHomOn
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    FreeGroup (SchreierSymbol X) ⧸
        Subgroup.normalClosure (schreierRelatorsOn S T R) →*
      L ⧸ relatorSubgroup (L := L) R
def

symbolEvalQuotientHom

L585 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalQuotientHom
Documentation

The canonical evaluation map from the Schreier-relator quotient to the relator-subgroup quotient of the subgroup.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def symbolEvalQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    FreeGroup (SchreierSymbol X) ⧸
        Subgroup.normalClosure (schreierRelators S R) →*
      L ⧸ relatorSubgroup (L := L) R
def

symbolEvalPresentationQuotientHomOn

L597 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalPresentationQuotientHomOn
Documentation

The evaluation map from a raw presentation quotient with a specified transversal set to the relator-subgroup quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def symbolEvalPresentationQuotientHomOn
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    FreeGroup (SchreierSymbol X) ⧸
        Subgroup.normalClosure (presentationRelatorsOn S T R) →*
      L ⧸ relatorSubgroup (L := L) R
def

symbolEvalPresentationQuotientHom

L619 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalPresentationQuotientHom
Documentation

The evaluation map from the raw Schreier presentation quotient to the relator-subgroup quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def symbolEvalPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    FreeGroup (SchreierSymbol X) ⧸
        Subgroup.normalClosure (presentationRelators S R) →*
      L ⧸ relatorSubgroup (L := L) R
theorem

symbolEvalPresentationQuotientHomOn_surjective

L628 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalPresentationQuotientHomOn_surjective
Documentation

The specified-transversal presentation evaluation quotient map is surjective.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalPresentationQuotientHomOn_surjective
    {T R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    Function.Surjective (symbolEvalPresentationQuotientHomOn (S := S) (T := T) hR)
theorem

symbolEvalPresentationQuotientHom_surjective

L645 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.symbolEvalPresentationQuotientHom_surjective
Documentation

The raw Schreier presentation evaluation quotient map is surjective.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem symbolEvalPresentationQuotientHom_surjective
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    Function.Surjective (symbolEvalPresentationQuotientHom (S := S) hR)
theorem

eval_tau_one_relator_mem_normalClosure

L655 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.eval_tau_one_relator_mem_normalClosure
Documentation

The kernel relator case: if an original relator lies in the subgroup being rewritten, its rewrite from the identity evaluates back to that relator.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem eval_tau_one_relator_mem_normalClosure
    {R : Set (FreeGroup X)}
    {r : FreeGroup X} (hr : r ∈ R) (hrL : r ∈ L) :
    symbolEvalHom S (tau S 1 r) ∈ Subgroup.normalClosure R
abbrev

RepresentativeSchreierSymbol

L664 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.RepresentativeSchreierSymbol
Documentation

Schreier generator labels indexed by the chosen representative set.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
abbrev RepresentativeSchreierSymbol
def

representativeSchreierGenerator

L671 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSchreierGenerator
Documentation

The representative Schreier generator is the correction term determined by a representative and an original generator.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeSchreierGenerator
    (z : RepresentativeSchreierSymbol S) : FreeGroup X
def

representativeSymbolEval

L677 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEval
Documentation

Evaluation of one representative-indexed Schreier symbol as its Schreier generator.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeSymbolEval
    (z : RepresentativeSchreierSymbol S) : FreeGroup X
theorem

representativeSymbolEval_mem

L683 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEval_mem
Documentation

Each evaluated representative-indexed Schreier symbol lies in the subgroup being rewritten.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeSymbolEval_mem
    (z : RepresentativeSchreierSymbol S) :
    representativeSymbolEval S z ∈ L
def

representativeSymbolEvalHom

L690 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalHom
Documentation

The homomorphism extending representative-indexed Schreier-symbol evaluation.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeSymbolEvalHom :
    FreeGroup (RepresentativeSchreierSymbol S) →* FreeGroup X
theorem

representativeSymbolEvalHom_of

L700 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalHom_of
Documentation

The representative evaluation homomorphism sends a generator to its representative symbol evaluation.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeSymbolEvalHom_of
    (z : RepresentativeSchreierSymbol S) :
    representativeSymbolEvalHom S (FreeGroup.of z) =
      representativeSymbolEval S z
theorem

representativeSymbolEvalHom_mem

L708 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalHom_mem
Documentation

The image of the representative evaluation homomorphism lies in the subgroup being rewritten.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeSymbolEvalHom_mem
    (q : FreeGroup (RepresentativeSchreierSymbol S)) :
    representativeSymbolEvalHom S q ∈ L
def

representativeSymbolEvalSubgroupHom

L723 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalSubgroupHom
Documentation

Representative-indexed Schreier-symbol evaluation bundled as a homomorphism into the subgroup being rewritten.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · full declaration
def representativeSymbolEvalSubgroupHom :
    FreeGroup (RepresentativeSchreierSymbol S) →* L where
  toFun q := ⟨representativeSymbolEvalHom S q,
    representativeSymbolEvalHom_mem (S := S) q⟩
  map_one' := Subtype.ext (representativeSymbolEvalHom S).map_one
  map_mul' q r := Subtype.ext ((representativeSymbolEvalHom S).map_mul q r)
theorem

representativeSymbolEvalSubgroupHom_apply

L736 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalSubgroupHom_apply
Documentation

Forgetting the subgroup target of the representative evaluation homomorphism gives the ordinary representative evaluation homomorphism.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeSymbolEvalSubgroupHom_apply
    (q : FreeGroup (RepresentativeSchreierSymbol S)) :
    (representativeSymbolEvalSubgroupHom S q : FreeGroup X) =
      representativeSymbolEvalHom S q
def

representativeLabel

L743 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeLabel
Documentation

The representative label records the chosen representative attached to 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeLabel (p : FreeGroup X) (x : X) :
    RepresentativeSchreierSymbol S
def

representativeTauList

L748 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList
Documentation

Restricted Schreier rewriting of a raw word list.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · full declaration
def representativeTauList :
    FreeGroup X → List (X × Bool) → FreeGroup (RepresentativeSchreierSymbol S)
  | _p, [] => 1
  | p, (x, true) :: xs =>
      FreeGroup.of (representativeLabel S p x) *
        representativeTauList (p * FreeGroup.of x) xs
  | p, (x, false) :: xs =>
      (FreeGroup.of
        (representativeLabel S (p * (FreeGroup.of x)⁻¹) x))⁻¹ *
        representativeTauList (p * (FreeGroup.of x)⁻¹) xs
theorem

representativeTauList_cons_true_false

L762 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_cons_true_false
Documentation

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

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_cons_true_false
    (p : FreeGroup X) (x : X) (xs : List (X × Bool)) :
    representativeTauList S p ((x, true) :: (x, false) :: xs) =
      representativeTauList S p xs
theorem

representativeTauList_cons_false_true

L771 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_cons_false_true
Documentation

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

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_cons_false_true
    (p : FreeGroup X) (x : X) (xs : List (X × Bool)) :
    representativeTauList S p ((x, false) :: (x, true) :: xs) =
      representativeTauList S p xs
theorem

representativeTauList_cons_cancel

L780 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_cons_cancel
Documentation

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

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_cons_cancel
    (p : FreeGroup X) (x : X) (b : Bool) (xs : List (X × Bool)) :
    representativeTauList S p ((x, b) :: (x, !b) :: xs) =
      representativeTauList S p xs
theorem

representativeTauList_append

L793 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_append
Documentation

The representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_append
    (p : FreeGroup X) (xs ys : List (X × Bool)) :
    representativeTauList S p (xs ++ ys) =
      representativeTauList S p xs *
        representativeTauList S (p * FreeGroup.mk xs) ys
theorem

representativeTauList_eq_of_sameRightCoset

L810 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_eq_of_sameRightCoset
Documentation

Representative \(\tau\)-list rewrites agree for starting words in the same right coset.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_eq_of_sameRightCoset
    {p q : FreeGroup X} (hpq : p * q⁻¹ ∈ L)
    (xs : List (X × Bool)) :
    representativeTauList S p xs = representativeTauList S q xs
theorem

representativeTauList_redStep

L841 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_redStep
Documentation

A single free-group reduction step does not change the representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_redStep
    (p : FreeGroup X) {xs ys : List (X × Bool)}
    (h : FreeGroup.Red.Step xs ys) :
    representativeTauList S p xs = representativeTauList S p ys
theorem

representativeTauList_red

L852 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_red
Documentation

Free-group reduction does not change the representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_red
    (p : FreeGroup X) {xs ys : List (X × Bool)}
    (h : FreeGroup.Red xs ys) :
    representativeTauList S p xs = representativeTauList S p ys
theorem

representativeTauList_eq_of_mk_eq

L867 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_eq_of_mk_eq
Documentation

Equal free-group words have equal the representative \(\tau\)-list rewrites from the same starting 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_eq_of_mk_eq
    (p : FreeGroup X) {xs ys : List (X × Bool)}
    (h : FreeGroup.mk xs = FreeGroup.mk ys) :
    representativeTauList S p xs = representativeTauList S p ys
theorem

representativeSymbolEvalHom_representativeTauList

L878 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalHom_representativeTauList
Documentation

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

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeSymbolEvalHom_representativeTauList
    (p : FreeGroup X) (xs : List (X × Bool)) :
    representativeSymbolEvalHom S (representativeTauList S p xs) =
      S.representative p * FreeGroup.mk xs *
        (S.representative (p * FreeGroup.mk xs))⁻¹
def

representativeTau

L907 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau
Documentation

The representative \(\tau\)-map applies the explicit Schreier rewriting procedure to free-group elements.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeTau (t w : FreeGroup X) :
    FreeGroup (RepresentativeSchreierSymbol S)
theorem

representativeTau_one

L913 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_one
Documentation

Rewriting the identity word by the representative \(\tau\)-map gives 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_one (t : FreeGroup X) :
    representativeTau S t 1 = 1
theorem

representativeTau_mk

L921 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_mk
Documentation

The representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_mk
    (t : FreeGroup X) (xs : List (X × Bool)) :
    representativeTau S t (FreeGroup.mk xs) =
      representativeTauList S t xs
theorem

representativeSymbolEvalHom_tau

L929 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalHom_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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSymbolEvalHom_tau
    (t w : FreeGroup X) :
    representativeSymbolEvalHom S (representativeTau S t w) =
      S.representative t * w * (S.representative (t * w))⁻¹
theorem

representativeTau_mul

L940 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_mul
Documentation

The representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_mul
    (t u v : FreeGroup X) :
    representativeTau S t (u * v) =
      representativeTau S t u * representativeTau S (t * u) v
theorem

representativeTau_eq_of_sameRightCoset

L958 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_eq_of_sameRightCoset
Documentation

Representative \(\tau\)-words agree for group elements in the same right coset.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_eq_of_sameRightCoset
    {p q : FreeGroup X} (hpq : p * q⁻¹ ∈ L)
    (w : FreeGroup X) :
    representativeTau S p w = representativeTau S q w
theorem

representativeTau_eq_one_start_of_mem

L968 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_eq_one_start_of_mem
Documentation

If the initial word lies in the Schreier subgroup, its representative \(\tau\)-rewrite agrees with the rewrite starting at 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_eq_one_start_of_mem
    {p : FreeGroup X} (hp : p ∈ L) (w : FreeGroup X) :
    representativeTau S p w = representativeTau S 1 w
theorem

representativeTau_mul_of_mem

L977 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_mul_of_mem
Documentation

For a kernel word, the representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_mul_of_mem
    {u v : FreeGroup X} (hu : u ∈ L) :
    representativeTau S 1 (u * v) =
      representativeTau S 1 u * representativeTau S 1 v
theorem

representativeTau_inv

L991 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_inv
Documentation

The representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_inv (t u : FreeGroup X) :
    representativeTau S (t * u) u⁻¹ =
      (representativeTau S t u)⁻¹
theorem

representativeTau_inv_of_mem

L1015 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_inv_of_mem
Documentation

For a kernel word, the representative \(\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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_inv_of_mem
    {u : FreeGroup X} (hu : u ∈ L) :
    representativeTau S 1 u⁻¹ = (representativeTau S 1 u)⁻¹
theorem

representativeSymbolEvalHom_tau_one_of_mem

L1025 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalHom_tau_one_of_mem
Documentation

For a word in the Schreier subgroup, evaluating its representative \(\tau\)-rewrite from the identity recovers that word.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSymbolEvalHom_tau_one_of_mem
    {w : FreeGroup X} (hw : w ∈ L) :
    representativeSymbolEvalHom S (representativeTau S 1 w) = w
theorem

representative_representative

L1034 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representative_representative
Documentation

Applying the representative-selection map twice gives the same representative.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representative_representative (g : FreeGroup X) :
    S.representative (S.representative g) = S.representative g
theorem

representative_eq_self_of_mem_representativeSet

L1041 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representative_eq_self_of_mem_representativeSet
Documentation

An element of the representative set is fixed by the representative-selection map.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representative_eq_self_of_mem_representativeSet
    {t : FreeGroup X} (ht : t ∈ representativeSet S) :
    S.representative t = t
theorem

representativeTau_of_representative

L1048 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_of_representative
Documentation

The representative \(\tau\) of a chosen representative is trivial in the Schreier rewriting.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_of_representative
    (t : representativeSet S) (x : X) :
    representativeTau S (t : FreeGroup X) (FreeGroup.of x) =
      FreeGroup.of (t, x)
def

representativeSchreierRelators

L1061 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSchreierRelators
Documentation

The representative Schreier relators are the rewrites of the original relators over the chosen representative transversal.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeSchreierRelators
    (R : Set (FreeGroup X)) :
    Set (FreeGroup (RepresentativeSchreierSymbol S))
def

representativeDegenerateSchreierRelators

L1071 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeDegenerateSchreierRelators
Documentation

The representative degenerate Schreier relators are the section relators forced by the representative transversal.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeDegenerateSchreierRelators :
    Set (FreeGroup (RepresentativeSchreierSymbol S))
def

representativePresentationRelators

L1082 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativePresentationRelators
Documentation

The representative presentation relators are the rewritten original relators together with degenerate Schreier-generator relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativePresentationRelators
    (R : Set (FreeGroup X)) :
    Set (FreeGroup (RepresentativeSchreierSymbol S))
def

representativeSectionRelators

L1093 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSectionRelators
Documentation

These extra relators kill the rewrites of the chosen representatives. They are redundant for prefix-closed Schreier systems, but are needed for an arbitrary normalized representative function.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeSectionRelators :
    Set (FreeGroup (RepresentativeSchreierSymbol S))
def

representativeAugmentedPresentationRelators

L1102 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeAugmentedPresentationRelators
Documentation

The augmented representative presentation relators consist of the representative presentation relators together with the section relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeAugmentedPresentationRelators
    (R : Set (FreeGroup X)) :
    Set (FreeGroup (RepresentativeSchreierSymbol S))
def

representativePrefixClosedAlongList

L1112 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativePrefixClosedAlongList
Documentation

Prefix-closedness along a concrete representative word. Positive letters say the next prefix is itself a representative; negative letters say the current prefix is obtained from the previous representative by appending the positive letter.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · full declaration
def representativePrefixClosedAlongList (S : RightSchreierRepresentative L) :
    FreeGroup X → List (X × Bool) → Prop
  | _p, [] => True
  | p, (x, true) :: xs =>
      S.representative (S.representative p * FreeGroup.of x) =
        S.representative p * FreeGroup.of x ∧
      representativePrefixClosedAlongList S (p * FreeGroup.of x) xs
  | p, (x, false) :: xs =>
      S.representative p =
        S.representative (p * (FreeGroup.of x)⁻¹) * FreeGroup.of x ∧
      representativePrefixClosedAlongList S (p * (FreeGroup.of x)⁻¹) xs
def

IsPrefixClosedRepresentativeSystem

L1125 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.IsPrefixClosedRepresentativeSystem
Documentation

The representative system is prefix closed on its own representative words.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def IsPrefixClosedRepresentativeSystem : Prop
theorem

representativeTau_mem_schreierRelators

L1133 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_mem_schreierRelators
Documentation

The representative \(\tau\)-rewrite of an original relator belongs to the representative Schreier relator set.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_mem_schreierRelators
    {R : Set (FreeGroup X)}
    (t : representativeSet S) {r : FreeGroup X} (hr : r ∈ R) :
    representativeTau S (t : FreeGroup X) r ∈
      representativeSchreierRelators S R
theorem

representativeTau_mem_sectionRelators

L1144 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_mem_sectionRelators
Documentation

The representative \(\tau\)-rewrite of a quotient-section word belongs to the representative section-relator set.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_mem_sectionRelators
    (t : representativeSet S) :
    representativeTau S 1 (t : FreeGroup X) ∈
      representativeSectionRelators S
theorem

representativePresentationRelators_subset_augmented

L1153 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativePresentationRelators_subset_augmented
Documentation

Every representative presentation relator is an augmented representative presentation relator.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativePresentationRelators_subset_augmented
    (R : Set (FreeGroup X)) :
    representativePresentationRelators S R ⊆
      representativeAugmentedPresentationRelators S R
theorem

representativeSectionRelators_subset_augmented

L1163 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSectionRelators_subset_augmented
Documentation

Every representative section relator is included among the augmented representative presentation relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSectionRelators_subset_augmented
    (R : Set (FreeGroup X)) :
    representativeSectionRelators S ⊆
      representativeAugmentedPresentationRelators S R
theorem

representativeTauList_mem_normalClosure_degenerate_of_prefixClosedAlongList

L1174 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauList_mem_normalClosure_degenerate_of_prefixClosedAlongList
Documentation

A list following the prefix-closed representative system rewrites into the normal closure of the degenerate representative Schreier relators.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeTauList_mem_normalClosure_degenerate_of_prefixClosedAlongList
    {p : FreeGroup X} {xs : List (X × Bool)}
    (hprefix : representativePrefixClosedAlongList S p xs) :
    representativeTauList S p xs ∈
      Subgroup.normalClosure (representativeDegenerateSchreierRelators S)
theorem

representativeTau_section_mem_normalClosure_degenerate_of_isPrefixClosed

L1213 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_section_mem_normalClosure_degenerate_of_isPrefixClosed
Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier normal closure.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_section_mem_normalClosure_degenerate_of_isPrefixClosed
    (hprefix : IsPrefixClosedRepresentativeSystem S)
    (t : representativeSet S) :
    representativeTau S 1 (t : FreeGroup X) ∈
      Subgroup.normalClosure (representativeDegenerateSchreierRelators S)
theorem

representativeTau_section_mem_normalClosure_presentation_of_isPrefixClosed

L1226 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_section_mem_normalClosure_presentation_of_isPrefixClosed
Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier normal closure.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_section_mem_normalClosure_presentation_of_isPrefixClosed
    (R : Set (FreeGroup X))
    (hprefix : IsPrefixClosedRepresentativeSystem S)
    (t : representativeSet S) :
    representativeTau S 1 (t : FreeGroup X) ∈
      Subgroup.normalClosure (representativePresentationRelators S R)
theorem

representativeSymbolEvalHom_tau_relator_mem_normalClosure

L1241 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalHom_tau_relator_mem_normalClosure
Documentation

Evaluating the representative \(\tau\)-rewrite of an original relator gives an element of the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSymbolEvalHom_tau_relator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (t : representativeSet S) {r : FreeGroup X} (hr : r ∈ R) :
    representativeSymbolEvalHom S
        (representativeTau S (t : FreeGroup X) r) ∈
      Subgroup.normalClosure R
theorem

representativeEval_schreierRelator_mem_normalClosure

L1264 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeEval_schreierRelator_mem_normalClosure
Documentation

Evaluating a representative Schreier relator gives an element of the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeEval_schreierRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈ representativeSchreierRelators S R) :
    representativeSymbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

representativeDegenerateRelator_eval_eq_one

L1276 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeDegenerateRelator_eval_eq_one
Documentation

The evaluation of a representative degenerate Schreier relator 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeDegenerateRelator_eval_eq_one
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈ representativeDegenerateSchreierRelators S) :
    representativeSymbolEvalHom S q = 1
theorem

representativeEval_degenerateRelator_mem_normalClosure

L1291 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeEval_degenerateRelator_mem_normalClosure
Documentation

The indicated evaluated relator belongs to the normal closure supplied by the Reidemeister--Schreier relator comparison.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem representativeEval_degenerateRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈ representativeDegenerateSchreierRelators S) :
    representativeSymbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

representativeSectionRelator_eval_eq_one

L1299 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSectionRelator_eval_eq_one
Documentation

The evaluation of a representative section relator is 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 : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSectionRelator_eval_eq_one
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈ representativeSectionRelators S) :
    representativeSymbolEvalHom S q = 1
theorem

representativeEval_sectionRelator_mem_normalClosure

L1314 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeEval_sectionRelator_mem_normalClosure
Documentation

The indicated evaluated relator belongs to the normal closure supplied by the Reidemeister--Schreier relator comparison.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeEval_sectionRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈ representativeSectionRelators S) :
    representativeSymbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

representativeEval_presentationRelator_mem_normalClosure

L1325 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeEval_presentationRelator_mem_normalClosure
Documentation

Evaluating a representative presentation relator gives an element of the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeEval_presentationRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈ representativePresentationRelators S R) :
    representativeSymbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

representativeEval_augmentedRelator_mem_normalClosure

L1339 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeEval_augmentedRelator_mem_normalClosure
Documentation

The indicated evaluated relator belongs to the normal closure supplied by the Reidemeister--Schreier relator comparison.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeEval_augmentedRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈ representativeAugmentedPresentationRelators S R) :
    representativeSymbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

representativeEval_mem_normalClosure_of_mem_normalClosure_augmentedRelators

L1353 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeEval_mem_normalClosure_of_mem_normalClosure_augmentedRelators
Documentation

Evaluation sends the normal closure of the augmented representative presentation relators into the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeEval_mem_normalClosure_of_mem_normalClosure_augmentedRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈
      Subgroup.normalClosure (representativeAugmentedPresentationRelators S R)) :
    representativeSymbolEvalHom S q ∈ Subgroup.normalClosure R
theorem

representativeSymbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_augmented

L1368 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_augmented
Documentation

The subgroup-valued evaluation map sends the normal closure of the augmented representative presentation relators into the relator subgroup.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSymbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_augmented
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {q : FreeGroup (RepresentativeSchreierSymbol S)}
    (hq : q ∈
      Subgroup.normalClosure (representativeAugmentedPresentationRelators S R)) :
    representativeSymbolEvalSubgroupHom S q ∈ relatorSubgroup (L := L) R
def

representativeSymbolEvalAugmentedPresentationQuotientHom

L1383 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalAugmentedPresentationQuotientHom
Documentation

The evaluation map from the representative augmented presentation quotient to the relator-subgroup quotient of the subgroup.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeSymbolEvalAugmentedPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    FreeGroup (RepresentativeSchreierSymbol S) ⧸
        Subgroup.normalClosure (representativeAugmentedPresentationRelators S R) →*
      L ⧸ relatorSubgroup (L := L) R
theorem

representativeTau_conjugate_relator_mem_normalClosure_schreierRelators

L1406 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_conjugate_relator_mem_normalClosure_schreierRelators
Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier normal closure.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_conjugate_relator_mem_normalClosure_schreierRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (g : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    representativeTau S 1 (g * r * g⁻¹) ∈
      Subgroup.normalClosure (representativeSchreierRelators S R)
theorem

representativeTau_conjugate_relator_mem_normalClosure_presentationRelators

L1479 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_conjugate_relator_mem_normalClosure_presentationRelators
Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier normal closure.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_conjugate_relator_mem_normalClosure_presentationRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (g : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    representativeTau S 1 (g * r * g⁻¹) ∈
      Subgroup.normalClosure (representativePresentationRelators S R)
theorem

representativeTau_conjugate_relator_mem_normalClosure_augmentedRelators

L1494 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_conjugate_relator_mem_normalClosure_augmentedRelators
Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier normal closure.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_conjugate_relator_mem_normalClosure_augmentedRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (g : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    representativeTau S 1 (g * r * g⁻¹) ∈
      Subgroup.normalClosure (representativeAugmentedPresentationRelators S R)
def

representativeTauKernelAugmentedPresentationQuotientHom

L1509 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauKernelAugmentedPresentationQuotientHom
Documentation

The representative \(\tau\)-homomorphism from the kernel to the augmented presentation quotient is defined by Reidemeister--Schreier rewriting.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · full declaration
def representativeTauKernelAugmentedPresentationQuotientHom
    (R : Set (FreeGroup X)) :
    L →* FreeGroup (RepresentativeSchreierSymbol S) ⧸
      Subgroup.normalClosure (representativeAugmentedPresentationRelators S R) where
  toFun k :=
    QuotientGroup.mk'
      (Subgroup.normalClosure (representativeAugmentedPresentationRelators S R))
      (representativeTau S 1 (k : FreeGroup X))
  map_one' := by
    simp only [OneMemClass.coe_one, representativeTau_one, QuotientGroup.mk'_apply,
        QuotientGroup.mk_one]
  map_mul' k l := by
    change
      QuotientGroup.mk'
          (Subgroup.normalClosure (representativeAugmentedPresentationRelators S R))
          (representativeTau S 1 ((k : FreeGroup X) * (l : FreeGroup X))) =
        QuotientGroup.mk'
          (Subgroup.normalClosure (representativeAugmentedPresentationRelators S R))
          (representativeTau S 1 (k : FreeGroup X)) *
        QuotientGroup.mk'
          (Subgroup.normalClosure (representativeAugmentedPresentationRelators S R))
          (representativeTau S 1 (l : FreeGroup X))
    rw [representativeTau_mul_of_mem (S := S) k.property]
    rfl
theorem

representativeTauKernelAugmentedPresentationQuotientHom_eq_one_of_mem_normalClosure

L1538 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauKernelAugmentedPresentationQuotientHom_eq_one_of_mem_normalClosure
Documentation

The representative \(\tau\)-homomorphism to the augmented-presentation quotient kills every element of the normal closure of the original relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTauKernelAugmentedPresentationQuotientHom_eq_one_of_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    {n : FreeGroup X} (hn : n ∈ Subgroup.normalClosure R) :
    representativeTauKernelAugmentedPresentationQuotientHom (S := S) R
      ⟨n, hR hn⟩ = 1
def

representativeTauRelatorSubgroupAugmentedPresentationQuotientHom

L1602 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauRelatorSubgroupAugmentedPresentationQuotientHom
Documentation

The quotient homomorphism induced by \(\tau\)-rewriting maps the relator subgroup quotient to the augmented Schreier-presentation quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeTauRelatorSubgroupAugmentedPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    L ⧸ relatorSubgroup (L := L) R →*
      FreeGroup (RepresentativeSchreierSymbol S) ⧸
        Subgroup.normalClosure (representativeAugmentedPresentationRelators S R)
theorem

representativeSectionRelator_relatorEquivalent_one

L1625 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSectionRelator_relatorEquivalent_one
Documentation

A representative section relator is relator-equivalent to the identity modulo the augmented presentation relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSectionRelator_relatorEquivalent_one
    (R : Set (FreeGroup X)) (t : representativeSet S) :
    RelatorEquivalent (representativeAugmentedPresentationRelators S R)
      (representativeTau S 1 (t : FreeGroup X)) 1
theorem

representativeTau_symbolEval_relatorEquivalent_augmented

L1637 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_symbolEval_relatorEquivalent_augmented
Documentation

The \(\tau\)-word and its symbol evaluation are relator-equivalent modulo the augmented presentation relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_symbolEval_relatorEquivalent_augmented
    (R : Set (FreeGroup X)) (z : RepresentativeSchreierSymbol S) :
    RelatorEquivalent (representativeAugmentedPresentationRelators S R)
      (representativeTau S 1 (representativeSymbolEval S z))
      (FreeGroup.of z)
theorem

representativeTau_symbolEvalHom_relatorEquivalent_augmented

L1745 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTau_symbolEvalHom_relatorEquivalent_augmented
Documentation

The \(\tau\)-word and its symbol evaluation are relator-equivalent modulo the augmented presentation relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTau_symbolEvalHom_relatorEquivalent_augmented
    (R : Set (FreeGroup X))
    (z : FreeGroup (RepresentativeSchreierSymbol S)) :
    RelatorEquivalent (representativeAugmentedPresentationRelators S R)
      (representativeTau S 1 (representativeSymbolEvalHom S z)) z
theorem

representativeSymbolEvalAugmentedPresentationQuotientHom_tauKernel

L1779 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalAugmentedPresentationQuotientHom_tauKernel
Documentation

The \(\tau\)-map sends kernel elements into the augmented Schreier presentation quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSymbolEvalAugmentedPresentationQuotientHom_tauKernel
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (k : L) :
    representativeSymbolEvalAugmentedPresentationQuotientHom (S := S) hR
        (representativeTauKernelAugmentedPresentationQuotientHom (S := S) R k) =
      QuotientGroup.mk' (relatorSubgroup (L := L) R) k
theorem

representativeSymbolEvalAugmentedPresentationQuotientHom_tauRelatorSubgroup

L1803 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeSymbolEvalAugmentedPresentationQuotientHom_tauRelatorSubgroup
Documentation

The \(\tau\)-map descends from the relator-subgroup quotient to the augmented Schreier presentation quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeSymbolEvalAugmentedPresentationQuotientHom_tauRelatorSubgroup
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (y : L ⧸ relatorSubgroup (L := L) R) :
    representativeSymbolEvalAugmentedPresentationQuotientHom (S := S) hR
        (representativeTauRelatorSubgroupAugmentedPresentationQuotientHom
          (S := S) hR y) = y
theorem

representativeTauRelatorSubgroupAugmentedPresentationQuotientHom_symbolEval

L1820 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeTauRelatorSubgroupAugmentedPresentationQuotientHom_symbolEval
Documentation

\(\tau\)-rewriting followed by symbol evaluation is the identity on the augmented Schreier-presentation quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem representativeTauRelatorSubgroupAugmentedPresentationQuotientHom_symbolEval
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (y : FreeGroup (RepresentativeSchreierSymbol S) ⧸
        Subgroup.normalClosure (representativeAugmentedPresentationRelators S R)) :
    representativeTauRelatorSubgroupAugmentedPresentationQuotientHom
        (S := S) hR
        (representativeSymbolEvalAugmentedPresentationQuotientHom
          (S := S) hR y) = y
def

representativeAugmentedPresentationQuotientEquiv

L1849 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeAugmentedPresentationQuotientEquiv
Documentation

The augmented representative presentation quotient is equivalent to the relator quotient of the subgroup.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · full declaration
def representativeAugmentedPresentationQuotientEquiv
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    FreeGroup (RepresentativeSchreierSymbol S) ⧸
        Subgroup.normalClosure (representativeAugmentedPresentationRelators S R) ≃*
      L ⧸ relatorSubgroup (L := L) R where
  toFun := representativeSymbolEvalAugmentedPresentationQuotientHom (S := S) hR
  invFun :=
    representativeTauRelatorSubgroupAugmentedPresentationQuotientHom
      (S := S) hR
  left_inv :=
    representativeTauRelatorSubgroupAugmentedPresentationQuotientHom_symbolEval
      (S := S) hR
  right_inv :=
    representativeSymbolEvalAugmentedPresentationQuotientHom_tauRelatorSubgroup
      (S := S) hR
  map_mul' x y :=
    (representativeSymbolEvalAugmentedPresentationQuotientHom
      (S := S) hR).map_mul x y
def

representativeAugmentedPresentedGroupEquiv

L1873 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativeAugmentedPresentedGroupEquiv
Documentation

The presented group for the augmented representative presentation is equivalent to the relator quotient of the subgroup.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativeAugmentedPresentedGroupEquiv
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L) :
    PresentedGroup (representativeAugmentedPresentationRelators S R) ≃*
      L ⧸ relatorSubgroup (L := L) R
theorem

normalClosure_representativeAugmentedPresentationRelators_eq

L1884 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.normalClosure_representativeAugmentedPresentationRelators_eq
Documentation

The augmented-presentation relator normal closure equals the normal closure generated by the corresponding Reidemeister--Schreier relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem normalClosure_representativeAugmentedPresentationRelators_eq
    {R : Set (FreeGroup X)}
    (hsection :
      ∀ t : representativeSet S,
        representativeTau S 1 (t : FreeGroup X) ∈
          Subgroup.normalClosure (representativePresentationRelators S R)) :
    Subgroup.normalClosure (representativeAugmentedPresentationRelators S R) =
      Subgroup.normalClosure (representativePresentationRelators S R)
theorem

normalClosure_representativeAugmentedPresentationRelators_eq_of_isPrefixClosed

L1905 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.normalClosure_representativeAugmentedPresentationRelators_eq_of_isPrefixClosed
Documentation

The augmented-presentation relator normal closure equals the normal closure generated by the corresponding Reidemeister--Schreier relators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
theorem normalClosure_representativeAugmentedPresentationRelators_eq_of_isPrefixClosed
    {R : Set (FreeGroup X)}
    (hprefix : IsPrefixClosedRepresentativeSystem S) :
    Subgroup.normalClosure (representativeAugmentedPresentationRelators S R) =
      Subgroup.normalClosure (representativePresentationRelators S R)
def

representativePresentationQuotientEquivOfSectionRelators

L1920 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativePresentationQuotientEquivOfSectionRelators
Documentation

After adding the section relators, the representative presentation quotient is equivalent to the subgroup relator quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativePresentationQuotientEquivOfSectionRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (hsection :
      ∀ t : representativeSet S,
        representativeTau S 1 (t : FreeGroup X) ∈
          Subgroup.normalClosure (representativePresentationRelators S R)) :
    FreeGroup (RepresentativeSchreierSymbol S) ⧸
        Subgroup.normalClosure (representativePresentationRelators S R) ≃*
      L ⧸ relatorSubgroup (L := L) R
def

representativePresentedGroupEquivOfSectionRelators

L1944 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativePresentedGroupEquivOfSectionRelators
Documentation

After adding the section relators, the representative presented group is equivalent to the subgroup quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativePresentedGroupEquivOfSectionRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (hsection :
      ∀ t : representativeSet S,
        representativeTau S 1 (t : FreeGroup X) ∈
          Subgroup.normalClosure (representativePresentationRelators S R)) :
    PresentedGroup (representativePresentationRelators S R) ≃*
      L ⧸ relatorSubgroup (L := L) R
def

representativePresentationQuotientEquivOfIsPrefixClosed

L1960 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativePresentationQuotientEquivOfIsPrefixClosed
Documentation

For a prefix-closed representative set, the representative presentation quotient is equivalent to the subgroup relator quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativePresentationQuotientEquivOfIsPrefixClosed
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (hprefix : IsPrefixClosedRepresentativeSystem S) :
    FreeGroup (RepresentativeSchreierSymbol S) ⧸
        Subgroup.normalClosure (representativePresentationRelators S R) ≃*
      L ⧸ relatorSubgroup (L := L) R
def

representativePresentedGroupEquivOfIsPrefixClosed

L1977 ↗
ReidemeisterSchreier.Discrete.SchreierRewriting.representativePresentedGroupEquivOfIsPrefixClosed
Documentation

For a prefix-closed representative set, the representative presented group is equivalent to the subgroup quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X : Type*}
namespace SchreierRewriting
variable {L : Subgroup (FreeGroup X)} (S : RightSchreierRepresentative L)
variable [DecidableEq X]
Lean source · statement
def representativePresentedGroupEquivOfIsPrefixClosed
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ L)
    (hprefix : IsPrefixClosedRepresentativeSystem S) :
    PresentedGroup (representativePresentationRelators S R) ≃*
      L ⧸ relatorSubgroup (L := L) R

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