Yamaguchi Lean 4 Library
ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.ClassicalGeneratorBasis
ProCGroups/ReidemeisterSchreier/Discrete/OpenSubgroups/ClassicalGeneratorBasis

ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.ClassicalGeneratorBasis

2 Theorems | 1 Definition

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.

import
Imported by

Declarations

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal.exists_schreierBasisEquiv 
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)

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.

Show Lean proof
Definition ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGeneratorInverseBasisEquiv 
noncomputable 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 :=
  Classical.choose (Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT)

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.

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGeneratorInverseBasisEquiv_of 
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)⁻¹

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

Show Lean proof