NYLL
Module

Core.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.Core
35 declarations indexed from sourceView source ↗

Module documentation

Reidemeister--Schreier target-presentation core

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Target Presentation / Core.

This module defines the structured certificates for prefix-closed quotient-section words and the core data specifying a cleaned Reidemeister--Schreier target presentation.

Imports1
Imported by2

Declarations

structure

PrefixClosedFiniteQuotientSchreierData

L32 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData
Documentation

Finite quotient Schreier data whose section is prefix closed on its representative words. This is the convenient application-facing input for the raw finite Reidemeister--Schreier presentation theorem.

Source context 3 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
Lean source · full declaration
structure PrefixClosedFiniteQuotientSchreierData
    (X Q : Type*) [Group Q] [Fintype Q] [DecidableEq X] where
  /-- The underlying finite quotient and normalized section. -/
  toFiniteQuotientSchreierData : FiniteQuotientSchreierData X Q
  /-- The chosen quotient-section words are closed under taking prefixes. -/
  isPrefixClosed :
    toFiniteQuotientSchreierData.IsPrefixClosedQuotientSection
structure

QuotientSectionWordCertificate

L41 ↗
ReidemeisterSchreier.Discrete.QuotientSectionWordCertificate
Documentation

Common word-level data for a finite quotient section.

Source context 3 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
Lean source · full declaration
structure QuotientSectionWordCertificate
    (X Q : Type*) [Group Q] [Fintype Q] where
  /-- The homomorphism from the free group to the finite quotient. -/
  quotientMap : FreeGroup X →* Q
  /-- The chosen word representing each finite quotient element. -/
  quotientSectionWord : Q → List (X × Bool)
  /-- Evaluating a chosen word and applying the quotient map recovers its quotient element. -/
  quotientMap_mk_quotientSectionWord :
    ∀ q : Q, quotientMap (FreeGroup.mk (quotientSectionWord q)) = q
structure

PrefixClosedQuotientSectionWordCertificate

L55 ↗
ReidemeisterSchreier.Discrete.PrefixClosedQuotientSectionWordCertificate
Documentation

A reusable word-level certificate for a prefix-closed finite quotient section, including the required reduced-word and prefix-closedness conditions.

Source context 3 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
Lean source · full declaration
structure PrefixClosedQuotientSectionWordCertificate
    (X Q : Type*) [Group Q] [Fintype Q] [DecidableEq X]
    extends QuotientSectionWordCertificate X Q where
  /-- The identity quotient element is represented by the empty word. -/
  quotientSectionWord_one : quotientSectionWord 1 = []
  /-- Every chosen quotient-section word is reduced. -/
  quotientSectionWord_reduced :
    ∀ q : Q, FreeGroup.reduce (quotientSectionWord q) = quotientSectionWord q
  /-- Every prefix of a chosen quotient-section word is the chosen word for its quotient state. -/
  prefixClosed_quotientSectionWord :
    ∀ q : Q,
      (FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
        quotientSectionWord quotientMap_mk_quotientSectionWord
        quotientSectionWord_one).prefixClosedQuotientSectionWordAlongList
          quotientSectionWord 1 (quotientSectionWord q)
def

toFiniteQuotientSchreierData

L77 ↗
ReidemeisterSchreier.Discrete.PrefixClosedQuotientSectionWordCertificate.toFiniteQuotientSchreierData
Documentation

The certificate data forgets to the underlying finite quotient Schreier data.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedQuotientSectionWordCertificate
variable [DecidableEq X]
variable (C : PrefixClosedQuotientSectionWordCertificate X Q)
Lean source · statement
def toFiniteQuotientSchreierData :
    FiniteQuotientSchreierData X Q
def

toPrefixClosedFiniteQuotientSchreierData

L84 ↗
ReidemeisterSchreier.Discrete.PrefixClosedQuotientSectionWordCertificate.toPrefixClosedFiniteQuotientSchreierData
Documentation

