NYLL
Module

CleanedSymbols.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedSymbols
23 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Cleaned Symbols

This module separates degenerate Schreier symbols from genuine generators and sets up the relator families needed to delete the trivial generators from the finite-quotient presentation.

Imports2
Imported by2

Declarations

def

IsDegenerateSchreierSymbol

L35 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.IsDegenerateSchreierSymbol
Documentation

Predicate saying that a finite Schreier symbol is degenerate and should be deleted from the cleaned presentation.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
def IsDegenerateSchreierSymbol (z : FiniteSchreierSymbol X Q) : Prop
def

degenerateSchreierRelators

L43 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.degenerateSchreierRelators
Documentation

The set of degenerate finite-quotient Schreier relators killed when deleting degenerate symbols.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
def degenerateSchreierRelators :
    Set (FreeGroup (FiniteSchreierSymbol X Q))
def

presentationRelators

L53 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelators
Documentation

The finite-quotient 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def presentationRelators (R : Set (FreeGroup X)) :
    Set (FreeGroup (FiniteSchreierSymbol X Q))
abbrev

NondegenerateSchreierSymbol

L59 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.NondegenerateSchreierSymbol
Documentation

The type of finite Schreier symbols kept after deleting degenerate symbols.

Source context 7 commands

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

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

DegenerateSchreierSymbol

L64 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.DegenerateSchreierSymbol
Documentation

The type of finite Schreier symbols marked for deletion as degenerate.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
abbrev DegenerateSchreierSymbol
theorem

trivialGeneratorRelatorsOfPredicate_isDegenerateSchreierSymbol

L72 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.trivialGeneratorRelatorsOfPredicate_isDegenerateSchreierSymbol
Documentation

The trivial-generator relators selected by the degeneracy predicate are exactly the degenerate 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem trivialGeneratorRelatorsOfPredicate_isDegenerateSchreierSymbol
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    Presented.trivialGeneratorRelatorsOfPredicate D.IsDegenerateSchreierSymbol =
      D.degenerateSchreierRelators
theorem

relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol

L103 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol
Documentation

Adding trivial-generator relators for degenerate Schreier symbols gives the 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 FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    Presented.relatorsWithTrivialGeneratorsOfPredicate
        (D.schreierRelators R) D.IsDegenerateSchreierSymbol =
      D.presentationRelators R
def

presentationRelatorsAfterDeletingDegenerateSchreierGenerators

L118 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelatorsAfterDeletingDegenerateSchreierGenerators
Documentation

The raw finite Reidemeister--Schreier relators after deleting the degenerate Schreier generators with relators \(s(q,x)=1\).

Source context 6 commands

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

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

deleteDegenerateSchreierGeneratorsScript

L129 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.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 FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def deleteDegenerateSchreierGeneratorsScript
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    VerifiedTietzeScript
      (Presentation.ofRelators (D.presentationRelators R))
      (Presentation.ofRelators
        (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R))
theorem

deleteDegenerateSchreierGeneratorsScript_trace

L148 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorsScript_trace
Documentation

The cleaned-symbol construction first identifies the proved-equal relator families and then performs one indexed generator-deletion move. This theorem makes the maintained concrete consumer visible to trace and cost clients.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem deleteDegenerateSchreierGeneratorsScript_trace
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    (D.deleteDegenerateSchreierGeneratorsScript R).trace =
      [ElementaryTietzeMove.Kind.replaceRelators,
        ElementaryTietzeMove.Kind.deleteTrivialGenerators]
theorem

deleteDegenerateSchreierGeneratorsScript_cost

L164 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorsScript_cost
Documentation

The deletion script's weighted cost is the cost of replacing relators plus the weighted cost of deleting each degenerate 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem deleteDegenerateSchreierGeneratorsScript_cost
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (weight : ElementaryTietzeMove.Kind → ℕ) :
    (D.deleteDegenerateSchreierGeneratorsScript R).cost weight =
      weight ElementaryTietzeMove.Kind.replaceRelators +
        weight ElementaryTietzeMove.Kind.deleteTrivialGenerators
def

deleteDegenerateSchreierGenerators

L183 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.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 FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def deleteDegenerateSchreierGenerators
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    PresentedGroup (D.presentationRelators R) ≃*
      PresentedGroup
        (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R)
def

deleteDegenerateSchreierGeneratorHom

