FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.SourceSubgroup

10 Theorem

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

Theorem FenchelNielsen.SecondStageCleanupPeriodData.periodOne_of_not_strict GitHub

theorem SecondStageCleanupPeriodData.periodOne_of_not_strict
    {σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
    {secondPrime : FirstKernelTailPrimeDivisorData D}
    (E : SecondStageCleanupPeriodData D secondPrime)
    (hNonStrict : ¬ (2 ≤ D.m₁' ∧ 2 ≤ D.m₂' ∧ 2 ≤ E.m₃')) :
    D.m₁' = 1 ∨ D.m₂' = 1 ∨ E.m₃' = 1

If the second-stage cleanup period data is not strict, one of the relevant periods is one.

Show proof

Theorem FenchelNielsen.originalFirstReduction_doublePeriodOne_sourceSubgroup_exists GitHub

private theorem originalFirstReduction_doublePeriodOne_sourceSubgroup_exists
    {tailLen p : ℕ} (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
    ∃ L : Subgroup
        (FuchsianPresentedGroup
          (originalFirstReductionSignature 1 1 tail hp (by norm_num) (by norm_num)
            htail hTailLen)),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 2

A source subgroup exists in the original first-reduction double-period-one case.

Show proof

Theorem FenchelNielsen.oneHeadPeriodOneTarget_sourceSubgroup_exists_by_tailPair GitHub

private theorem oneHeadPeriodOneTarget_sourceSubgroup_exists_by_tailPair
    {tailLen p : ℕ} (m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₂' : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
    (hTailLen : 0 < tailLen) :
    ∃ L : Subgroup
        (FuchsianPresentedGroup
          (oneHeadPeriodOneTargetSignature m₂' tail hp hm₂' htail hTailLen)),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 2

The one-head period-one target source subgroup exists from the tail-pair hypothesis.

Show proof

Theorem FenchelNielsen.firstReductionCanonicalTarget_periods_eq GitHub

private theorem firstReductionCanonicalTarget_periods_eq
    {tailLen p : ℕ}
    (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
    (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
    (x : FirstReductionIndex tailLen p) :
    (firstReductionCanonicalTargetSignature
        m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
      (firstReductionIndexEquivCanonicalTargetFin tailLen p x) =
        firstReductionPeriods (p := p) m₁' m₂' tail x

The first-reduction canonical target periods agree with the transported period data.

Show proof

Theorem FenchelNielsen.firstReductionCanonicalTarget_sourceSubgroup_exists_by_tailPair GitHub

private theorem firstReductionCanonicalTarget_sourceSubgroup_exists_by_tailPair
    {tailLen p : ℕ}
    (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
    (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
    ∃ L : Subgroup
        (FuchsianPresentedGroup
          (firstReductionCanonicalTargetSignature
            m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 2

The first-reduction target contains the required source subgroup in the tail-pair case.

Show proof

Theorem FenchelNielsen.firstReductionSourceSubgroup_leftPeriodOne_exists GitHub

theorem firstReductionSourceSubgroup_leftPeriodOne_exists
    {σ : FuchsianSignature}
    (D : FirstReductionPeriodData σ)
    (hm₁' : D.m₁' = 1) :
    ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 3

A source subgroup exists in the left period-one first-reduction case.

Show proof

Theorem FenchelNielsen.firstReductionSourceSubgroup_rightPeriodOne_exists GitHub

theorem firstReductionSourceSubgroup_rightPeriodOne_exists
    {σ : FuchsianSignature}
    (D : FirstReductionPeriodData σ)
    (hm₂' : D.m₂' = 1) :
    ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 3

A source subgroup exists in the right period-one first-reduction case.

Show proof

Theorem FenchelNielsen.SecondStageCleanupPeriodData.sourceSubgroup_exists_of_tailPair GitHub

private theorem SecondStageCleanupPeriodData.sourceSubgroup_exists_of_tailPair
    {σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
    {secondPrime : FirstKernelTailPrimeDivisorData D}
    (E : SecondStageCleanupPeriodData D secondPrime)
    (hm₁' : 2 ≤ D.m₁') (hm₂' : 2 ≤ D.m₂') :
    ∃ L : Subgroup (FuchsianPresentedGroup E.sourceSignature),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 3

The second-stage cleanup period data supplies a source subgroup from the tail-pair hypothesis.

Show proof

Theorem FenchelNielsen.firstReductionSourceSubgroup_tailPrimeQuotientOne_exists GitHub

theorem firstReductionSourceSubgroup_tailPrimeQuotientOne_exists
    {σ : FuchsianSignature}
    (D : FirstReductionPeriodData σ)
    (_hquot : D.tail D.tailPrimeDivisorData.k / D.tailPrimeDivisorData.q = 1) :
    ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 3

In the tail-prime quotient-one case, the first-reduction source subgroup exists with the required quotient data.

Show proof

Theorem FenchelNielsen.SecondStageCleanupPeriodData.sourceSubgroup_exists_of_canonicalReductions GitHub

theorem SecondStageCleanupPeriodData.sourceSubgroup_exists_of_canonicalReductions
    {σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
    {secondPrime : FirstKernelTailPrimeDivisorData D}
    (E : SecondStageCleanupPeriodData D secondPrime)
    (hm₁' : 2 ≤ D.m₁') (hm₂' : 2 ≤ D.m₂') (hm₃' : 2 ≤ E.m₃') :
    ∃ L : Subgroup (FuchsianPresentedGroup E.sourceSignature),
      L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
        SubgroupQuotientHasDerivedLengthAtMost L 3

Source-subgroup form of the strict two-stage branch. This is the form actually needed before the final mathematical normal core is taken: the two cyclic extensions only require finite-index torsion-free source subgroups, not local normality.

Show proof

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.SourceSubgroup

Declarations