The certificate data determines prefix-closed finite quotient Schreier data.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedQuotientSectionWordCertificate
variable [DecidableEq X]
variable (C : PrefixClosedQuotientSectionWordCertificate X Q)
Lean source · full declaration
def toPrefixClosedFiniteQuotientSchreierData :
    PrefixClosedFiniteQuotientSchreierData X Q where
  toFiniteQuotientSchreierData := C.toFiniteQuotientSchreierData
  isPrefixClosed :=
    FiniteQuotientSchreierData.isPrefixClosedQuotientSection_of_prefixClosedQuotientSectionWord
      C.toFiniteQuotientSchreierData
      (by intro q; rfl)
      C.quotientSectionWord_reduced
      (by
        intro q
        exact C.prefixClosed_quotientSectionWord q)
structure

PositivePrefixClosedQuotientSectionWordCertificate

L103 ↗
ReidemeisterSchreier.Discrete.PositivePrefixClosedQuotientSectionWordCertificate
Documentation

A certificate for a positive prefix-closed quotient-section tree. Each quotient element has a positive word in the original generators, and every prefix is the chosen word for the quotient element it represents.

Source context 3 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
Lean source · full declaration
structure PositivePrefixClosedQuotientSectionWordCertificate
    (X Q : Type*) [Group Q] [Fintype Q]
    extends QuotientSectionWordCertificate X Q where
  /-- Every letter in every chosen quotient-section word has positive orientation. -/
  quotientSectionWord_positive :
    ∀ q : Q, ∀ xb ∈ quotientSectionWord q, xb.2 = true
  /-- Each prefix is the chosen word for the quotient element obtained by evaluating that prefix. -/
  prefixState :
    ∀ q : Q, ∀ acc rest : List (X × Bool),
      acc ++ rest = quotientSectionWord q →
        quotientSectionWord (quotientMap (FreeGroup.mk acc)) = acc
theorem

quotientSectionWord_one

L120 ↗
ReidemeisterSchreier.Discrete.PositivePrefixClosedQuotientSectionWordCertificate.quotientSectionWord_one
Documentation

The quotient-section word certificate sends the identity quotient element to the empty word.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PositivePrefixClosedQuotientSectionWordCertificate
variable (C : PositivePrefixClosedQuotientSectionWordCertificate X Q)
Lean source · statement
theorem quotientSectionWord_one :
    C.quotientSectionWord 1 = []
theorem

quotientSectionWord_reduced

L126 ↗
ReidemeisterSchreier.Discrete.PositivePrefixClosedQuotientSectionWordCertificate.quotientSectionWord_reduced
Documentation

Every quotient-section word in the positive prefix-closed certificate is reduced.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PositivePrefixClosedQuotientSectionWordCertificate
variable (C : PositivePrefixClosedQuotientSectionWordCertificate X Q)
Lean source · statement
theorem quotientSectionWord_reduced [DecidableEq X] (q : Q) :
    FreeGroup.reduce (C.quotientSectionWord q) = C.quotientSectionWord q
def

toFiniteQuotientSchreierData

L132 ↗
ReidemeisterSchreier.Discrete.PositivePrefixClosedQuotientSectionWordCertificate.toFiniteQuotientSchreierData
Documentation

The certificate data forgets to the underlying finite quotient Schreier data.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PositivePrefixClosedQuotientSectionWordCertificate
variable (C : PositivePrefixClosedQuotientSectionWordCertificate X Q)
Lean source · statement
def toFiniteQuotientSchreierData :
    FiniteQuotientSchreierData X Q
def

toPrefixClosedFiniteQuotientSchreierData

L140 ↗
ReidemeisterSchreier.Discrete.PositivePrefixClosedQuotientSectionWordCertificate.toPrefixClosedFiniteQuotientSchreierData
Documentation

