FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.ActualTransport
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.
private theorem firstReductionIndex_card_ge_three
{tailLen p : ℕ} (hp : 2 ≤ p) (hTailLen : 0 < tailLen) :
3 ≤ Fintype.card (FirstReductionIndex tailLen p)The first-reduction index set has at least three elements in the canonical finite quotient data.
Show proof
by
simp only [FirstReductionIndex, Fintype.card_sum, Fintype.card_fin, Fintype.card_prod]
nlinarith [Nat.succ_le_iff.mpr hTailLen, hp]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. 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. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. 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.
□private theorem firstReductionPeriods_ge_two
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
(x : FirstReductionIndex tailLen p) :
2 ≤ firstReductionPeriods (p := p) m₁' m₂' tail xEvery period in the first-reduction period family is at least \(2\).
Show proof
by
cases x using Sum.casesOn <;> rename_i x
· fin_cases x
· simpa [firstReductionPeriods, twoPeriods] using hm₁'
· simpa [firstReductionPeriods, twoPeriods] using hm₂'
· simpa [firstReductionPeriods] using htail x.1Proof. Unfold the relevant period-family or signature definition and split on the finite index cases. Each branch reduces to the stored period entry or to the specified reindexing or transport map, so the displayed period value follows directly.
□noncomputable def firstReductionTransportSignature
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
FuchsianSignature :=
familyFuchsianSignature
(firstReductionPeriods (p := p) m₁' m₂' tail)
(firstReductionPeriods_ge_two m₁' m₂' tail hm₁' hm₂' htail)
(firstReductionIndex_card_ge_three hp hTailLen)def firstReductionTailSuccEquivFirstSecondTail
(tailLen p : ℕ) :
Fin (tailLen + 1) × Fin p ≃ Sum (Fin p) (Fin tailLen × Fin p) where
toFun jk :=
Fin.cases (motive := fun _ => Sum (Fin p) (Fin tailLen × Fin p))
(.inl jk.2)
(fun j => .inr (j, jk.2))
jk.1
invFun
| .inl k => (0, k)
| .inr jk => (jk.1.succ, jk.2)
left_inv := by
intro jk
rcases jk with ⟨j, k⟩
cases j using Fin.cases with
| zero => rfl
| succ j => rfl
right_inv := by
intro s
cases s with
| inl k => rfl
| inr jk =>
rcases jk with ⟨j, k⟩
rflThe named finite-index equivalence identifies the source and target index types used in the reduction step.
def firstReductionIndexSuccEquivFirstSecondInputIndex
(tailLen p : ℕ) :
FirstReductionIndex (tailLen + 1) p ≃ FirstSecondInputIndex tailLen p :=
Equiv.sumCongr (Equiv.refl (Fin 2))
(firstReductionTailSuccEquivFirstSecondTail tailLen p)The named finite-index equivalence identifies the source and target index types used in the reduction step.
def finTwoRestEquiv {p : ℕ} (hp : 2 ≤ p) : Fin p ≃ Sum (Fin 2) (Fin (p - 2)) :=
(finCongr (by omega : p = 2 + (p - 2))).trans finSumFinEquiv.symmThe named finite-index equivalence identifies the source and target index types used in the reduction step.
def firstSecondInputIndexEquivSecondReductionSourceIndex
{tailLen p : ℕ} (hp : 2 ≤ p) :
FirstSecondInputIndex tailLen p ≃ SecondReductionSourceIndex tailLen p :=
Equiv.sumCongr (Equiv.refl (Fin 2))
((Equiv.sumCongr (finTwoRestEquiv hp) (Equiv.refl (Fin tailLen × Fin p))).trans
(Equiv.sumAssoc (Fin 2) (Fin (p - 2)) (Fin tailLen × Fin p)))The finite-index equivalence reindexes the first-second input periods as the second-reduction source periods.
def firstReductionIndexSuccEquivSecondReductionSourceIndex
{tailLen p : ℕ} (hp : 2 ≤ p) :
FirstReductionIndex (tailLen + 1) p ≃ SecondReductionSourceIndex tailLen p :=
(firstReductionIndexSuccEquivFirstSecondInputIndex tailLen p).trans
(firstSecondInputIndexEquivSecondReductionSourceIndex hp)The named finite-index equivalence identifies the source and target index types used in the reduction step.
private theorem firstReductionTailIncludingThird_transportPeriods_reindexed
{tailLen p q : ℕ}
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) (hp : 2 ≤ p)
(x : FirstReductionIndex (tailLen + 1) p) :
firstReductionPeriods (p := p) m₁' m₂'
(firstReductionTailIncludingThird (q := q) m₃' tail) x =
secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail
(firstReductionIndexSuccEquivSecondReductionSourceIndex hp x)The transported tail-including-third period family agrees with the corresponding reindexing.
Show proof
by
cases x using Sum.casesOn <;> rename_i x
· fin_cases x <;> rfl
· rcases x with ⟨j, k⟩
cases j using Fin.cases with
| zero =>
change q * m₃' =
secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail
(firstSecondInputIndexEquivSecondReductionSourceIndex hp (.inr (.inl k)))
unfold firstSecondInputIndexEquivSecondReductionSourceIndex
cases h : finTwoRestEquiv hp k with
| inl i =>
simp only [secondReductionSourcePeriods, Equiv.sumCongr_apply, Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr,
Function.comp_apply, Sum.map_inl, h, Equiv.sumAssoc_apply_inl_inl]
| inr i =>
simp only [secondReductionSourcePeriods, Equiv.sumCongr_apply, Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr,
Function.comp_apply, Sum.map_inl, h, Equiv.sumAssoc_apply_inl_inr]
| succ j =>
rflProof. Unfold the relevant period-family or signature definition and split on the finite index cases. Each branch reduces to the stored period entry or to the specified reindexing or transport map, so the displayed period value follows directly.
□theorem firstReductionTransportSignature_mulEquiv_secondReductionSourceSignature_exists
{tailLen p q : ℕ}
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hq : 2 ≤ q)
(hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 0 < m₃')
(htail : ∀ j, 2 ≤ tail j) :
Nonempty
(FuchsianPresentedGroup
(firstReductionTransportSignature m₁' m₂'
(firstReductionTailIncludingThird (q := q) m₃' tail)
hp hm₁' hm₂'
(firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
(Nat.succ_pos _))
≃*
FuchsianPresentedGroup
(secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
hm₃' htail))There is a multiplicative equivalence between the first-reduction transport signature and the second-reduction source signature.
Show proof
by
classical
refine
zeroGenusFuchsianPresentedGroupEquivOfIndexedPeriods
(firstReductionTransportSignature m₁' m₂'
(firstReductionTailIncludingThird (q := q) m₃' tail)
hp hm₁' hm₂'
(firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
(Nat.succ_pos _))
(secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
hm₃' htail)
?_ ?_
(Fintype.equivFin (FirstReductionIndex (tailLen + 1) p))
((firstReductionIndexSuccEquivSecondReductionSourceIndex hp).trans
(Fintype.equivFin (SecondReductionSourceIndex tailLen p))) ?_
· simp only [firstReductionTransportSignature, familyFuchsianSignature]
· simp only [secondReductionSourceSignature, familyFuchsianSignature]
· intro x
calc
(firstReductionTransportSignature m₁' m₂'
(firstReductionTailIncludingThird (q := q) m₃' tail)
hp hm₁' hm₂'
(firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
(Nat.succ_pos _)).periods
((Fintype.equivFin (FirstReductionIndex (tailLen + 1) p)) x)
=
firstReductionPeriods (p := p) m₁' m₂'
(firstReductionTailIncludingThird (q := q) m₃' tail) x := by
simp only [firstReductionTransportSignature, familyFuchsianSignature_periods]
_ =
secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail
(firstReductionIndexSuccEquivSecondReductionSourceIndex hp x) :=
firstReductionTailIncludingThird_transportPeriods_reindexed
m₁' m₂' m₃' tail hp x
_ =
(secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
hm₃' htail).periods
((Fintype.equivFin (SecondReductionSourceIndex tailLen p))
(firstReductionIndexSuccEquivSecondReductionSourceIndex hp x)) := by
simp only [secondReductionSourceSignature, familyFuchsianSignature_periods]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. 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. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□