Module

Presentation.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.Presentation

51 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Presentation

This module proves the normal-closure identities behind the finite-quotient Reidemeister--Schreier presentation, including tau images of section words, symbols, and conjugated original relators.

Imports1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.WordCertificates

Imported by2

theorem

tauList_mem_normalClosure_degenerateSchreierRelators_of_prefixClosedAlongList

L34 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauList_mem_normalClosure_degenerateSchreierRelators_of_prefixClosedAlongList

Documentation

A list whose successive quotient states follow the chosen prefix-closed section rewrites into the normal closure of 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 tauList_mem_normalClosure_degenerateSchreierRelators_of_prefixClosedAlongList
    {q : Q} {xs : List (X × Bool)}
    (hprefix : D.prefixClosedAlongList q xs) :
    D.tauList q xs ∈ Subgroup.normalClosure D.degenerateSchreierRelators

theorem

tau_quotientSection_mem_normalClosure_degenerateSchreierRelators_of_isPrefixClosed

L65 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_quotientSection_mem_normalClosure_degenerateSchreierRelators_of_isPrefixClosed

Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier 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 · statement

theorem tau_quotientSection_mem_normalClosure_degenerateSchreierRelators_of_isPrefixClosed
    (hprefix : D.IsPrefixClosedQuotientSection) (q : Q) :
    D.tau 1 (D.quotientSection q) ∈
      Subgroup.normalClosure D.degenerateSchreierRelators

theorem

tau_quotientSection_mem_normalClosure_presentationRelators_of_isPrefixClosed

L77 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_quotientSection_mem_normalClosure_presentationRelators_of_isPrefixClosed

Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier 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 · statement

theorem tau_quotientSection_mem_normalClosure_presentationRelators_of_isPrefixClosed
    (R : Set (FreeGroup X))
    (hprefix : D.IsPrefixClosedQuotientSection) (q : Q) :
    D.tau 1 (D.quotientSection q) ∈
      Subgroup.normalClosure (D.presentationRelators R)

theorem

quotientSectionRelator_relatorEquivalent_one

L91 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientSectionRelator_relatorEquivalent_one

Documentation

A quotient-section relator is relator-equivalent to the identity modulo 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 quotientSectionRelator_relatorEquivalent_one
    (R : Set (FreeGroup X)) (q : Q) :
    RelatorEquivalent (D.augmentedPresentationRelators R)
      (D.tau 1 (D.quotientSection q)) 1

theorem

tau_symbolEval_relatorEquivalent_augmentedPresentationRelators

L103 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_symbolEval_relatorEquivalent_augmentedPresentationRelators

Documentation

The \(\tau\)-word and its symbol evaluation are relator-equivalent modulo 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 tau_symbolEval_relatorEquivalent_augmentedPresentationRelators
    (R : Set (FreeGroup X)) (q : Q) (x : X) :
    RelatorEquivalent (D.augmentedPresentationRelators R)
      (D.tau 1 (D.symbolEval (q, x))) (FreeGroup.of (q, x))

theorem

tau_symbolEvalHom_relatorEquivalent_augmentedPresentationRelators

L173 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_symbolEvalHom_relatorEquivalent_augmentedPresentationRelators

Documentation

The \(\tau\)-word and its symbol evaluation are relator-equivalent modulo 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 tau_symbolEvalHom_relatorEquivalent_augmentedPresentationRelators
    (R : Set (FreeGroup X)) (z : FreeGroup (FiniteSchreierSymbol X Q)) :
    RelatorEquivalent (D.augmentedPresentationRelators R)
      (D.tau 1 (D.symbolEvalHom z)) z

theorem

tau_conjugate_relator_mem_normalClosure_schreierRelators

L206 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_conjugate_relator_mem_normalClosure_schreierRelators

Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier 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 · statement