The certificate data determines prefix-closed finite quotient Schreier data.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PositivePrefixClosedQuotientSectionWordCertificate
variable (C : PositivePrefixClosedQuotientSectionWordCertificate X Q)
Lean source · full declaration
def toPrefixClosedFiniteQuotientSchreierData [DecidableEq X] :
    PrefixClosedFiniteQuotientSchreierData X Q where
  toFiniteQuotientSchreierData := C.toFiniteQuotientSchreierData
  isPrefixClosed := by
    apply
      FiniteQuotientSchreierData.isPrefixClosedQuotientSection_of_prefixClosedQuotientSectionWord
        (D := C.toFiniteQuotientSchreierData)
    · intro q
      rfl
    · intro q
      exact C.quotientSectionWord_reduced q
    · intro q
      exact
        FiniteQuotientSchreierData.prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates
          (D := C.toFiniteQuotientSchreierData)
          (by intro q; rfl)
          C.quotientSectionWord_positive
          (by
            intro target acc rest hcat
            simpa [toFiniteQuotientSchreierData,
              FiniteQuotientSchreierData.ofQuotientSectionWords] using
              C.prefixState target acc rest hcat)
          q
def

ofQuotientSectionWords

L174 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.ofQuotientSectionWords
Documentation

Finite quotient Schreier data can be built from quotient-section words whose evaluations are the prescribed quotient sections.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
Lean source · full declaration
def ofQuotientSectionWords
    (quotientMap : FreeGroup X →* Q)
    (quotientSectionWord : Q → List (X × Bool))
    (quotientMap_mk_quotientSectionWord :
      ∀ q : Q, quotientMap (FreeGroup.mk (quotientSectionWord q)) = q)
    (quotientSectionWord_one : quotientSectionWord 1 = [])
    (quotientSectionWord_reduced :
      ∀ q : Q, FreeGroup.reduce (quotientSectionWord q) = quotientSectionWord q)
    (prefixClosed_quotientSectionWord :
      ∀ q : Q,
        (FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
          quotientSectionWord quotientMap_mk_quotientSectionWord
          quotientSectionWord_one).prefixClosedAlongList 1
            (quotientSectionWord q)) :
    PrefixClosedFiniteQuotientSchreierData X Q where
  toFiniteQuotientSchreierData :=
    FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
      quotientSectionWord quotientMap_mk_quotientSectionWord
      quotientSectionWord_one
  isPrefixClosed := by
    intro q
    simpa [FiniteQuotientSchreierData.ofQuotientSectionWords,
      FreeGroup.toWord_mk, quotientSectionWord_reduced q] using
      prefixClosed_quotientSectionWord q
def

ofPrefixClosedQuotientSectionWords

L203 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.ofPrefixClosedQuotientSectionWords
Documentation

Build prefix-closed finite-quotient Schreier data from reduced quotient-section words and their prefix-closedness certificate.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
Lean source · full declaration
def ofPrefixClosedQuotientSectionWords
    (quotientMap : FreeGroup X →* Q)
    (quotientSectionWord : Q → List (X × Bool))
    (quotientMap_mk_quotientSectionWord :
      ∀ q : Q, quotientMap (FreeGroup.mk (quotientSectionWord q)) = q)
    (quotientSectionWord_one : quotientSectionWord 1 = [])
    (quotientSectionWord_reduced :
      ∀ q : Q, FreeGroup.reduce (quotientSectionWord q) = quotientSectionWord q)
    (prefixClosed_quotientSectionWord :
      ∀ q : Q,
        FiniteQuotientSchreierData.prefixClosedQuotientSectionWordAlongList
          (FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
            quotientSectionWord quotientMap_mk_quotientSectionWord
            quotientSectionWord_one)
          quotientSectionWord 1 (quotientSectionWord q)) :
    PrefixClosedFiniteQuotientSchreierData X Q where
  toFiniteQuotientSchreierData :=
    FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
      quotientSectionWord quotientMap_mk_quotientSectionWord
      quotientSectionWord_one
  isPrefixClosed :=
    FiniteQuotientSchreierData.isPrefixClosedQuotientSection_of_prefixClosedQuotientSectionWord
      (FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
        quotientSectionWord quotientMap_mk_quotientSectionWord
        quotientSectionWord_one)
      (by intro q; rfl)
      quotientSectionWord_reduced
      prefixClosed_quotientSectionWord
theorem

