ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedSymbols

11 Theorems | 10 Definitions | 2 Abbreviations

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.

imports

Imported by

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.IsDegenerateSchreierSymbol

omit [DecidableEq X] in
def IsDegenerateSchreierSymbol (z : FiniteSchreierSymbol X Q) : Prop :=
  D.quotientSection (D.transition z.1 z.2) =
    D.quotientSection z.1 * FreeGroup.of z.2

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

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.degenerateSchreierRelators

omit [DecidableEq X] in
def degenerateSchreierRelators :
    Set (FreeGroup (FiniteSchreierSymbol X Q)) :=
  { q | ∃ s : Q, ∃ x : X,
      D.quotientSection (D.transition s x) = D.quotientSection s * FreeGroup.of x ∧
        q = FreeGroup.of (s, x) }

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

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelators

def presentationRelators (R : Set (FreeGroup X)) :
    Set (FreeGroup (FiniteSchreierSymbol X Q)) :=
  D.schreierRelators R ∪ D.degenerateSchreierRelators

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

Abbreviation ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.NondegenerateSchreierSymbol

omit [DecidableEq X] in
abbrev NondegenerateSchreierSymbol :=
  Presented.GeneratorPartition.Kept D.IsDegenerateSchreierSymbol

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

Abbreviation ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.DegenerateSchreierSymbol

omit [DecidableEq X] in
abbrev DegenerateSchreierSymbol :=
  Presented.GeneratorPartition.Deleted D.IsDegenerateSchreierSymbol

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

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.trivialGeneratorRelatorsOfPredicate_isDegenerateSchreierSymbol

omit [DecidableEq X] in
theorem trivialGeneratorRelatorsOfPredicate_isDegenerateSchreierSymbol
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    Presented.trivialGeneratorRelatorsOfPredicate D.IsDegenerateSchreierSymbol =
      D.degenerateSchreierRelators

The trivial-generator relators selected by the degeneracy predicate are exactly the degenerate Schreier relators.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol

theorem relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    Presented.relatorsWithTrivialGeneratorsOfPredicate
        (D.schreierRelators R) D.IsDegenerateSchreierSymbol =
      D.presentationRelators R

Adding trivial-generator relators for degenerate Schreier symbols gives the presentation relators.

Show Lean proof

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelatorsAfterDeletingDegenerateSchreierGenerators

def presentationRelatorsAfterDeletingDegenerateSchreierGenerators
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    Set (FreeGroup D.NondegenerateSchreierSymbol) :=
  Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate
    (D.schreierRelators R) D.IsDegenerateSchreierSymbol

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

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorsScript

def deleteDegenerateSchreierGeneratorsScript
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    VerifiedTietzeScript
      (Presentation.ofRelators (D.presentationRelators R))
      (Presentation.ofRelators
        (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R)) := by
  let hRelators :=
    D.relatorsWithTrivialGeneratorsOfPredicate_isDegenerateSchreierSymbol R
  exact
    (VerifiedTietzeScript.replaceRelators
      (fun r hr => RelatorEquivalent.of_mem (by simpa only [hRelators] using hr))
      (fun r hr => RelatorEquivalent.of_mem (by simpa only [hRelators] using hr))).trans
      (VerifiedTietzeScript.deleteTrivialGeneratorsOfPredicate
        (D.schreierRelators R) D.IsDegenerateSchreierSymbol)

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

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorsScript_trace

theorem deleteDegenerateSchreierGeneratorsScript_trace
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    (D.deleteDegenerateSchreierGeneratorsScript R).trace =
      [ElementaryTietzeMove.Kind.replaceRelators,
        ElementaryTietzeMove.Kind.deleteTrivialGenerators]

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.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorsScript_cost

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

The deletion script's weighted cost is the cost of replacing relators plus the weighted cost of deleting each degenerate Schreier generator.

Show Lean proof

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGenerators

noncomputable def deleteDegenerateSchreierGenerators
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    PresentedGroup (D.presentationRelators R) ≃*
      PresentedGroup
        (D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R) :=
  (D.deleteDegenerateSchreierGeneratorsScript R).toCertificate.presentedEquiv

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

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom

def deleteDegenerateSchreierGeneratorHom
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    FreeGroup (FiniteSchreierSymbol X Q) →*
      FreeGroup D.NondegenerateSchreierSymbol :=
  (Presented.trivializeGeneratorsHom
      D.NondegenerateSchreierSymbol D.DegenerateSchreierSymbol).comp
    (FreeGroup.freeGroupCongr
      (Presented.GeneratorPartition.equiv D.IsDegenerateSchreierSymbol))

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

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom_of_not_degenerate

omit [DecidableEq X] in
@[simp]
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)

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

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom_of_degenerate

omit [DecidableEq X] in
@[simp]
theorem deleteDegenerateSchreierGeneratorHom_of_degenerate
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
    D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) = 1

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

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEval_eq_one_of_isDegenerateSchreierSymbol

omit [DecidableEq X] in
theorem symbolEval_eq_one_of_isDegenerateSchreierSymbol
    {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
    D.symbolEval z = 1

A degenerate Schreier symbol evaluates to the identity.

Show Lean proof

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.nondegenerateSymbolEval

def nondegenerateSymbolEval
    (z : D.NondegenerateSchreierSymbol) : FreeGroup X :=
  D.symbolEval z.1

The evaluation map on the nondegenerate finite Schreier generators.

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.nondegenerateSymbolEvalHom

def nondegenerateSymbolEvalHom :
    FreeGroup D.NondegenerateSchreierSymbol →* FreeGroup X :=
  FreeGroup.lift D.nondegenerateSymbolEval

The evaluation homomorphism on nondegenerate finite Schreier symbols.

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.nondegenerateSymbolEvalHom_deleteDegenerateSchreierGeneratorHom

omit [DecidableEq X] in
theorem nondegenerateSymbolEvalHom_deleteDegenerateSchreierGeneratorHom
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (w : FreeGroup (FiniteSchreierSymbol X Q)) :
    D.nondegenerateSymbolEvalHom
        (D.deleteDegenerateSchreierGeneratorHom w) =
      D.symbolEvalHom w

Evaluating after deleting degenerate Schreier generators agrees with ordinary symbol evaluation.

Show Lean proof

Definition ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierSymbolWord

def cleanedSchreierSymbolWord
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (z : FiniteSchreierSymbol X Q) :
    FreeGroup D.NondegenerateSchreierSymbol :=
  if hz : D.IsDegenerateSchreierSymbol z then
    1
  else
    FreeGroup.of (⟨z, hz⟩ : D.NondegenerateSchreierSymbol)

A single finite Schreier generator after deleting degenerate generators.

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierSymbolWord_of_degenerate

omit [DecidableEq X] in
@[simp]
theorem cleanedSchreierSymbolWord_of_degenerate
    [DecidablePred D.IsDegenerateSchreierSymbol]
    {z : FiniteSchreierSymbol X Q} (hz : D.IsDegenerateSchreierSymbol z) :
    D.cleanedSchreierSymbolWord z = 1

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

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierSymbolWord_of_not_degenerate

omit [DecidableEq X] in
@[simp]
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)

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

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.deleteDegenerateSchreierGeneratorHom_of

omit [DecidableEq X] in
@[simp]
theorem deleteDegenerateSchreierGeneratorHom_of
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (z : FiniteSchreierSymbol X Q) :
    D.deleteDegenerateSchreierGeneratorHom (FreeGroup.of z) =
      D.cleanedSchreierSymbolWord z

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

Show Lean proof

ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.CleanedSymbols

Declarations