theorem tau_conjugate_relator_mem_normalClosure_schreierRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (g : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    D.tau 1 (g * r * g⁻¹) ∈
      Subgroup.normalClosure (D.schreierRelators R)

theorem

tau_conjugate_relator_mem_normalClosure_presentationRelators

L242 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_conjugate_relator_mem_normalClosure_presentationRelators

Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier 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 · statement

theorem tau_conjugate_relator_mem_normalClosure_presentationRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (g : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    D.tau 1 (g * r * g⁻¹) ∈
      Subgroup.normalClosure (D.presentationRelators R)

theorem

tau_conjugate_relator_mem_normalClosure_augmentedPresentationRelators

L256 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tau_conjugate_relator_mem_normalClosure_augmentedPresentationRelators

Documentation

The \(\tau\)-rewrite of the indicated relator or section word belongs to the appropriate Reidemeister--Schreier 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 · statement

theorem tau_conjugate_relator_mem_normalClosure_augmentedPresentationRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (g : FreeGroup X) {r : FreeGroup X} (hr : r ∈ R) :
    D.tau 1 (g * r * g⁻¹) ∈
      Subgroup.normalClosure (D.augmentedPresentationRelators R)

theorem

tauKernelPresentationQuotientHom_eq_one_of_mem_normalClosure

L270 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauKernelPresentationQuotientHom_eq_one_of_mem_normalClosure

Documentation

The \(\tau\)-homomorphism to the presentation-relator quotient kills every element of the normal closure of the 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

theorem tauKernelPresentationQuotientHom_eq_one_of_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {n : FreeGroup X} (hn : n ∈ Subgroup.normalClosure R) :
    D.tauKernelPresentationQuotientHom R ⟨n, hR hn⟩ = 1

def

tauRelatorSubgroupPresentationQuotientHom

L324 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauRelatorSubgroupPresentationQuotientHom

Documentation

The \(\tau\)-map descends from the kernel's relator-subgroup quotient to the quotient by the finite Schreier 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 tauRelatorSubgroupPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    D.kernel ⧸ D.relatorSubgroup R →*
      FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.presentationRelators R)

theorem

tauKernelAugmentedPresentationQuotientHom_eq_one_of_mem_normalClosure

L345 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauKernelAugmentedPresentationQuotientHom_eq_one_of_mem_normalClosure

Documentation

The \(\tau\)-homomorphism to the augmented-presentation quotient kills every element of the normal closure of the 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

theorem tauKernelAugmentedPresentationQuotientHom_eq_one_of_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {n : FreeGroup X} (hn : n ∈ Subgroup.normalClosure R) :
    D.tauKernelAugmentedPresentationQuotientHom R ⟨n, hR hn⟩ = 1

def

tauRelatorSubgroupAugmentedPresentationQuotientHom

L399 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauRelatorSubgroupAugmentedPresentationQuotientHom

Documentation

The \(\tau\)-map descends from the relator-subgroup quotient to the augmented Schreier presentation quotient.

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 tauRelatorSubgroupAugmentedPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    D.kernel ⧸ D.relatorSubgroup R →*
      FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.augmentedPresentationRelators R)

theorem

degenerateSchreierRelator_eval_eq_one

L421 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.degenerateSchreierRelator_eval_eq_one

Documentation

Every degenerate finite-quotient Schreier relator evaluates to the identity under the finite Schreier evaluation 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 degenerateSchreierRelator_eval_eq_one
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ D.degenerateSchreierRelators) :
    D.symbolEvalHom q = 1

theorem

quotientMap_relator_eq_one_of_normalClosure_le_kernel

L438 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientMap_relator_eq_one_of_normalClosure_le_kernel

Documentation

If the relator normal closure is contained in the kernel, the quotient map sends each relator to \(1\).

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 quotientMap_relator_eq_one_of_normalClosure_le_kernel
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {r : FreeGroup X} (hr : r ∈ R) :
    D.quotientMap r = 1

theorem

quotientMap_quotientSection_mul_relator

L450 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientMap_quotientSection_mul_relator

Documentation

Multiplying a quotient section by an original relator has the same quotient-map value as the quotient section.

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 quotientMap_quotientSection_mul_relator
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (q : Q) {r : FreeGroup X} (hr : r ∈ R) :
    D.quotientMap (D.quotientSection q * r) = q

theorem

eval_tau_relator_mem_normalClosure

L462 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_tau_relator_mem_normalClosure

Documentation

The evaluated \(\tau\)-word of an original relator lies in the normal closure of the 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