ofQuotientSectionWords_toFiniteQuotientSchreierData

L237 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.ofQuotientSectionWords_toFiniteQuotientSchreierData
Documentation

Forgetting the prefix-closed structure from ofQuotientSectionWords recovers the underlying finite-quotient Schreier data built from the same section words.

Source context 5 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
Lean source · statement
theorem ofQuotientSectionWords_toFiniteQuotientSchreierData
    (quotientMap : FreeGroup X →* Q)
    (quotientSectionWord : Q → List (X × Bool))
    (quotientMap_mk_quotientSectionWord :
      ∀ q : Q, quotientMap (FreeGroup.mk (quotientSectionWord q)) = q)
    (quotientSectionWord_one : quotientSectionWord 1 = [])
    (quotientSectionWord_reduced :
      ∀ q : Q, FreeGroup.reduce (quotientSectionWord q) = quotientSectionWord q)
    (prefixClosed_quotientSectionWord :
      ∀ q : Q,
        (FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
          quotientSectionWord quotientMap_mk_quotientSectionWord
          quotientSectionWord_one).prefixClosedAlongList 1
            (quotientSectionWord q)) :
    (ofQuotientSectionWords quotientMap quotientSectionWord
      quotientMap_mk_quotientSectionWord quotientSectionWord_one
      quotientSectionWord_reduced prefixClosed_quotientSectionWord).toFiniteQuotientSchreierData =
      FiniteQuotientSchreierData.ofQuotientSectionWords quotientMap
        quotientSectionWord quotientMap_mk_quotientSectionWord
        quotientSectionWord_one
instance

instCoePrefixClosedFiniteQuotientSchreierData

L263 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.instCoePrefixClosedFiniteQuotientSchreierData
Documentation

Prefix-closed finite-quotient Schreier data coerces to its underlying finite-quotient Schreier data.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · full declaration
instance instCoePrefixClosedFiniteQuotientSchreierData :
    Coe (PrefixClosedFiniteQuotientSchreierData X Q)
    (FiniteQuotientSchreierData X Q) where
  coe D := D.toFiniteQuotientSchreierData
abbrev

kernel

L269 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.kernel
Documentation

The kernel of the finite quotient map is the subgroup used in the finite Schreier data.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev kernel : Subgroup (FreeGroup X)
abbrev

presentationRelators

L276 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.presentationRelators
Documentation

For a prefix-closed finite quotient section, the presentation relators are those of the underlying finite-quotient Schreier data.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev presentationRelators (R : Set (FreeGroup X)) :
    Set (FreeGroup (FiniteQuotientSchreierData.FiniteSchreierSymbol X Q))
abbrev

relatorSubgroup

L281 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.relatorSubgroup
Documentation

The relator subgroup is the normal subgroup generated by the target 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 Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev relatorSubgroup (R : Set (FreeGroup X)) :
    Subgroup D.kernel
def

presentationQuotientEquiv

L289 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.presentationQuotientEquiv
Documentation

The raw finite Reidemeister--Schreier presentation theorem for a prefix-closed finite quotient section.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def presentationQuotientEquiv
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    FreeGroup (FiniteQuotientSchreierData.FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (presentationRelators D R) ≃*
      D.kernel ⧸ relatorSubgroup D R
def

presentationPresentedGroupEquiv

L302 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.presentationPresentedGroupEquiv
Documentation

The prefix-closed finite quotient Schreier target presentation has presented group equivalent to the kernel quotient.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def presentationPresentedGroupEquiv
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    PresentedGroup (presentationRelators D R) ≃*
      D.kernel ⧸ relatorSubgroup D R
abbrev

nondegenerateSchreierSymbol

L310 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.nondegenerateSchreierSymbol
Documentation

The nondegenerate Schreier symbols attached to the underlying finite-quotient Schreier data.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev nondegenerateSchreierSymbol :
    Type _
abbrev

presentationRelatorsAfterDeletingDegenerateSchreierGenerators

L318 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.presentationRelatorsAfterDeletingDegenerateSchreierGenerators
Documentation

For a prefix-closed finite quotient section, these are the raw Reidemeister--Schreier relators after deleting 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 Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev presentationRelatorsAfterDeletingDegenerateSchreierGenerators
    (R : Set (FreeGroup X))
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol] :
    Set (FreeGroup D.nondegenerateSchreierSymbol)
