ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

13 Theorem | 2 Definition | 1 Instance

This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.

Open this file on GitHub

import

Mathlib.GroupTheory.Schreier
ReidemeisterSchreier.Discrete.OpenSubgroups.Words.Basic

Imported by

Definition ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal GitHub

def IsRightSchreierTransversal {X : Type u} [DecidableEq X]
    (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop :=
  Subgroup.IsComplement (L : Set (FreeGroup X)) T ∧
    (1 : FreeGroup X) ∈ T ∧
      ∀ ⦃t : FreeGroup X⦄, t ∈ T → freeGroupInitialSegments t ⊆ T

A right Schreier transversal is a right transversal containing every initial segment of each of its elements.

Definition ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightPartialSchreierTransversal GitHub

def IsRightPartialSchreierTransversal {X : Type u} [DecidableEq X]
    (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop :=
  (1 : FreeGroup X) ∈ T ∧
    (∀ ⦃t : FreeGroup X⦄, t ∈ T → freeGroupInitialSegments t ⊆ T) ∧
      ∀ ⦃a b : FreeGroup X⦄, a ∈ T → b ∈ T →
        (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
          Quotient.mk'' b → a = b

A right partial Schreier transversal is prefix-closed, contains 1, and meets each right coset in at most one element.

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal.isComplement GitHub

theorem IsRightSchreierTransversal.isComplement {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Subgroup.IsComplement (L : Set (FreeGroup X)) T

A right Schreier transversal gives the required complement to the subgroup action.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal.one_mem GitHub

theorem IsRightSchreierTransversal.one_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    (1 : FreeGroup X) ∈ T

A right Schreier transversal contains the identity word.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal.prefix_closed GitHub

theorem IsRightSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
    freeGroupInitialSegments t ⊆ T

A right Schreier transversal is closed under initial segments.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightPartialSchreierTransversal.one_mem GitHub

theorem IsRightPartialSchreierTransversal.one_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T) :
    (1 : FreeGroup X) ∈ T

A right partial Schreier transversal contains the identity word.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightPartialSchreierTransversal.prefix_closed GitHub

theorem IsRightPartialSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
    freeGroupInitialSegments t ⊆ T

A right partial Schreier transversal is closed under initial segments.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightPartialSchreierTransversal.eq_of_rightQuotient_eq GitHub

theorem IsRightPartialSchreierTransversal.eq_of_rightQuotient_eq
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T)
    {a b : FreeGroup X} (ha : a ∈ T) (hb : b ∈ T)
    (hEq :
      (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
        Quotient.mk'' b) :
    a = b

Two right Schreier transversal representatives are equal when their right quotients agree.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.prefixParent_mem_of_partial GitHub

theorem prefixParent_mem_of_partial {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
    FreeGroup.prefixParent t ∈ T

The prefix parent of a partial Schreier word satisfies the required membership condition.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.chain_sUnion_isRightPartialSchreierTransversal GitHub

theorem chain_sUnion_isRightPartialSchreierTransversal
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {c : Set (Set (FreeGroup X))}
    (hcn : c.Nonempty)
    (hc :
      ∀ ⦃s⦄, s ∈ c → ∀ ⦃t⦄, t ∈ c → s ≠ t → s ⊆ t ∨ t ⊆ s)
    (hcPartial :
      ∀ ⦃s⦄, s ∈ c → IsRightPartialSchreierTransversal (X := X) L s) :
    IsRightPartialSchreierTransversal (X := X) L (⋃₀ c)

A nonempty chain of right partial Schreier transversals has a union that is again a right partial Schreier transversal. This is the chain-upper-bound step used in the Zorn construction.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.exists_rightSchreierTransversal_of_partial GitHub

theorem exists_rightSchreierTransversal_of_partial {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T₀ : Set (FreeGroup X)}
    (hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀) :
    ∃ T : Set (FreeGroup X), T₀ ⊆ T ∧ IsRightSchreierTransversal (X := X) L T

Every right partial Schreier transversal extends to a full right Schreier transversal.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.exists_rightSchreierTransversal GitHub

theorem exists_rightSchreierTransversal {X : Type u} [DecidableEq X]
    (L : Subgroup (FreeGroup X)) :
    ∃ T : Set (FreeGroup X), IsRightSchreierTransversal (X := X) L T

Every subgroup of a free group admits a right Schreier transversal.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.generatorPower_sub_mem_of_rightQuotient_eq GitHub

theorem generatorPower_sub_mem_of_rightQuotient_eq {X : Type u}
    {L : Subgroup (FreeGroup X)} (x : X) {m n : ℕ} (hmn : m ≤ n)
    (hEq :
      (Quotient.mk'' ((FreeGroup.of x) ^ m) : Quotient (QuotientGroup.rightRel L)) =
        Quotient.mk'' ((FreeGroup.of x) ^ n)) :
    (FreeGroup.of x) ^ (n - m) ∈ L

If two generator powers determine the same right quotient, their difference lies in the subgroup.

Show proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.isRightPartialSchreierTransversal_generatorPowers_of_minimalPower GitHub

theorem isRightPartialSchreierTransversal_generatorPowers_of_minimalPower
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} (x : X) {N : ℕ}
    (hN : 0 < N)
    (hmin : ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ L) :
    IsRightPartialSchreierTransversal (X := X) L
      (Set.range fun i : Fin N => (FreeGroup.of x) ^ (i : ℕ))

The representatives built from minimal generator powers form a right partial Schreier transversal.

Show proof

Instance ReidemeisterSchreier.Discrete.OpenSubgroups.rightCosetLeftMulActionByInverse GitHub

instance rightCosetLeftMulActionByInverse {X : Type u} (L : Subgroup (FreeGroup X)) :
    MulAction (FreeGroup X) (Quotient (QuotientGroup.rightRel L)) where
  smul g :=
    Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
      rw [QuotientGroup.rightRel_apply] at hab ⊢
      simpa [mul_assoc] using hab
  one_smul q := by
    refine Quotient.inductionOn' q ?_
    intro a
    apply Quotient.sound'
    rw [QuotientGroup.rightRel_apply]
    simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
  mul_smul g h q := by
    refine Quotient.inductionOn' q ?_
    intro a
    apply Quotient.sound'
    rw [QuotientGroup.rightRel_apply]
    simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]

Right multiplication on right cosets, expressed as a left action via \(g \cdot [t] = [t * g{}^{-1}]\). This is the action naturally compatible with Schreier generators of the form \(t x (\widetilde{t x}){}^{-1}\).

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.rightCosetLeftMulActionByInverse_mk_smul GitHub

@[simp] theorem rightCosetLeftMulActionByInverse_mk_smul {X : Type u}
    (L : Subgroup (FreeGroup X)) (g a : FreeGroup X) :
    g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
      Quotient.mk'' (a * g⁻¹)

The Schreier generator component used in the corresponding rewriting calculation.

Show proof

ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

Declarations