Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian.Discrete.FiniteIndex.Definitions
FenchelNielsenZomorrodian/Discrete/FiniteIndex/Definitions

FenchelNielsenZomorrodian.Discrete.FiniteIndex.Definitions

2 Theorem | 3 Definition

This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.

Open this file on GitHub
import
Imported by

Declarations

Definition FenchelNielsen.SubgroupQuotientHasDerivedLengthAtMost GitHub 
def SubgroupQuotientHasDerivedLengthAtMost {G : Type*} [Group G]
    (H : Subgroup G) (m : ℕ) : Prop :=
  derivedSeries G m ≤ H

The predicate records that the quotient attached to the subgroup has derived length at most the given bound.

Definition FenchelNielsen.HasFiniteIndexTorsionFreeNormalSubgroupWithDerivedLengthAtMost GitHub 
def HasFiniteIndexTorsionFreeNormalSubgroupWithDerivedLengthAtMost
    (G : Type*) [Group G] (m : ℕ) : Prop :=
  ∃ H : Subgroup G,
    H.FiniteIndex ∧ H.Normal ∧ IsTorsionFreeGroup H ∧
      SubgroupQuotientHasDerivedLengthAtMost H m

The predicate records the existence of a finite-index torsion-free normal subgroup whose derived length is bounded by the given parameter.

Definition FenchelNielsen.HasFiniteIndexTorsionFreeSubgroupWithDerivedLengthAtMost GitHub 
def HasFiniteIndexTorsionFreeSubgroupWithDerivedLengthAtMost
    (G : Type*) [Group G] (m : ℕ) : Prop :=
  ∃ H : Subgroup G,
    H.FiniteIndex ∧ IsTorsionFreeGroup H ∧
      SubgroupQuotientHasDerivedLengthAtMost H m

The predicate records the existence of a finite-index torsion-free subgroup whose derived length is bounded by the given parameter.

Theorem FenchelNielsen.subgroupQuotientHasDerivedLengthAtMost_mono GitHub 
theorem subgroupQuotientHasDerivedLengthAtMost_mono
    {G : Type*} [Group G] {H : Subgroup G} {m n : ℕ}
    (hmn : m ≤ n)
    (h : SubgroupQuotientHasDerivedLengthAtMost H m) :
    SubgroupQuotientHasDerivedLengthAtMost H n

The subgroup-quotient derived-length condition is monotone in the length bound.

Show proof
Theorem FenchelNielsen.hasFiniteIndexTorsionFreeSubgroupWithDerivedLengthAtMost_mono GitHub 
theorem hasFiniteIndexTorsionFreeSubgroupWithDerivedLengthAtMost_mono
    {G : Type*} [Group G] {m n : ℕ} (hmn : m ≤ n)
    (h : HasFiniteIndexTorsionFreeSubgroupWithDerivedLengthAtMost G m) :
    HasFiniteIndexTorsionFreeSubgroupWithDerivedLengthAtMost G n

The finite-index torsion-free subgroup condition with quotient derived length at most \(m\) is monotone in the length bound.

Show proof