theorem eval_tau_relator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (q : Q) {r : FreeGroup X} (hr : r ∈ R) :
    D.symbolEvalHom (D.tau q r) ∈ Subgroup.normalClosure R

theorem

eval_schreierRelator_mem_normalClosure

L478 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_schreierRelator_mem_normalClosure

Documentation

Evaluating a finite-quotient Schreier relator gives an element of the normal closure of the 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

theorem eval_schreierRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ D.schreierRelators R) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

eval_mem_normalClosure_of_mem_normalClosure_schreierRelators

L491 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_mem_normalClosure_of_mem_normalClosure_schreierRelators

Documentation

Membership in the source relator normal closure is preserved by the Reidemeister--Schreier evaluation map.

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 eval_mem_normalClosure_of_mem_normalClosure_schreierRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ Subgroup.normalClosure (D.schreierRelators R)) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

eval_degenerateSchreierRelator_mem_normalClosure

L505 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_degenerateSchreierRelator_mem_normalClosure

Documentation

The evaluation of a degenerate finite-quotient Schreier relator lies in the normal closure of the finite-quotient presentation 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 eval_degenerateSchreierRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ D.degenerateSchreierRelators) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

eval_presentationRelator_mem_normalClosure

L516 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_presentationRelator_mem_normalClosure

Documentation

Evaluating a finite-quotient presentation relator gives an element of the normal closure of the 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

theorem eval_presentationRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ D.presentationRelators R) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

quotientSectionRelator_eval_eq_one

L527 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientSectionRelator_eval_eq_one

Documentation

The symbol evaluation of a quotient-section relator is the identity.

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 quotientSectionRelator_eval_eq_one
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ D.quotientSectionRelators) :
    D.symbolEvalHom q = 1

theorem

eval_quotientSectionRelator_mem_normalClosure

L539 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_quotientSectionRelator_mem_normalClosure

Documentation

The indicated evaluated relator belongs to the normal closure supplied by the Reidemeister--Schreier relator comparison.

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 eval_quotientSectionRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ D.quotientSectionRelators) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

eval_augmentedPresentationRelator_mem_normalClosure

L550 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_augmentedPresentationRelator_mem_normalClosure

Documentation

The indicated evaluated relator belongs to the normal closure supplied by the Reidemeister--Schreier relator comparison.

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 eval_augmentedPresentationRelator_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ D.augmentedPresentationRelators R) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

eval_mem_normalClosure_of_mem_normalClosure_presentationRelators

L564 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_mem_normalClosure_of_mem_normalClosure_presentationRelators

Documentation

Membership in the source relator normal closure is preserved by the Reidemeister--Schreier evaluation map.

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 eval_mem_normalClosure_of_mem_normalClosure_presentationRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ Subgroup.normalClosure (D.presentationRelators R)) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

eval_mem_normalClosure_of_mem_normalClosure_augmentedPresentationRelators

L577 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.eval_mem_normalClosure_of_mem_normalClosure_augmentedPresentationRelators

Documentation

Membership in the source relator normal closure is preserved by the Reidemeister--Schreier evaluation map.

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 eval_mem_normalClosure_of_mem_normalClosure_augmentedPresentationRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ Subgroup.normalClosure (D.augmentedPresentationRelators R)) :
    D.symbolEvalHom q ∈ Subgroup.normalClosure R

theorem

symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_schreierRelators

L590 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_schreierRelators

Documentation

The symbol-evaluation subgroup homomorphism sends the indicated normal-closure element into 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 · statement

theorem symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_schreierRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ Subgroup.normalClosure (D.schreierRelators R)) :
    D.symbolEvalSubgroupHom q ∈ D.relatorSubgroup R

theorem

symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_presentationRelators

L603 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_presentationRelators

Documentation

The symbol-evaluation subgroup homomorphism sends the indicated normal-closure element into 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 · statement

theorem symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure_presentationRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ Subgroup.normalClosure (D.presentationRelators R)) :
    D.symbolEvalSubgroupHom q ∈ D.relatorSubgroup R

theorem

symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure

L616 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure

Documentation

A word in the normal closure of augmented presentation relators evaluates into 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 · statement

