FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/ActualTransport.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.Reductions
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/ActualTransport.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14The first explicit finite quotient reduction for compact zero-genus Fuchsian presentations, including quotient maps, basis transport, signatures, and relator verification.
15-/
17namespace FenchelNielsen
18private theorem firstReductionIndex_card_ge_three
19 {tailLen p : ℕ} (hp : 2 ≤ p) (hTailLen : 0 < tailLen) :
20 3 ≤ Fintype.card (FirstReductionIndex tailLen p) := by
21 simp only [FirstReductionIndex, Fintype.card_sum, Fintype.card_fin, Fintype.card_prod]
22 nlinarith [Nat.succ_le_iff.mpr hTailLen, hp]
23private theorem firstReductionPeriods_ge_two
24 {tailLen p : ℕ}
25 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
26 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
27 (x : FirstReductionIndex tailLen p) :
28 2 ≤ firstReductionPeriods (p := p) m₁' m₂' tail x := by
29 cases x using Sum.casesOn <;> rename_i x
30 · fin_cases x
31 · simpa [firstReductionPeriods, twoPeriods] using hm₁'
32 · simpa [firstReductionPeriods, twoPeriods] using hm₂'
33 · simpa [firstReductionPeriods] using htail x.1
34noncomputable def firstReductionTransportSignature
35 {tailLen p : ℕ}
36 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
37 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
38 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
41 (firstReductionPeriods (p := p) m₁' m₂' tail)
42 (firstReductionPeriods_ge_two m₁' m₂' tail hm₁' hm₂' htail)
43 (firstReductionIndex_card_ge_three hp hTailLen)
45 (tailLen p : ℕ) :
46 Fin (tailLen + 1) × Fin p ≃ Sum (Fin p) (Fin tailLen × Fin p) where
47 toFun jk :=
48 Fin.cases (motive := fun _ => Sum (Fin p) (Fin tailLen × Fin p))
49 (.inl jk.2)
50 (fun j => .inr (j, jk.2))
51 jk.1
52 invFun
53 | .inl k => (0, k)
54 | .inr jk => (jk.1.succ, jk.2)
55 left_inv := by
56 intro jk
57 rcases jk with ⟨j, k⟩
58 cases j using Fin.cases with
60 | succ j => rfl
61 right_inv := by
62 intro s
63 cases s with
64 | inl k => rfl
65 | inr jk =>
66 rcases jk with ⟨j, k⟩
67 rfl
69 (tailLen p : ℕ) :
70 FirstReductionIndex (tailLen + 1) p ≃ FirstSecondInputIndex tailLen p :=
71 Equiv.sumCongr (Equiv.refl (Fin 2))
72 (firstReductionTailSuccEquivFirstSecondTail tailLen p)
73def finTwoRestEquiv {p : ℕ} (hp : 2 ≤ p) : Fin p ≃ Sum (Fin 2) (Fin (p - 2)) :=
74 (finCongr (by omega : p = 2 + (p - 2))).trans finSumFinEquiv.symm
76 {tailLen p : ℕ} (hp : 2 ≤ p) :
77 FirstSecondInputIndex tailLen p ≃ SecondReductionSourceIndex tailLen p :=
78 Equiv.sumCongr (Equiv.refl (Fin 2))
79 ((Equiv.sumCongr (finTwoRestEquiv hp) (Equiv.refl (Fin tailLen × Fin p))).trans
80 (Equiv.sumAssoc (Fin 2) (Fin (p - 2)) (Fin tailLen × Fin p)))
82 {tailLen p : ℕ} (hp : 2 ≤ p) :
83 FirstReductionIndex (tailLen + 1) p ≃ SecondReductionSourceIndex tailLen p :=
84 (firstReductionIndexSuccEquivFirstSecondInputIndex tailLen p).trans
86private theorem firstReductionTailIncludingThird_transportPeriods_reindexed
87 {tailLen p q : ℕ}
88 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) (hp : 2 ≤ p)
89 (x : FirstReductionIndex (tailLen + 1) p) :
90 firstReductionPeriods (p := p) m₁' m₂'
91 (firstReductionTailIncludingThird (q := q) m₃' tail) x =
92 secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail
93 (firstReductionIndexSuccEquivSecondReductionSourceIndex hp x) := by
94 cases x using Sum.casesOn <;> rename_i x
95 · fin_cases x <;> rfl
96 · rcases x with ⟨j, k⟩
97 cases j using Fin.cases with
99 change q * m₃' =
100 secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail
101 (firstSecondInputIndexEquivSecondReductionSourceIndex hp (.inr (.inl k)))
103 cases h : finTwoRestEquiv hp k with
104 | inl i =>
105 simp only [secondReductionSourcePeriods, Equiv.sumCongr_apply, Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr,
106 Function.comp_apply, Sum.map_inl, h, Equiv.sumAssoc_apply_inl_inl]
107 | inr i =>
108 simp only [secondReductionSourcePeriods, Equiv.sumCongr_apply, Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr,
109 Function.comp_apply, Sum.map_inl, h, Equiv.sumAssoc_apply_inl_inr]
110 | succ j =>
111 rfl
113 {tailLen p q : ℕ}
114 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
115 (hp : 2 ≤ p) (hq : 2 ≤ q)
116 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 0 < m₃')
117 (htail : ∀ j, 2 ≤ tail j) :
118 Nonempty
120 (firstReductionTransportSignature m₁' m₂'
121 (firstReductionTailIncludingThird (q := q) m₃' tail)
122 hp hm₁' hm₂'
123 (firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
124 (Nat.succ_pos _))
125 ≃*
127 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
128 hm₃' htail)) := by
129 classical
130 refine
132 (firstReductionTransportSignature m₁' m₂'
133 (firstReductionTailIncludingThird (q := q) m₃' tail)
134 hp hm₁' hm₂'
135 (firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
136 (Nat.succ_pos _))
137 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
138 hm₃' htail)
139 ?_ ?_
140 (Fintype.equivFin (FirstReductionIndex (tailLen + 1) p))
142 (Fintype.equivFin (SecondReductionSourceIndex tailLen p))) ?_
143 · simp only [firstReductionTransportSignature, familyFuchsianSignature]
144 · simp only [secondReductionSourceSignature, familyFuchsianSignature]
145 · intro x
146 calc
147 (firstReductionTransportSignature m₁' m₂'
148 (firstReductionTailIncludingThird (q := q) m₃' tail)
149 hp hm₁' hm₂'
150 (firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
151 (Nat.succ_pos _)).periods
152 ((Fintype.equivFin (FirstReductionIndex (tailLen + 1) p)) x)
153 =
154 firstReductionPeriods (p := p) m₁' m₂'
155 (firstReductionTailIncludingThird (q := q) m₃' tail) x := by
157 _ =
158 secondReductionSourcePeriods (p := p) (q := q) m₁' m₂' m₃' tail
161 m₁' m₂' m₃' tail hp x
162 _ =
163 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
164 hm₃' htail).periods
165 ((Fintype.equivFin (SecondReductionSourceIndex tailLen p))
166 (firstReductionIndexSuccEquivSecondReductionSourceIndex hp x)) := by
168end FenchelNielsen