Module

NormalWords.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.NormalWords

7 declarations indexed from sourceView source ↗

Module documentation

Reidemeister--Schreier target-presentation normal words

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Target Presentation / Normal Words.

This module packages normal-word witnesses for the cleaned symbols and uses them to construct the cleaned target-presentation data, Tietze equivalence, and kernel equivalence.

Imports1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.Core

Imported by1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.TargetPresentation.All

structure

CleanedReidemeisterSchreierTargetPresentationNormalWordData

L37 ↗

ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationNormalWordData

Documentation

A computation-facing variant of \(\mathrm{CleanedReidemeisterSchreierTargetPresentationData}\), carrying a concrete target word and a certificate that substitution into the reduced \(\mathrm{cleanedTauNormalWord}(q,r)\) reduces to 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 Q : Type*} [Group Q] [Fintype Q]
namespace PrefixClosedFiniteQuotientSchreierData
variable [DecidableEq X]
variable (D : PrefixClosedFiniteQuotientSchreierData X Q)

Lean source · full declaration

structure CleanedReidemeisterSchreierTargetPresentationNormalWordData
    (R : Set (FreeGroup X)) (Y : Type*)
    [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
    [DecidableEq D.nondegenerateSchreierSymbol] [DecidableEq Y] 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
  /-- A concrete target word representing each cleaned Reidemeister--Schreier relator. -/
  cleanedRelatorWord : Q → FreeGroup X → List (Y × Bool)
  /--
  Substituting target words into a cleaned normal word reduces to the specified target relator
  word.
  -/
  cleanedRelatorWord_reduce :
    ∀ q : Q, ∀ r ∈ R,
      FreeGroup.reduce
          (freeGroupSubstitutionWord toTargetGenerator
            (D.cleanedTauNormalWord q r)) =
        FreeGroup.reduce (cleanedRelatorWord q r)
  /-- Every specified target relator word is trivial modulo the target relators. -/
  mapsCleanedRelatorWords :
    ∀ q : Q, ∀ r ∈ R,
      RelatorEquivalent targetRelators
        (FreeGroup.mk (cleanedRelatorWord 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)

theorem

mapsCleanedRelators

L93 ↗

ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationNormalWordData.mapsCleanedRelators

Documentation

The normal-word target data maps every cleaned Schreier relator to an identity modulo the target relators.

Source context 11 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 CleanedReidemeisterSchreierTargetPresentationNormalWordData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
variable [DecidableEq D.nondegenerateSchreierSymbol] [DecidableEq Y]

Lean source · statement

theorem mapsCleanedRelators
    (C : D.CleanedReidemeisterSchreierTargetPresentationNormalWordData R Y) :
    ∀ q : Q, ∀ r ∈ R,
      RelatorEquivalent C.targetRelators
        (FreeGroup.lift C.toTargetGenerator (D.cleanedTau q r)) 1

def

toTargetPresentationData

L107 ↗

ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationNormalWordData.toTargetPresentationData

Documentation

Normal-word target presentation data forgets to the corresponding cleaned target presentation data.

Source context 11 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 CleanedReidemeisterSchreierTargetPresentationNormalWordData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
variable [DecidableEq D.nondegenerateSchreierSymbol] [DecidableEq Y]

Lean source · full declaration

def toTargetPresentationData
    (C : D.CleanedReidemeisterSchreierTargetPresentationNormalWordData R Y) :
    D.CleanedReidemeisterSchreierTargetPresentationData R Y where
  targetRelators := C.targetRelators
  toTargetGenerator := C.toTargetGenerator
  fromTargetGenerator := C.fromTargetGenerator
  mapsCleanedRelators := C.mapsCleanedRelators
  mapsTargetRelators := C.mapsTargetRelators
  from_toTargetGenerator := C.from_toTargetGenerator
  to_fromTargetGenerator := C.to_fromTargetGenerator

def

toTietzeEquiv

L119 ↗

ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationNormalWordData.toTietzeEquiv

Documentation

The normal-word cleaned target presentation data yields a Tietze equivalence.

Source context 11 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 CleanedReidemeisterSchreierTargetPresentationNormalWordData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
variable [DecidableEq D.nondegenerateSchreierSymbol] [DecidableEq Y]

Lean source · statement

def toTietzeEquiv
    (C : D.CleanedReidemeisterSchreierTargetPresentationNormalWordData R Y) :
    TietzeEquiv (D.cleanedSchreierRelators R) C.targetRelators

def

presentedEquiv

L128 ↗

ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationNormalWordData.presentedEquiv

Documentation

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

Source context 11 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 CleanedReidemeisterSchreierTargetPresentationNormalWordData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
variable [DecidableEq D.nondegenerateSchreierSymbol] [DecidableEq Y]

Lean source · statement

def presentedEquiv
    (C : D.CleanedReidemeisterSchreierTargetPresentationNormalWordData R Y) :
    PresentedGroup (D.cleanedSchreierRelators R) ≃*
      PresentedGroup C.targetRelators

def

targetPresentedGroupEquivKernel

L138 ↗

ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationNormalWordData.targetPresentedGroupEquivKernel

Documentation

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

Source context 11 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 CleanedReidemeisterSchreierTargetPresentationNormalWordData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
variable [DecidableEq D.nondegenerateSchreierSymbol] [DecidableEq Y]

Lean source · statement

def targetPresentedGroupEquivKernel
    (C : D.CleanedReidemeisterSchreierTargetPresentationNormalWordData R Y)
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    PresentedGroup C.targetRelators ≃*
      D.kernel ⧸ relatorSubgroup D R

def

toPresentationEquivCertificate

L146 ↗

ReidemeisterSchreier.Discrete.PrefixClosedFiniteQuotientSchreierData.CleanedReidemeisterSchreierTargetPresentationNormalWordData.toPresentationEquivCertificate

Documentation

The normal-word cleaned target presentation data yields the corresponding Tietze script.

Source context 11 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 CleanedReidemeisterSchreierTargetPresentationNormalWordData
variable {D}
variable {R : Set (FreeGroup X)} {Y : Type*}
variable [DecidablePred D.toFiniteQuotientSchreierData.IsDegenerateSchreierSymbol]
variable [DecidableEq D.nondegenerateSchreierSymbol] [DecidableEq Y]

Lean source · statement

def toPresentationEquivCertificate
    (C : D.CleanedReidemeisterSchreierTargetPresentationNormalWordData R Y) :
    PresentationEquivCertificate
      (Presentation.ofRelators (D.cleanedSchreierRelators R))
      (Presentation.ofRelators C.targetRelators)

Module documentation

Reidemeister--Schreier target-presentation normal words

Declarations

CleanedReidemeisterSchreierTargetPresentationNormalWordData

mapsCleanedRelators

toTargetPresentationData

toTietzeEquiv

presentedEquiv

targetPresentedGroupEquivKernel

toPresentationEquivCertificate