theorem symbolEvalSubgroupHom_mem_relatorSubgroup_of_mem_normalClosure
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    {q : FreeGroup (FiniteSchreierSymbol X Q)}
    (hq : q ∈ Subgroup.normalClosure (D.augmentedPresentationRelators R)) :
    D.symbolEvalSubgroupHom q ∈ D.relatorSubgroup R

def

symbolEvalQuotientHom

L629 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalQuotientHom

Documentation

The canonical map from the finite Schreier-relator quotient to the kernel modulo its intersection with the normal closure of \(R\).

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 symbolEvalQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.schreierRelators R) →*
      D.kernel ⧸ D.relatorSubgroup R

theorem

symbolEvalQuotientHom_tauKernelQuotientHom

L652 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalQuotientHom_tauKernelQuotientHom

Documentation

Evaluating the \(\tau\)-image of a kernel element recovers its class in the corresponding relator quotient.

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 symbolEvalQuotientHom_tauKernelQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (k : D.kernel) :
    D.symbolEvalQuotientHom hR (D.tauKernelQuotientHom R k) =
      QuotientGroup.mk' (D.relatorSubgroup R) k

theorem

symbolEvalQuotientHom_surjective

L672 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalQuotientHom_surjective

Documentation

The Schreier-relator quotient evaluation map is surjective.

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 symbolEvalQuotientHom_surjective
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    Function.Surjective (D.symbolEvalQuotientHom hR)

def

symbolEvalPresentationQuotientHom

L685 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalPresentationQuotientHom

Documentation

The canonical map from the raw finite Reidemeister--Schreier presentation quotient to the kernel modulo its intersection with the normal closure of \(R\).

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 symbolEvalPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.presentationRelators R) →*
      D.kernel ⧸ D.relatorSubgroup R

def

symbolEvalAugmentedPresentationQuotientHom

L708 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalAugmentedPresentationQuotientHom

Documentation

The evaluation map from the augmented finite Reidemeister--Schreier presentation quotient to the relator-subgroup quotient of the kernel.

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 symbolEvalAugmentedPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.augmentedPresentationRelators R) →*
      D.kernel ⧸ D.relatorSubgroup R

theorem

symbolEvalPresentationQuotientHom_tauKernelPresentationQuotientHom

L731 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalPresentationQuotientHom_tauKernelPresentationQuotientHom

Documentation

Evaluating the \(\tau\)-image of a kernel element recovers its class in the corresponding relator quotient.

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 symbolEvalPresentationQuotientHom_tauKernelPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (k : D.kernel) :
    D.symbolEvalPresentationQuotientHom hR
        (D.tauKernelPresentationQuotientHom R k) =
      QuotientGroup.mk' (D.relatorSubgroup R) k

theorem

symbolEvalPresentationQuotientHom_tauRelatorSubgroupPresentationQuotientHom

L751 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalPresentationQuotientHom_tauRelatorSubgroupPresentationQuotientHom

Documentation

The symbol-evaluation map is inverse to the \(\tau\)-map on the relator-subgroup quotient.

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 symbolEvalPresentationQuotientHom_tauRelatorSubgroupPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (y : D.kernel ⧸ D.relatorSubgroup R) :
    D.symbolEvalPresentationQuotientHom hR
        (D.tauRelatorSubgroupPresentationQuotientHom hR y) = y

theorem

symbolEvalAugmentedPresentationQuotientHom_tauKernelAugmentedPresentationQuotientHom

L765 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalAugmentedPresentationQuotientHom_tauKernelAugmentedPresentationQuotientHom

Documentation

Evaluating the \(\tau\)-image of a kernel element recovers its class in the corresponding relator quotient.

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 symbolEvalAugmentedPresentationQuotientHom_tauKernelAugmentedPresentationQuotientHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (k : D.kernel) :
    D.symbolEvalAugmentedPresentationQuotientHom hR
        (D.tauKernelAugmentedPresentationQuotientHom R k) =
      QuotientGroup.mk' (D.relatorSubgroup R) k

theorem

symbolEvalQuotHom_tauRelatorQuotHom

L788 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalQuotHom_tauRelatorQuotHom

Documentation

