NYLL
Module

CleanedRelators.lean

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

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Cleaned Relators

This module removes relators attached to degenerate Schreier symbols, builds the finite cleaned relator set, and records the remaining quotient-section and augmented relator families.

Imports1
Imported by2

Declarations

def

cleanedSchreierRelators

L33 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierRelators
Documentation

This is the relator family obtained by rewriting original relators and then 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 FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def cleanedSchreierRelators
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    Set (FreeGroup D.NondegenerateSchreierSymbol)
theorem

mem_cleanedSchreierRelators

L43 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mem_cleanedSchreierRelators
Documentation

Membership in the cleaned Schreier relator set is characterized by a quotient element and an original relator whose cleaned rewrite gives the word.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem mem_cleanedSchreierRelators
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol]
    (q : Q) {r : FreeGroup X} (hr : r ∈ R) :
    D.cleanedTau q r ∈ D.cleanedSchreierRelators R
def

cleanedSchreierRelatorFinset

L54 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.cleanedSchreierRelatorFinset
Documentation

The cleaned Schreier relator finset contains the cleaned rewrites of the finite quotient elements and 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def cleanedSchreierRelatorFinset
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq (FreeGroup D.NondegenerateSchreierSymbol)]
    (R : Finset (FreeGroup X)) :
    Finset (FreeGroup D.NondegenerateSchreierSymbol)
theorem

mem_cleanedSchreierRelatorFinset

L67 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mem_cleanedSchreierRelatorFinset
Documentation

Membership in the cleaned Schreier relator finset is characterized by a quotient element and an original relator whose cleaned rewrite gives the word.

Source context 6 commands

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

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem mem_cleanedSchreierRelatorFinset
    {D : FiniteQuotientSchreierData X Q}
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq (FreeGroup D.NondegenerateSchreierSymbol)]
    {R : Finset (FreeGroup X)} {z : FreeGroup D.NondegenerateSchreierSymbol} :
    z ∈ D.cleanedSchreierRelatorFinset R ↔
      z ∈ D.cleanedSchreierRelators ({r | r ∈ R} : Set (FreeGroup X))
theorem

coe_cleanedSchreierRelatorFinset

L80 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.coe_cleanedSchreierRelatorFinset
Documentation

Coercing the cleaned Schreier relator finset gives the cleaned 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem coe_cleanedSchreierRelatorFinset
    [DecidablePred D.IsDegenerateSchreierSymbol]
    [DecidableEq (FreeGroup D.NondegenerateSchreierSymbol)]
    (R : Finset (FreeGroup X)) :
    ({z | z ∈ D.cleanedSchreierRelatorFinset R} :
      Set (FreeGroup D.NondegenerateSchreierSymbol)) =
      D.cleanedSchreierRelators ({r | r ∈ R} : Set (FreeGroup X))
theorem

presentationRelatorsAfterDeletingDegenerate_eq_cleaned

L94 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelatorsAfterDeletingDegenerate_eq_cleaned
Documentation

The relators after deleting degenerate Schreier generators are exactly the cleaned 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem presentationRelatorsAfterDeletingDegenerate_eq_cleaned
    (R : Set (FreeGroup X))
    [DecidablePred D.IsDegenerateSchreierSymbol] :
    D.presentationRelatorsAfterDeletingDegenerateSchreierGenerators R =
      D.cleanedSchreierRelators R
def

quotientSectionRelators

L123 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientSectionRelators
Documentation

Relators forcing the chosen quotient representatives to rewrite to the empty word. These are automatic for a prefix-closed Schreier transversal, but are useful for arbitrary finite quotient sections.

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

augmentedPresentationRelators

L131 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.augmentedPresentationRelators
Documentation

The augmented presentation relators combine quotient-section relators with 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
def augmentedPresentationRelators (R : Set (FreeGroup X)) :
    Set (FreeGroup (FiniteSchreierSymbol X Q))
def

schreierRelatorFinset

L136 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.schreierRelatorFinset
Documentation

A finite set enumerating the finite-quotient 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def schreierRelatorFinset
    (R : Finset (FreeGroup X)) :
    Finset (FreeGroup (FiniteSchreierSymbol X Q))
theorem

mem_schreierRelatorFinset

L146 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mem_schreierRelatorFinset
Documentation

Membership in the Schreier-relator finset is equivalent to membership in the finite-quotient 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem mem_schreierRelatorFinset
    {D : FiniteQuotientSchreierData X Q}
    {R : Finset (FreeGroup X)}
    {z : FreeGroup (FiniteSchreierSymbol X Q)} :
    z ∈ D.schreierRelatorFinset R ↔
      z ∈ D.schreierRelators ({r | r ∈ R} : Set (FreeGroup X))