def

deleteDegenerateSchreierGeneratorsScript

L328 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorsScript
Documentation

Deleting degenerate finite Schreier generators gives a Tietze equivalence with the cleaned presentation.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def deleteDegenerateSchreierGeneratorsScript
    (R : Set (FreeGroup X))
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol] :
    VerifiedTietzeScript
      (Presentation.ofRelators (presentationRelators D R))
      (Presentation.ofRelators
        (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R))
def

deleteDegenerateSchreierGenerators

L346 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.deleteDegenerateSchreierGenerators
Documentation

Deleting degenerate finite Schreier generators produces the cleaned presentation on nondegenerate Schreier symbols.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def deleteDegenerateSchreierGenerators
    (R : Set (FreeGroup X))
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol] :
    PresentedGroup (presentationRelators D R) ≃*
      PresentedGroup
        (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R)
def

presentationAfterDeletingDegenerateSchreierGeneratorsPresentedGroupEquiv

L358 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.presentationAfterDeletingDegenerateSchreierGeneratorsPresentedGroupEquiv
Documentation

Prefix-closed finite Reidemeister--Schreier theorem after deleting all 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 Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def presentationAfterDeletingDegenerateSchreierGeneratorsPresentedGroupEquiv
    {R : Set (FreeGroup X)}
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    PresentedGroup
        (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R) ≃*
      D.kernel ⧸ relatorSubgroup D R
abbrev

cleanedTau

L372 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.cleanedTau
Documentation

The cleaned \(\tau\)-map is the Reidemeister--Schreier rewriting map with degenerate generators removed.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev cleanedTau
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
    (q : Q) (w : FreeGroup X) :
    FreeGroup D.nondegenerateSchreierSymbol
abbrev

cleanedTauList

L382 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.cleanedTauList
Documentation

The cleaned \(\tau\)-list is the Reidemeister--Schreier \(\tau\)-list after deleting 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 Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev cleanedTauList
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
    (q : Q) (xs : List (X × Bool)) :
    FreeGroup D.nondegenerateSchreierSymbol
def

cleanedTauNormalWord

L391 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.cleanedTauNormalWord
Documentation

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

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def cleanedTauNormalWord
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
    [DecidableEq D.nondegenerateSchreierSymbol]
    (q : Q) (w : FreeGroup X) :
    List (D.nondegenerateSchreierSymbol × Bool)
def

cleanedTauListNormalWord

L402 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.cleanedTauListNormalWord
Documentation

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

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def cleanedTauListNormalWord
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
    [DecidableEq D.nondegenerateSchreierSymbol]
    (q : Q) (xs : List (X × Bool)) :
    List (D.nondegenerateSchreierSymbol × Bool)
abbrev

cleanedSchreierRelators

L413 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.cleanedSchreierRelators
Documentation

The cleaned Schreier relators are the cleaned \(\tau\)-rewrites of original relators over all finite quotient elements.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
abbrev cleanedSchreierRelators
    (R : Set (FreeGroup X))
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol] :
    Set (FreeGroup D.nondegenerateSchreierSymbol)
def

cleanedPresentationPresentedGroupEquiv

L423 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.cleanedPresentationPresentedGroupEquiv
Documentation

Prefix-closed finite Reidemeister--Schreier theorem stated directly with cleaned relators, i.e. after deleting 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 Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · statement
def cleanedPresentationPresentedGroupEquiv
    {R : Set (FreeGroup X)}
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    PresentedGroup (D.cleanedSchreierRelators R) ≃*
      D.kernel ⧸ relatorSubgroup D R
structure

CleanedReidemeisterSchreierTargetPresentationData

L448 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationData
Documentation

