ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

13 Theorems | 2 Definitions | 1 Instance

This module defines full and partial right Schreier transversals in free groups, proves their complement and prefix-closure properties, and supplies the existence and extension results used later.

imports

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

Imported by

Definition ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal

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

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

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal.one_mem

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightSchreierTransversal.prefix_closed

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightPartialSchreierTransversal.one_mem

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightPartialSchreierTransversal.prefix_closed

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.IsRightPartialSchreierTransversal.eq_of_rightQuotient_eq

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.prefixParent_mem_of_partial

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.chain_sUnion_isRightPartialSchreierTransversal

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.exists_rightSchreierTransversal_of_partial

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.exists_rightSchreierTransversal

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.generatorPower_sub_mem_of_rightQuotient_eq

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 Lean proof

Theorem ReidemeisterSchreier.Discrete.OpenSubgroups.isRightPartialSchreierTransversal_generatorPowers_of_minimalPower

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 Lean proof

Instance ReidemeisterSchreier.Discrete.OpenSubgroups.rightCosetLeftMulActionByInverse

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

@[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 of the corresponding rewriting map.

Show Lean proof

ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Transversals

Declarations