def

degenerateSchreierRelatorFinset

L158 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.degenerateSchreierRelatorFinset
Documentation

A finite set enumerating the degenerate finite-quotient 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def degenerateSchreierRelatorFinset [Fintype X] :
    Finset (FreeGroup (FiniteSchreierSymbol X Q))
theorem

mem_degenerateSchreierRelatorFinset

L171 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mem_degenerateSchreierRelatorFinset
Documentation

Membership in the degenerate-Schreier-relator finset is equivalent to membership in the degenerate 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem mem_degenerateSchreierRelatorFinset [Fintype X]
    {D : FiniteQuotientSchreierData X Q}
    {z : FreeGroup (FiniteSchreierSymbol X Q)} :
    z ∈ D.degenerateSchreierRelatorFinset ↔
      z ∈ D.degenerateSchreierRelators
def

presentationRelatorFinset

L183 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelatorFinset
Documentation

A finite set enumerating the finite-quotient 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
def presentationRelatorFinset [Fintype X]
    (R : Finset (FreeGroup X)) :
    Finset (FreeGroup (FiniteSchreierSymbol X Q))
theorem

mem_presentationRelatorFinset

L193 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mem_presentationRelatorFinset
Documentation

Membership in the presentation-relator finset is equivalent to membership in the finite-quotient presentation 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem mem_presentationRelatorFinset [Fintype X]
    {D : FiniteQuotientSchreierData X Q}
    {R : Finset (FreeGroup X)}
    {z : FreeGroup (FiniteSchreierSymbol X Q)} :
    z ∈ D.presentationRelatorFinset R ↔
      z ∈ D.presentationRelators ({r | r ∈ R} : Set (FreeGroup X))
theorem

coe_presentationRelatorFinset

L205 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.coe_presentationRelatorFinset
Documentation

The presentation-relator finset coerces to the finite-quotient presentation 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem coe_presentationRelatorFinset [Fintype X]
    (R : Finset (FreeGroup X)) :
    ({z | z ∈ D.presentationRelatorFinset R} :
      Set (FreeGroup (FiniteSchreierSymbol X Q))) =
      D.presentationRelators ({r | r ∈ R} : Set (FreeGroup X))
def

quotientSectionRelatorFinset

L217 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientSectionRelatorFinset
Documentation

The quotient-section relator finset contains the finite relators killing the chosen quotient-section words.

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 quotientSectionRelatorFinset :
    Finset (FreeGroup (FiniteSchreierSymbol X Q))
theorem

mem_quotientSectionRelatorFinset

L226 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mem_quotientSectionRelatorFinset
Documentation

Membership in the quotient-section relator finset is characterized by a quotient element whose section word is being killed.

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 mem_quotientSectionRelatorFinset
    {D : FiniteQuotientSchreierData X Q}
    {z : FreeGroup (FiniteSchreierSymbol X Q)} :
    z ∈ D.quotientSectionRelatorFinset ↔
      z ∈ D.quotientSectionRelators
def

augmentedPresentationRelatorFinset

L239 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.augmentedPresentationRelatorFinset
Documentation

The finite augmented presentation relator set combines quotient-section relators with the finite 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
def augmentedPresentationRelatorFinset [Fintype X]
    (R : Finset (FreeGroup X)) :
    Finset (FreeGroup (FiniteSchreierSymbol X Q))
theorem

mem_augmentedPresentationRelatorFinset

L249 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.mem_augmentedPresentationRelatorFinset
Documentation

Membership in the augmented presentation relator finset is membership in either the quotient-section relators or the presentation relator finset.

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 mem_augmentedPresentationRelatorFinset [Fintype X]
    {D : FiniteQuotientSchreierData X Q}
    {R : Finset (FreeGroup X)}
    {z : FreeGroup (FiniteSchreierSymbol X Q)} :
    z ∈ D.augmentedPresentationRelatorFinset R ↔
      z ∈ D.augmentedPresentationRelators ({r | r ∈ R} : Set (FreeGroup X))
theorem

coe_augmentedPresentationRelatorFinset

L263 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.coe_augmentedPresentationRelatorFinset
Documentation

Coercing the augmented presentation relator finset gives the augmented presentation 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 Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem coe_augmentedPresentationRelatorFinset [Fintype X]
    (R : Finset (FreeGroup X)) :
    ({z | z ∈ D.augmentedPresentationRelatorFinset R} :
      Set (FreeGroup (FiniteSchreierSymbol X Q))) =
      D.augmentedPresentationRelators ({r | r ∈ R} : Set (FreeGroup X))

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