L195 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom
Documentation

The homomorphism that deletes degenerate finite Schreier generators. A nondegenerate generator is kept, and a degenerate generator is sent to \(1\).

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def deleteDegenerateSchreierGeneratorHom
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    FreeGroup (FiniteSchreierSymbol X Q) →*
      FreeGroup D.NondegenerateSchreierSymbol
theorem

deleteDegenerateSchreierGeneratorHom_of_not_degenerate

L210 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom_of_not_degenerate
Documentation

The generator-deletion homomorphism sends a nondegenerate finite Schreier generator to the corresponding nondegenerate generator.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem deleteDegenerateSchreierGeneratorHom_of_not_degenerate
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {z : FiniteSchreierSymbol X Q} (hz : ¬ D.IsDegenerateSchreierSymbol z) :
    D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) =
      FreeGroup.of (⟨z, hz⟩ : D.NondegenerateSchreierSymbol)
theorem

deleteDegenerateSchreierGeneratorHom_of_degenerate

L230 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom_of_degenerate
Documentation

The generator-deletion homomorphism sends a degenerate finite Schreier generator to the identity.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem deleteDegenerateSchreierGeneratorHom_of_degenerate
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
    D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) = 1
theorem

symbolEval_eq_one_of_isDegenerateSchreierSymbol

L245 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEval_eq_one_of_isDegenerateSchreierSymbol
Documentation

A degenerate Schreier symbol evaluates to the identity.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem symbolEval_eq_one_of_isDegenerateSchreierSymbol
    {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
    D.symbolEval z = 1
def

nondegenerateSymbolEval

L254 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.nondegenerateSymbolEval
Documentation

The evaluation map on the nondegenerate finite Schreier generators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def nondegenerateSymbolEval
    (z : D.NondegenerateSchreierSymbol) : FreeGroup X
def

nondegenerateSymbolEvalHom

L259 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.nondegenerateSymbolEvalHom
Documentation

The evaluation homomorphism on nondegenerate finite 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 FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def nondegenerateSymbolEvalHom :
    FreeGroup D.NondegenerateSchreierSymbol →* FreeGroup X
theorem

nondegenerateSymbolEvalHom_deleteDegenerateSchreierGeneratorHom

L267 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.nondegenerateSymbolEvalHom_deleteDegenerateSchreierGeneratorHom
Documentation

Evaluating after deleting degenerate Schreier generators agrees with ordinary 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem nondegenerateSymbolEvalHom_deleteDegenerateSchreierGeneratorHom
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (w : FreeGroup (FiniteSchreierSymbol X Q)) :
    D.nondegenerateSymbolEvalHom
        (D.deleteDegenerateSchreierGeneratorHom w) =
      D.symbolEvalHom w
def

cleanedSchreierSymbolWord

L289 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierSymbolWord
Documentation

A single finite Schreier generator after deleting degenerate generators.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def cleanedSchreierSymbolWord
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (z : FiniteSchreierSymbol X Q) :
    FreeGroup D.NondegenerateSchreierSymbol
theorem

cleanedSchreierSymbolWord_of_degenerate

L301 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierSymbolWord_of_degenerate
Documentation

A degenerate Schreier symbol is deleted by the cleaned Schreier-symbol word map.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem cleanedSchreierSymbolWord_of_degenerate
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
    D.cleanedSchreierSymbolWord z = 1
theorem

cleanedSchreierSymbolWord_of_not_degenerate

L313 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierSymbolWord_of_not_degenerate
Documentation

A nondegenerate Schreier symbol is kept as the corresponding generator by the cleaned Schreier-symbol word map.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem cleanedSchreierSymbolWord_of_not_degenerate
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {z : FiniteSchreierSymbol X Q} (hz : ¬ D.IsDegenerateSchreierSymbol z) :
    D.cleanedSchreierSymbolWord z =
      FreeGroup.of (⟨z, hz⟩ : D.NondegenerateSchreierSymbol)
theorem

deleteDegenerateSchreierGeneratorHom_of

L327 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom_of
Documentation

The generator-deletion homomorphism sends a finite Schreier generator to its cleaned Schreier-symbol word.

Source context 7 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem deleteDegenerateSchreierGeneratorHom_of
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (z : FiniteSchreierSymbol X Q) :
    D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) =
      D.cleanedSchreierSymbolWord z

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