NYLL
Module

Kernel.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Kernel
7 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Kernel

This module constructs the quotient homomorphisms induced by tau and proves that the Schreier, quotient-section, and augmented relator families give the required kernel-level maps.

Imports1
Imported by2

Declarations

def

tauKernelQuotientHom

L33 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauKernelQuotientHom
Documentation

The \(\tau\)-map sends a kernel element to its class in the quotient by the Schreier relator normal closure.

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 · full declaration
def tauKernelQuotientHom
    (R : Set (FreeGroup X)) :
    D.kernel →* FreeGroup (FiniteSchreierSymbol X Q) ⧸
      Subgroup.normalClosure (D.schreierRelators R) where
  toFun k :=
    QuotientGroup.mk'
      (Subgroup.normalClosure (D.schreierRelators R))
      (D.tau 1 (k : FreeGroup X))
  map_one' := by
    simp only [OneMemClass.coe_one, tau_one, QuotientGroup.mk'_apply, QuotientGroup.mk_one]
  map_mul' k l := by
    change
      QuotientGroup.mk'
          (Subgroup.normalClosure (D.schreierRelators R))
          (D.tau 1 ((k : FreeGroup X) * (l : FreeGroup X))) =
        QuotientGroup.mk'
          (Subgroup.normalClosure (D.schreierRelators R))
          (D.tau 1 (k : FreeGroup X)) *
        QuotientGroup.mk'
          (Subgroup.normalClosure (D.schreierRelators R))
          (D.tau 1 (l : FreeGroup X))
    rw [D.tau_mul_of_mem_kernel k.property]
    rfl
def

tauKernelPresentationQuotientHom

L61 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauKernelPresentationQuotientHom
Documentation

The inverse-map candidate on the kernel for the raw presentation quotient, before descent through the relator subgroup.

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 · full declaration
def tauKernelPresentationQuotientHom
    (R : Set (FreeGroup X)) :
    D.kernel →* FreeGroup (FiniteSchreierSymbol X Q) ⧸
      Subgroup.normalClosure (D.presentationRelators R) where
  toFun k :=
    QuotientGroup.mk'
      (Subgroup.normalClosure (D.presentationRelators R))
      (D.tau 1 (k : FreeGroup X))
  map_one' := by
    simp only [OneMemClass.coe_one, tau_one, QuotientGroup.mk'_apply, QuotientGroup.mk_one]
  map_mul' k l := by
    change
      QuotientGroup.mk'
          (Subgroup.normalClosure (D.presentationRelators R))
          (D.tau 1 ((k : FreeGroup X) * (l : FreeGroup X))) =
        QuotientGroup.mk'
          (Subgroup.normalClosure (D.presentationRelators R))
          (D.tau 1 (k : FreeGroup X)) *
        QuotientGroup.mk'
          (Subgroup.normalClosure (D.presentationRelators R))
          (D.tau 1 (l : FreeGroup X))
    rw [D.tau_mul_of_mem_kernel k.property]
    rfl
def

tauKernelAugmentedPresentationQuotientHom

L89 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauKernelAugmentedPresentationQuotientHom
Documentation

The inverse-map candidate on the kernel for the augmented raw presentation quotient, before descent through the relator subgroup.

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 · full declaration
def tauKernelAugmentedPresentationQuotientHom
    (R : Set (FreeGroup X)) :
    D.kernel →* FreeGroup (FiniteSchreierSymbol X Q) ⧸
      Subgroup.normalClosure (D.augmentedPresentationRelators R) where
  toFun k :=
    QuotientGroup.mk'
      (Subgroup.normalClosure (D.augmentedPresentationRelators R))
      (D.tau 1 (k : FreeGroup X))
  map_one' := by
    simp only [OneMemClass.coe_one, tau_one, QuotientGroup.mk'_apply, QuotientGroup.mk_one]
  map_mul' k l := by
    change
      QuotientGroup.mk'
          (Subgroup.normalClosure (D.augmentedPresentationRelators R))
          (D.tau 1 ((k : FreeGroup X) * (l : FreeGroup X))) =
        QuotientGroup.mk'
          (Subgroup.normalClosure (D.augmentedPresentationRelators R))
          (D.tau 1 (k : FreeGroup X)) *
        QuotientGroup.mk'
          (Subgroup.normalClosure (D.augmentedPresentationRelators R))
          (D.tau 1 (l : FreeGroup X))
    rw [D.tau_mul_of_mem_kernel k.property]
    rfl
theorem

tau_mem_schreierRelators

L117 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_mem_schreierRelators
Documentation

The \(\tau\)-rewrite of an original relator at a finite quotient state belongs to 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 tau_mem_schreierRelators
    {R : Set (FreeGroup X)} (q : Q) {r : FreeGroup X} (hr : r ∈ R) :
    D.tau q r ∈ D.schreierRelators R
theorem

tau_mem_quotientSectionRelators

L123 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_mem_quotientSectionRelators
Documentation

The \(\tau\)-word of a kernel element belongs to the quotient-section 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 tau_mem_quotientSectionRelators (q : Q) :
    D.tau 1 (D.quotientSection q) ∈ D.quotientSectionRelators
theorem

presentationRelators_subset_augmentedPresentationRelators

L131 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelators_subset_augmentedPresentationRelators
Documentation

Every finite-quotient presentation relator is included among the augmented 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 presentationRelators_subset_augmentedPresentationRelators
    (R : Set (FreeGroup X)) :
    D.presentationRelators R ⊆ D.augmentedPresentationRelators R
theorem

quotientSectionRelators_subset_augmentedPresentationRelators

L137 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientSectionRelators_subset_augmentedPresentationRelators
Documentation

Every quotient-section relator is included among the augmented 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 quotientSectionRelators_subset_augmentedPresentationRelators
    (R : Set (FreeGroup X)) :
    D.quotientSectionRelators ⊆ D.augmentedPresentationRelators R

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