FenchelNielsenZomorrodian.Discrete.MainTheorem
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
theorem threeStep_sourceSubgroup_exists_of_zeroGenus_periodData
(σ : FuchsianSignature)
(hZero : σ.orbitGenus = 0)
(D : FirstReductionPeriodData σ) :
∃ L : Subgroup (FuchsianPresentedGroup σ),
L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
SubgroupQuotientHasDerivedLengthAtMost L 3Zero-genus compact three-step construction from explicit period data. This is the proof-carrying discrete main theorem used by the profinite bridge. It avoids re-running the perfectness-to-period-data conversion when the profinite side has already produced the required shared-prime pair.
Show proof
by
classical
let secondPrime : FirstKernelTailPrimeDivisorData D := D.tailPrimeDivisorData
let E : SecondStageCleanupPeriodData D secondPrime :=
secondStageCleanupPeriodDataOfTailPrime D secondPrime
let sourceEquiv₀ :
FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup D.sourceSignature :=
Classical.choice (firstReductionSourceMulEquiv_exists D hZero)
by_cases hStrict : 2 ≤ D.m₁' ∧ 2 ≤ D.m₂' ∧ 2 ≤ E.m₃'
· have hStrictSubgroup :
∃ L : Subgroup (FuchsianPresentedGroup E.sourceSignature),
L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
SubgroupQuotientHasDerivedLengthAtMost L 3 :=
E.sourceSubgroup_exists_of_canonicalReductions
hStrict.1 hStrict.2.1 hStrict.2.2
let sourceEquiv₁ :
FuchsianPresentedGroup D.sourceSignature ≃*
FuchsianPresentedGroup E.sourceSignature :=
Classical.choice (secondStageCleanupSourceMulEquiv_exists E)
let sourceEquiv :
FuchsianPresentedGroup σ ≃* FuchsianPresentedGroup E.sourceSignature :=
sourceEquiv₀.trans sourceEquiv₁
exact sourceSubgroup_exists_of_mulEquiv sourceEquiv hStrictSubgroup
· have hPeriodOne :
D.m₁' = 1 ∨ D.m₂' = 1 ∨ E.m₃' = 1 :=
E.periodOne_of_not_strict hStrict
have hSubgroup :
∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
SubgroupQuotientHasDerivedLengthAtMost L 3 := by
rcases hPeriodOne with hm₁' | hm₂' | hm₃'
· exact
firstReductionSourceSubgroup_leftPeriodOne_exists
D hm₁'
· exact
firstReductionSourceSubgroup_rightPeriodOne_exists
D hm₂'
· have hquot : D.tail secondPrime.k / secondPrime.q = 1 := by
simpa [E, secondStageCleanupPeriodDataOfTailPrime] using hm₃'
exact
firstReductionSourceSubgroup_tailPrimeQuotientOne_exists
D (by simpa [secondPrime] using hquot)
exact sourceSubgroup_exists_of_mulEquiv sourceEquiv₀ hSubgroupProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□