A certificate that the cleaned finite Reidemeister--Schreier presentation is Tietze equivalent to a chosen target presentation.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
Lean source · full declaration
structure CleanedReidemeisterSchreierTargetPresentationData
    (R : Set (FreeGroup X)) (Y : Type*)
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol] where
  /-- The relators of the chosen target presentation on generators \(Y\). -/
  targetRelators : Set (FreeGroup Y)
  /-- The word in target generators assigned to each nondegenerate Schreier generator. -/
  toTargetGenerator : D.nondegenerateSchreierSymbol → FreeGroup Y
  /-- The word in nondegenerate Schreier generators assigned to each target generator. -/
  fromTargetGenerator : Y → FreeGroup D.nondegenerateSchreierSymbol
  /-- Cleaned Reidemeister--Schreier relators map to consequences of the target relators. -/
  mapsCleanedRelators :
    ∀ q : Q, ∀ r ∈ R,
      RelatorEquivalent targetRelators
        (FreeGroup.lift toTargetGenerator (D.cleanedTau q r)) 1
  /-- Target relators map to consequences of the cleaned Reidemeister--Schreier relators. -/
  mapsTargetRelators :
    ∀ s ∈ targetRelators,
      RelatorEquivalent (D.cleanedSchreierRelators R)
        (FreeGroup.lift fromTargetGenerator s) 1
  /-- Mapping a nondegenerate Schreier generator forward and back recovers it modulo relators. -/
  from_toTargetGenerator :
    ∀ z : D.nondegenerateSchreierSymbol,
      RelatorEquivalent (D.cleanedSchreierRelators R)
        (FreeGroup.lift fromTargetGenerator (toTargetGenerator z))
        (FreeGroup.of z)
  /-- Mapping a target generator back and forward recovers it modulo target relators. -/
  to_fromTargetGenerator :
    ∀ y : Y,
      RelatorEquivalent targetRelators
        (FreeGroup.lift toTargetGenerator (fromTargetGenerator y))
        (FreeGroup.of y)
def

toTietzeEquiv

L487 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationData.toTietzeEquiv
Documentation

The cleaned Reidemeister--Schreier target presentation data yields a Tietze equivalence.

Source context 10 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
namespace CleanedReidemeisterSchreierTargetPresentationData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
Lean source · statement
def toTietzeEquiv
    (C : D.CleanedReidemeisterSchreierTargetPresentationData R Y) :
    TietzeEquiv (D.cleanedSchreierRelators R) C.targetRelators
def

presentedEquiv

L501 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationData.presentedEquiv
Documentation

The target presentation is equivalent to the cleaned Reidemeister--Schreier presentation.

Source context 10 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
namespace CleanedReidemeisterSchreierTargetPresentationData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
Lean source · statement
def presentedEquiv
    (C : D.CleanedReidemeisterSchreierTargetPresentationData R Y) :
    PresentedGroup (D.cleanedSchreierRelators R) ≃*
      PresentedGroup C.targetRelators
def

targetPresentedGroupEquivKernel

L511 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationData.targetPresentedGroupEquivKernel
Documentation

The target presented group is equivalent to the subgroup kernel described by the cleaned Reidemeister--Schreier presentation.

Source context 10 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
namespace CleanedReidemeisterSchreierTargetPresentationData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
Lean source · statement
def targetPresentedGroupEquivKernel
    (C : D.CleanedReidemeisterSchreierTargetPresentationData R Y)
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    PresentedGroup C.targetRelators ≃*
      D.kernel ⧸ relatorSubgroup D R
def

toPresentationEquivCertificate

L522 ↗
ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationData.toPresentationEquivCertificate
Documentation

The cleaned Reidemeister--Schreier target presentation data yields the corresponding Tietze script.

Source context 10 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)
namespace CleanedReidemeisterSchreierTargetPresentationData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
Lean source · statement
def toPresentationEquivCertificate
    (C : D.CleanedReidemeisterSchreierTargetPresentationData R Y) :
    PresentationEquivCertificate
      (Presentation.ofRelators (D.cleanedSchreierRelators R))
      (Presentation.ofRelators C.targetRelators)

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