Module

ClassicalGeneratorBasis.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.ClassicalGeneratorBasis

4 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Open Subgroups / Classical Generator Basis

This module identifies the classical Schreier generators with the free basis obtained from complement edges, including the inverse-basis convention needed for the standard generator formula.

Imports1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis

Imported by1

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.All

theorem

exists_inverseSchreierBasisEquiv

L30 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv

Documentation

There is an inverse-valued Schreier-basis equivalence sending the standard free generator represented by \(z\) to \(z^{-1}\) in the subgroup; the positive-valued compatibility theorem is exposed separately.

Source context 4 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section ClassicalGeneratorBasis
namespace Internal

Lean source · statement

theorem IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    ∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
      ∀ z : ↥(schreierGeneratorSet (X := X) hT),
        e (FreeGroup.of z) = (z : L)⁻¹

theorem

exists_schreierBasisEquiv

L157 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal.exists_schreierBasisEquiv

Documentation

Positive-valued Schreier-basis existence statement on the classical Schreier generator set. It is equivalent to the nontrivial Schreier-pair basis equivalence used in the main formulation.

Source context 3 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section ClassicalGeneratorBasis

Lean source · statement

theorem IsRightSchreierTransversal.exists_schreierBasisEquiv
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    ∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
      ∀ z : ↥(schreierGeneratorSet (X := X) hT),
        e (FreeGroup.of z) = (z : L)

def

schreierGeneratorInverseBasisEquiv

L180 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGeneratorInverseBasisEquiv

Documentation

The inverse-valued free-group equivalence on the classical Schreier generator value set is equivalent to the nontrivial Schreier-pair basis equivalence used in the main formulation.

Source context 3 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section ClassicalGeneratorBasis

Lean source · statement

def schreierGeneratorInverseBasisEquiv
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L

theorem

schreierGeneratorInverseBasisEquiv_of

L190 ↗

ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGeneratorInverseBasisEquiv_of

Documentation

The inverse-valued classical generator-set equivalence sends a free generator to the inverse of the represented Schreier generator.

Source context 3 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section ClassicalGeneratorBasis

Lean source · statement

theorem schreierGeneratorInverseBasisEquiv_of
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (z : ↥(schreierGeneratorSet (X := X) hT)) :
    schreierGeneratorInverseBasisEquiv (X := X) hT (FreeGroup.of z) = (z : L)⁻¹

Module documentation

Reidemeister Schreier / Discrete / Open Subgroups / Classical Generator Basis

Declarations

exists_inverseSchreierBasisEquiv

exists_schreierBasisEquiv

schreierGeneratorInverseBasisEquiv

schreierGeneratorInverseBasisEquiv_of