Evaluating after the \(\tau\)-relator quotient map returns the original relator quotient class.

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 symbolEvalQuotHom_tauRelatorQuotHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (y : D.kernel ⧸ D.relatorSubgroup R) :
    D.symbolEvalAugmentedPresentationQuotientHom hR
        (D.tauRelatorSubgroupAugmentedPresentationQuotientHom hR y) = y

theorem

tauRelatorQuotHom_symbolEvalQuotHom

L802 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.tauRelatorQuotHom_symbolEvalQuotHom

Documentation

Applying the \(\tau\)-relator quotient map after symbol evaluation returns the original augmented presentation quotient class.

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 tauRelatorQuotHom_symbolEvalQuotHom
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (y : FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.augmentedPresentationRelators R)) :
    D.tauRelatorSubgroupAugmentedPresentationQuotientHom hR
        (D.symbolEvalAugmentedPresentationQuotientHom hR y) = y

def

augmentedPresentationQuotientEquiv

L825 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.augmentedPresentationQuotientEquiv

Documentation

The augmented finite Schreier presentation quotient is equivalent to the kernel relator quotient.

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 augmentedPresentationQuotientEquiv
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.augmentedPresentationRelators R) ≃*
      D.kernel ⧸ D.relatorSubgroup R where
  toFun := D.symbolEvalAugmentedPresentationQuotientHom hR
  invFun := D.tauRelatorSubgroupAugmentedPresentationQuotientHom hR
  left_inv :=
    D.tauRelatorQuotHom_symbolEvalQuotHom hR
  right_inv :=
    D.symbolEvalQuotHom_tauRelatorQuotHom hR
  map_mul' x y := (D.symbolEvalAugmentedPresentationQuotientHom hR).map_mul x y

def

augmentedPresentedGroupEquiv

L840 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.augmentedPresentedGroupEquiv

Documentation

The augmented finite Schreier presented group is equivalent to the kernel relator quotient.

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 augmentedPresentedGroupEquiv
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    PresentedGroup (D.augmentedPresentationRelators R) ≃*
      D.kernel ⧸ D.relatorSubgroup R

theorem

normalClosure_augmentedPresentationRelators_eq

L851 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.normalClosure_augmentedPresentationRelators_eq

Documentation

The augmented-presentation relator normal closure equals the normal closure generated by the corresponding Reidemeister--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 normalClosure_augmentedPresentationRelators_eq
    {R : Set (FreeGroup X)}
    (hsection :
      ∀ q : Q,
        D.tau 1 (D.quotientSection q) ∈
          Subgroup.normalClosure (D.presentationRelators R)) :
    Subgroup.normalClosure (D.augmentedPresentationRelators R) =
      Subgroup.normalClosure (D.presentationRelators R)

theorem

normalClosure_augmentedPresentationRelators_eq_of_isPrefixClosed

L872 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.normalClosure_augmentedPresentationRelators_eq_of_isPrefixClosed

Documentation

The augmented-presentation relator normal closure equals the normal closure generated by the corresponding Reidemeister--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 normalClosure_augmentedPresentationRelators_eq_of_isPrefixClosed
    {R : Set (FreeGroup X)}
    (hprefix : D.IsPrefixClosedQuotientSection) :
    Subgroup.normalClosure (D.augmentedPresentationRelators R) =
      Subgroup.normalClosure (D.presentationRelators R)

def

presentationQuotientEquivOfQuotientSectionRelators

L886 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationQuotientEquivOfQuotientSectionRelators

Documentation

After adding quotient-section relators, the finite Schreier presentation quotient is equivalent to the kernel relator quotient.

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 presentationQuotientEquivOfQuotientSectionRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (hsection :
      ∀ q : Q,
        D.tau 1 (D.quotientSection q) ∈
          Subgroup.normalClosure (D.presentationRelators R)) :
    FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.presentationRelators R) ≃*
      D.kernel ⧸ D.relatorSubgroup R

def

presentationPresentedGroupEquivOfQuotientSectionRelators

L908 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationPresentedGroupEquivOfQuotientSectionRelators

Documentation

