FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.CleanupData
This module studies cleanup data for fenchel nielsen zomorrodian. The transported second-reduction index set has cardinality at least three. Every transported second-reduction period is at least \(2\).
import
private theorem secondReductionTransportIndex_card_ge_three
{tailLen p q : ℕ} (hq : 2 ≤ q) :
3 ≤ Fintype.card (SecondReductionTransportIndex tailLen p q)The transported second-reduction index set has cardinality at least three.
Show proof
by
have hcard :
Fintype.card (SecondReductionTransportIndex tailLen p q) =
2 * q + 2 + q * (p - 2) + tailLen * p * q := by
simp only [SecondReductionTransportIndex, secondReductionSourceCycleCount, Fintype.card_sigma,
Fintype.card_fin, Fintype.sum_sum_type, Finset.sum_const, Finset.card_univ, smul_eq_mul, Nat.mul_comm, mul_one,
Fintype.card_prod, Nat.mul_left_comm, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
rw [hcard]
omegaProof. 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.
□private theorem secondReductionTransportPeriods_ge_two
{tailLen p q : ℕ} (hq : 2 ≤ q)
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
(hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃') (htail : ∀ j, 2 ≤ tail j)
(x : SecondReductionTransportIndex tailLen p q) :
2 ≤ secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail xEvery transported second-reduction period is at least \(2\).
Show proof
by
rcases x with ⟨i, k⟩
cases i with
| inl i =>
fin_cases i
· simpa [secondReductionTransportPeriods, secondReductionSourceTransportPeriods, twoPeriods]
using hm₁'
· simpa [secondReductionTransportPeriods, secondReductionSourceTransportPeriods, twoPeriods]
using hm₂'
| inr s =>
cases s with
| inl j =>
fin_cases j
· simpa [secondReductionTransportPeriods, secondReductionSourceTransportPeriods]
using hm₃'
· simpa [secondReductionTransportPeriods, secondReductionSourceTransportPeriods]
using hm₃'
| inr s =>
cases s with
| inl j =>
exact le_trans hq
(Nat.le_mul_of_pos_right q (lt_of_lt_of_le (by decide : 0 < 2) hm₃'))
| inr jk =>
simpa [secondReductionTransportPeriods, secondReductionSourceTransportPeriods]
using htail jk.1Proof. Unfold the constructed period family and reduce each entry to either an original elliptic period or the selected prime-period entry. The original period hypotheses give positivity and the lower bound for nontrivial periods, and reindexing or transport preserves those inequalities.
□noncomputable def secondReductionTransportSignature
{tailLen p q : ℕ} (hq : 2 ≤ q)
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
(hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃') (htail : ∀ j, 2 ≤ tail j) :
FuchsianSignature :=
familyFuchsianSignature
(secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail)
(secondReductionTransportPeriods_ge_two hq m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
(secondReductionTransportIndex_card_ge_three hq)The transported signature used in the second reduction.
theorem secondReductionTransportSignature_lcmCondition
{tailLen p q : ℕ} (hq : 2 ≤ q)
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
(hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃') (htail : ∀ j, 2 ≤ tail j) :
LCMCondition
(secondReductionTransportSignature (p := p) hq m₁' m₂' m₃' tail
hm₁' hm₂' hm₃' htail).toFenchelSignatureThe transported second-reduction signature satisfies the LCM condition.
Show proof
by
simpa [secondReductionTransportSignature] using
familyFuchsianSignature_lcmCondition_of_lcmConditionFamily
(secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail)
(secondReductionTransportPeriods_ge_two hq m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
(secondReductionTransportIndex_card_ge_three hq)
(lcmConditionFamily_of_hasEqualPartnerFamily
(secondReductionTransport_hasEqualPartnerFamily hq m₁' m₂' m₃' tail))Proof. 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. 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.
□private theorem secondReductionSourcePeriods_pos
{tailLen p q : ℕ} (hq : 2 ≤ q)
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
(hm₁' : 0 < m₁') (hm₂' : 0 < m₂') (hm₃' : 0 < m₃')
(htail : ∀ j, 0 < tail j) :
∀ i : SecondReductionSourceIndex tailLen p, 0 < secondReductionSourcePeriods
(p := p) (q := q) m₁' m₂' m₃' tail iEvery entry in the second-reduction source period family is positive.
Show proof
by
intro i
cases i with
| inl h =>
fin_cases h <;> simpa [secondReductionSourcePeriods, twoPeriods]
| inr rest =>
cases rest with
| inl _ =>
exact Nat.mul_pos (lt_of_lt_of_le (by decide : 0 < 2) hq) hm₃'
| inr rest =>
cases rest with
| inl _ =>
exact Nat.mul_pos (lt_of_lt_of_le (by decide : 0 < 2) hq) hm₃'
| inr jk =>
exact htail jk.1Proof. Unfold the constructed period family and reduce each entry to either an original elliptic period or the selected prime-period entry. The original period hypotheses give positivity and the lower bound for nontrivial periods, and reindexing or transport preserves those inequalities.
□theorem secondReductionSource_nonOne_periods_ge_two
{tailLen p q : ℕ} (hq : 2 ≤ q)
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
(hm₁' : 0 < m₁') (hm₂' : 0 < m₂') (hm₃' : 0 < m₃')
(htail : ∀ j, 0 < tail j) :
∀ i : NonOneSubfamilyIndex
(secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail),
2 ≤ nonOneSubfamilyPeriods
(secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail) iEvery nontrivial period in the second-reduction source family is at least \(2\).
Show proof
nonOneSubfamilyPeriods_ge_two
(secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail)
(secondReductionSourcePeriods_pos hq m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)Proof. Unfold the constructed period family and reduce each entry to either an original elliptic period or the selected prime-period entry. The original period hypotheses give positivity and the lower bound for nontrivial periods, and reindexing or transport preserves those inequalities.
□def firstReductionTailIncludingThird
{tailLen q : ℕ} (m₃' : ℕ) (tail : Fin tailLen → ℕ) :
Fin (tailLen + 1) → ℕ :=
Fin.cases (q * m₃') tailThe first-reduction tail includes the third period entry.
theorem firstReductionTailIncludingThird_ge_two_of_pos
{tailLen q : ℕ} (hq : 2 ≤ q) (m₃' : ℕ) (tail : Fin tailLen → ℕ)
(hm₃' : 0 < m₃') (htail : ∀ j, 2 ≤ tail j) :
∀ j : Fin (tailLen + 1), 2 ≤ firstReductionTailIncludingThird (q := q) m₃' tail jThe first-reduction positivity construction gives the required lower bound for the associated period or index.
Show proof
by
intro j
refine Fin.cases ?_ (fun k => htail k) j
exact le_trans hq (Nat.le_mul_of_pos_right q hm₃')Proof. Unfold the constructed period family and reduce each entry to either an original elliptic period or the selected prime-period entry. The original period hypotheses give positivity and the lower bound for nontrivial periods, and reindexing or transport preserves those inequalities.
□noncomputable def finHeadInsertionEquiv {n : ℕ} (k : Fin (n + 1)) :
Fin (n + 1) ≃ Fin (n + 1) :=
Equiv.ofBijective (Fin.cases k k.succAbove) <| by
constructor
· intro a b h
cases a using Fin.cases with
| zero =>
cases b using Fin.cases with
| zero => rfl
| succ j =>
exfalso
exact Fin.ne_succAbove k j h
| succ i =>
cases b using Fin.cases with
| zero =>
exfalso
exact Fin.succAbove_ne k i h
| succ j =>
exact congrArg Fin.succ (Fin.succAbove_right_inj.mp h)
· intro y
rcases Fin.eq_self_or_eq_succAbove k y with rfl | ⟨j, rfl⟩
· exact ⟨0, rfl⟩
· exact ⟨j.succ, rfl⟩Equivalence inserting a distinguished head index into a finite index type.
noncomputable def twoPointSubtypeEquiv {ι : Type*} [DecidableEq ι]
(i j : ι) (hij : i ≠ j) : Fin 2 ≃ {k : ι // k = i ∨ k = j} where
toFun k :=
match k with
| ⟨0, _⟩ => ⟨i, Or.inl rfl⟩
| ⟨1, _⟩ => ⟨j, Or.inr rfl⟩
| ⟨n + 2, h⟩ => by omega
invFun k := if _h : (k : ι) = i then 0 else 1
left_inv := by
intro k
fin_cases k
· simp only [↓reduceDIte, Fin.isValue, Fin.zero_eta]
· simp only [hij.symm, ↓reduceDIte, Fin.isValue, Fin.mk_one]
right_inv := by
intro k
apply Subtype.ext
rcases k with ⟨k, hk | hk⟩
· subst hk
simp only [↓reduceDIte, Fin.isValue]
· subst hk
simp only [hij.symm, ↓reduceDIte, Fin.isValue]noncomputable def notTwoSubtypeEquiv {ι : Type*}
(i j : ι) : {k : ι // k ≠ i ∧ k ≠ j} ≃ {k : ι // ¬ (k = i ∨ k = j)} :=
Equiv.subtypeEquivRight (fun _ => by simp only [ne_eq, not_or])Equivalence between the complement of the two distinguished points and the remaining finite index type.
noncomputable def originalFirstReductionReindex
{ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) :
OriginalFirstReductionIndex (Fintype.card {k : ι // k ≠ i ∧ k ≠ j}) ≃ ι :=
(Equiv.sumCongr
(twoPointSubtypeEquiv i j hij)
((Fintype.equivFin {k : ι // k ≠ i ∧ k ≠ j}).symm.trans
(notTwoSubtypeEquiv i j))).trans
(Equiv.sumCompl (fun k : ι => k = i ∨ k = j))The reindexing map for the original first-reduction period family.
@[simp 900] theorem originalFirstReductionReindex_left_zero
{ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) :
originalFirstReductionReindex i j hij (.inl 0) = iThe original first-reduction reindexing sends the left zero index to its prescribed target.
Show proof
by
simp only [ne_eq, originalFirstReductionReindex, twoPointSubtypeEquiv, Fin.isValue, dite_eq_ite,
Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_fn_mk, Equiv.coe_trans, Sum.map_inl, Equiv.sumCompl_apply_inl]Proof. 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. 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.
□@[simp 900] theorem originalFirstReductionReindex_left_one
{ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) :
originalFirstReductionReindex i j hij (.inl 1) = jThe original first-reduction reindexing sends the left one index to its prescribed target.
Show proof
by
simp only [ne_eq, originalFirstReductionReindex, twoPointSubtypeEquiv, Fin.isValue, dite_eq_ite,
Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_fn_mk, Equiv.coe_trans, Sum.map_inl, Equiv.sumCompl_apply_inl]Proof. 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. 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.
□@[simp 900] theorem originalFirstReductionReindex_right
{ι : Type*} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j)
(k : Fin (Fintype.card {k : ι // k ≠ i ∧ k ≠ j})) :
originalFirstReductionReindex i j hij (.inr k) =
((Fintype.equivFin {k : ι // k ≠ i ∧ k ≠ j}).symm k :
{k : ι // k ≠ i ∧ k ≠ j}).1The original first-reduction reindexing sends the right-side index to its prescribed target.
Show proof
by
simp only [ne_eq, originalFirstReductionReindex, notTwoSubtypeEquiv, Equiv.trans_apply, Equiv.sumCongr_apply,
Equiv.coe_trans, Sum.map_inr, Function.comp_apply, Equiv.sumCompl_apply_inr, Equiv.subtypeEquivRight_apply_coe]Proof. 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. 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.
□structure FirstReductionPeriodData (σ : FuchsianSignature) where
p : ℕ
hpPrime : p.Prime
hp : 2 ≤ p
tailLen : ℕ
m₁' : ℕ
m₂' : ℕ
tail : Fin tailLen → ℕ
hm₁' : 0 < m₁'
hm₂' : 0 < m₂'
htail : ∀ j, 2 ≤ tail j
hTailLen : 0 < tailLen
reindex : OriginalFirstReductionIndex tailLen ≃ Fin σ.numPeriods
periods_eq :
∀ x, originalFirstReductionPeriods (p := p) m₁' m₂' tail x = σ.periods (reindex x)The period-data package used for the first zero-genus reduction.
noncomputable def firstReductionPeriodDataOfPrimePair
(σ : FuchsianSignature) {p : ℕ} (hpPrime : p.Prime)
{i j : Fin σ.numPeriods} (hij : i ≠ j)
(hpi : p ∣ σ.periods i) (hpj : p ∣ σ.periods j) :
FirstReductionPeriodData σ := by
classical
let tailSubtype := {k : Fin σ.numPeriods // k ≠ i ∧ k ≠ j}
let tailLen := Fintype.card tailSubtype
let tailEquiv : Fin tailLen ≃ tailSubtype := (Fintype.equivFin tailSubtype).symm
let tail : Fin tailLen → ℕ := fun k => σ.periods ((tailEquiv k).1)
have hpPos : 0 < p := hpPrime.pos
have hpi_period_pos : 0 < σ.periods i :=
lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two i)
have hpj_period_pos : 0 < σ.periods j :=
lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two j)
have hm₁pos : 0 < σ.periods i / p :=
Nat.div_pos (Nat.le_of_dvd hpi_period_pos hpi) hpPos
have hm₂pos : 0 < σ.periods j / p :=
Nat.div_pos (Nat.le_of_dvd hpj_period_pos hpj) hpPos
have hmul₁ : p * (σ.periods i / p) = σ.periods i := by
rw [Nat.mul_comm]
exact Nat.div_mul_cancel hpi
have hmul₂ : p * (σ.periods j / p) = σ.periods j := by
rw [Nat.mul_comm]
exact Nat.div_mul_cancel hpj
have htailLen : 0 < tailLen := by
have hcard0 := Fintype.card_congr (originalFirstReductionReindex i j hij)
have hcard : 2 + tailLen = σ.numPeriods := by
simpa [OriginalFirstReductionIndex, tailLen] using hcard0
have hsig : 3 ≤ σ.numPeriods := σ.numPeriods_ge_three
omega
exact
{ p := p
hpPrime := hpPrime
hp := hpPrime.two_le
tailLen := tailLen
m₁' := σ.periods i / p
m₂' := σ.periods j / p
tail := tail
hm₁' := hm₁pos
hm₂' := hm₂pos
htail := by
intro k
exact σ.period_ge_two ((tailEquiv k).1)
hTailLen := htailLen
reindex := originalFirstReductionReindex i j hij
periods_eq := by
intro x
cases x using Sum.casesOn with
| inl a =>
fin_cases a
· simpa [originalFirstReductionPeriods, twoPeriods,
originalFirstReductionReindex_left_zero] using hmul₁
· simpa [originalFirstReductionPeriods, twoPeriods,
originalFirstReductionReindex_left_one] using hmul₂
| inr k =>
change σ.periods ((tailEquiv k).1) =
σ.periods (originalFirstReductionReindex i j hij (.inr k))
rw [originalFirstReductionReindex_right] }The first-reduction period data attached to the chosen prime pair.
noncomputable def FirstReductionPeriodData.sourceSignature
{σ : FuchsianSignature} (D : FirstReductionPeriodData σ) : FuchsianSignature :=
originalFirstReductionSignature D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail
D.hTailLenThe source signature determined by the first-reduction period data.