FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.Reductions
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.
structure FirstKernelTailPrimeDivisorData {σ : FuchsianSignature}
(D : FirstReductionPeriodData σ) where
q : ℕ
hqPrime : q.Prime
k : Fin D.tailLen
hqk : q ∣ D.tail k
hm₃pos : 0 < D.tail k / qData choosing a prime divisor of one tail period in the first-reduction kernel construction, together with the quotient period remaining positive.
noncomputable def FirstReductionPeriodData.tailPrimeDivisorData
{σ : FuchsianSignature} (D : FirstReductionPeriodData σ) :
FirstKernelTailPrimeDivisorData D := by
classical
let k : Fin D.tailLen := ⟨0, D.hTailLen⟩
have htail_ge : 2 ≤ D.tail k := D.htail k
have htail_pos : 0 < D.tail k := lt_of_lt_of_le (by decide : 0 < 2) htail_ge
have htail_ne_one : D.tail k ≠ 1 := by omega
let hqExists : ∃ q, q.Prime ∧ q ∣ D.tail k := Nat.exists_prime_and_dvd htail_ne_one
let q := Classical.choose hqExists
have hqPrime : q.Prime := (Classical.choose_spec hqExists).1
have hqk : q ∣ D.tail k := (Classical.choose_spec hqExists).2
exact
{ q := q
hqPrime := hqPrime
k := k
hqk := hqk
hm₃pos := Nat.div_pos (Nat.le_of_dvd htail_pos hqk) hqPrime.pos }Prime-divisor data selected from the tail periods for the first reduction.
structure SecondStageCleanupPeriodData
{σ : FuchsianSignature} (D : FirstReductionPeriodData σ)
(secondPrime : FirstKernelTailPrimeDivisorData D) where
tailLen : ℕ
m₃' : ℕ
tail : Fin tailLen → ℕ
hm₃' : 0 < m₃'
htail : ∀ j, 2 ≤ tail j
reindexTail : Fin (tailLen + 1) ≃ Fin D.tailLen
tail_eq :
∀ j, firstReductionTailIncludingThird (q := secondPrime.q) m₃' tail j =
D.tail (reindexTail j)Period data for the second-stage cleanup in the zero-genus reduction.
noncomputable def secondStageCleanupPeriodDataOfTailPrime
{σ : FuchsianSignature} (D : FirstReductionPeriodData σ)
(secondPrime : FirstKernelTailPrimeDivisorData D) :
SecondStageCleanupPeriodData D secondPrime := by
classical
let tailLen := D.tailLen - 1
have hLen : tailLen + 1 = D.tailLen := by
have hpos : 1 ≤ D.tailLen := Nat.succ_le_of_lt D.hTailLen
omega
let k' : Fin (tailLen + 1) := (finCongr hLen).symm secondPrime.k
let reindexTail : Fin (tailLen + 1) ≃ Fin D.tailLen :=
(finHeadInsertionEquiv k').trans (finCongr hLen)
let tail : Fin tailLen → ℕ := fun j => D.tail (reindexTail j.succ)
have hmul : secondPrime.q * (D.tail secondPrime.k / secondPrime.q) =
D.tail secondPrime.k := by
rw [Nat.mul_comm]
exact Nat.div_mul_cancel secondPrime.hqk
exact
{ tailLen := tailLen
m₃' := D.tail secondPrime.k / secondPrime.q
tail := tail
hm₃' := secondPrime.hm₃pos
htail := by
intro j
exact D.htail (reindexTail j.succ)
reindexTail := reindexTail
tail_eq := by
intro j
refine Fin.cases ?_ ?_ j
· change secondPrime.q * (D.tail secondPrime.k / secondPrime.q) =
D.tail (reindexTail 0)
simpa [reindexTail, k'] using hmul
· intro a
rfl }Second-stage cleanup period data constructed from the tail-prime divisor data.
noncomputable def SecondStageCleanupPeriodData.reindexSource
{σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
{secondPrime : FirstKernelTailPrimeDivisorData D}
(E : SecondStageCleanupPeriodData D secondPrime) :
OriginalFirstReductionIndex (E.tailLen + 1) ≃ OriginalFirstReductionIndex D.tailLen :=
Equiv.sumCongr (Equiv.refl (Fin 2)) E.reindexTailThe reindexed source signature for second-stage cleanup period data.
noncomputable def SecondStageCleanupPeriodData.sourceSignature
{σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
{secondPrime : FirstKernelTailPrimeDivisorData D}
(E : SecondStageCleanupPeriodData D secondPrime) :
FuchsianSignature :=
originalFirstReductionSignature D.m₁' D.m₂'
(firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
D.hp D.hm₁' D.hm₂'
(firstReductionTailIncludingThird_ge_two_of_pos
secondPrime.hqPrime.two_le E.m₃' E.tail E.hm₃' E.htail)
(Nat.succ_pos _)The source signature associated with second-stage cleanup period data.
theorem secondStageCleanupSourceMulEquiv_exists
{σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
{secondPrime : FirstKernelTailPrimeDivisorData D}
(E : SecondStageCleanupPeriodData D secondPrime) :
Nonempty (FuchsianPresentedGroup D.sourceSignature ≃*
FuchsianPresentedGroup E.sourceSignature)There is a multiplicative equivalence between the second-stage cleanup source presentation and its reindexed source presentation.
Show proof
by
refine
zeroGenusFuchsianPresentedGroupEquivOfIndexedPeriods D.sourceSignature E.sourceSignature
?_ ?_
(E.reindexSource.trans (originalFirstReductionOrderedIndexEquiv D.tailLen))
(originalFirstReductionOrderedIndexEquiv (E.tailLen + 1)) ?_
· rfl
· rfl
· intro x
cases x using Sum.casesOn with
| inl i =>
fin_cases i <;>
rfl
| inr j =>
have hD : 2 + (E.reindexTail j).val ≠ 1 := by omega
have hE : 2 + j.val ≠ 1 := by omega
simpa [SecondStageCleanupPeriodData.sourceSignature,
FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature,
originalFirstReductionSignaturePeriod, originalFirstReductionOrderedIndexEquiv,
originalFirstReductionPeriods, twoPeriods, SecondStageCleanupPeriodData.reindexSource,
hD, hE]
using (E.tail_eq j).symmProof. 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. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the 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.
□theorem SecondStageCleanupPeriodData.source_nonOne_periods_ge_two
{σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
{secondPrime : FirstKernelTailPrimeDivisorData D}
(E : SecondStageCleanupPeriodData D secondPrime) :
∀ i : NonOneSubfamilyIndex
(secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
D.m₁' D.m₂' E.m₃' E.tail),
2 ≤ nonOneSubfamilyPeriods
(secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
D.m₁' D.m₂' E.m₃' E.tail) iEvery nontrivial source period in the second-stage cleanup is at least \(2\).
Show proof
secondReductionSource_nonOne_periods_ge_two
secondPrime.hqPrime.two_le D.m₁' D.m₂' E.m₃' E.tail
D.hm₁' D.hm₂' E.hm₃'
(fun j => lt_of_lt_of_le (by decide : 0 < 2) (E.htail j))Proof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□theorem SecondStageCleanupPeriodData.source_nonOne_card_ge_three_of_firstHead
{σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
{secondPrime : FirstKernelTailPrimeDivisorData D}
(E : SecondStageCleanupPeriodData D secondPrime)
(hm₁ne : D.m₁' ≠ 1) :
3 ≤ Fintype.card
(NonOneSubfamilyIndex
(secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
D.m₁' D.m₂' E.m₃' E.tail))With a first-head source, the second-stage cleanup source has at least \(3\) nontrivial periods.
Show proof
by
let periods :=
secondReductionSourcePeriods (p := D.p) (q := secondPrime.q)
D.m₁' D.m₂' E.m₃' E.tail
have hqm_ne : secondPrime.q * E.m₃' ≠ 1 := by
have hqge : 2 ≤ secondPrime.q * E.m₃' :=
le_trans secondPrime.hqPrime.two_le
(Nat.le_mul_of_pos_right secondPrime.q E.hm₃')
omega
let f : Fin 3 → NonOneSubfamilyIndex periods := fun i =>
match i with
| ⟨0, _⟩ =>
⟨.inl 0, by
simpa [periods, secondReductionSourcePeriods, twoPeriods] using hm₁ne⟩
| ⟨1, _⟩ =>
⟨.inr (.inl 0), by
simpa [periods, secondReductionSourcePeriods] using hqm_ne⟩
| ⟨2, _⟩ =>
⟨.inr (.inl 1), by
simpa [periods, secondReductionSourcePeriods] using hqm_ne⟩
| ⟨n + 3, hn⟩ => False.elim (by omega)
have hf : Function.Injective f := by
intro a b h
fin_cases a <;> fin_cases b <;> first | rfl | cases h
simpa using Fintype.card_le_of_injective f hfProof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□