After adding quotient-section relators, the finite Schreier presented group is equivalent to the kernel quotient.

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 presentationPresentedGroupEquivOfQuotientSectionRelators
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (hsection :
      ∀ q : Q,
        D.tau 1 (D.quotientSection q) ∈
          Subgroup.normalClosure (D.presentationRelators R)) :
    PresentedGroup (D.presentationRelators R) ≃*
      D.kernel ⧸ D.relatorSubgroup R

def

presentationQuotientEquivOfIsPrefixClosedQuotientSection

L923 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationQuotientEquivOfIsPrefixClosedQuotientSection

Documentation

For a prefix-closed quotient section, the finite Schreier presentation quotient is equivalent to the kernel relator quotient.

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 presentationQuotientEquivOfIsPrefixClosedQuotientSection
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (hprefix : D.IsPrefixClosedQuotientSection) :
    FreeGroup (FiniteSchreierSymbol X Q) ⧸
        Subgroup.normalClosure (D.presentationRelators R) ≃*
      D.kernel ⧸ D.relatorSubgroup R

def

presentationPresentedGroupEquivOfIsPrefixClosedQuotientSection

L939 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationPresentedGroupEquivOfIsPrefixClosedQuotientSection

Documentation

For a prefix-closed quotient section, the finite Schreier presented group is equivalent to the kernel quotient.

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 presentationPresentedGroupEquivOfIsPrefixClosedQuotientSection
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel)
    (hprefix : D.IsPrefixClosedQuotientSection) :
    PresentedGroup (D.presentationRelators R) ≃*
      D.kernel ⧸ D.relatorSubgroup R

def

augmentedPresentationRelatorFinsetPresentedGroupEquiv

L951 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.augmentedPresentationRelatorFinsetPresentedGroupEquiv

Documentation

The presented group using the finite augmented relator finset is equivalent to the kernel relator quotient.

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 augmentedPresentationRelatorFinsetPresentedGroupEquiv [Fintype X]
    (R : Finset (FreeGroup X))
    (hR : Subgroup.normalClosure ({r | r ∈ R} : Set (FreeGroup X)) ≤ D.kernel) :
    PresentedGroup
        ({z | z ∈ D.augmentedPresentationRelatorFinset R} :
          Set (FreeGroup (FiniteSchreierSymbol X Q))) ≃*
      D.kernel ⧸ D.relatorSubgroup ({r | r ∈ R} : Set (FreeGroup X))

def

presentationRelatorFinsetPresentedGroupEquivOfIsPrefixClosedQuotientSection

L974 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.presentationRelatorFinsetPresentedGroupEquivOfIsPrefixClosedQuotientSection

Documentation

Under the prefix-closed quotient-section hypothesis, replacing the presentation relator set by its finite relator finset preserves the presented group.

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 presentationRelatorFinsetPresentedGroupEquivOfIsPrefixClosedQuotientSection
    [Fintype X]
    (R : Finset (FreeGroup X))
    (hR : Subgroup.normalClosure ({r | r ∈ R} : Set (FreeGroup X)) ≤ D.kernel)
    (hprefix : D.IsPrefixClosedQuotientSection) :
    PresentedGroup
        ({z | z ∈ D.presentationRelatorFinset R} :
          Set (FreeGroup (FiniteSchreierSymbol X Q))) ≃*
      D.kernel ⧸ D.relatorSubgroup ({r | r ∈ R} : Set (FreeGroup X))

theorem

symbolEvalPresentationQuotientHom_surjective

L996 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalPresentationQuotientHom_surjective

Documentation

The raw presentation evaluation quotient map is surjective.

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 symbolEvalPresentationQuotientHom_surjective
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    Function.Surjective (D.symbolEvalPresentationQuotientHom hR)

theorem

symbolEvalAugmentedPresentationQuotientHom_surjective

L1006 ↗

ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.symbolEvalAugmentedPresentationQuotientHom_surjective

Documentation

The augmented-presentation evaluation quotient map is surjective.

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 symbolEvalAugmentedPresentationQuotientHom_surjective
    {R : Set (FreeGroup X)}
    (hR : Subgroup.normalClosure R ≤ D.kernel) :
    Function.Surjective (D.symbolEvalAugmentedPresentationQuotientHom hR)

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Presentation

Declarations