FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Signatures.lean
1import FenchelNielsenZomorrodian.Discrete.Core.EllipticQuotientHom
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.ActualTransport
3import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.Signatures
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Signatures.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
16The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.
17-/
19open scoped BigOperators
20namespace FenchelNielsen
22 {tailLen p q : ℕ}
23 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
24 (i : Fin (2 + (p + tailLen * p))) : ℕ :=
25 if _h0 : i.val = 0 then
26 m₁'
27 else if _h1 : i.val = 1 then
28 m₂'
29 else if _hmid : i.val < 2 + p then
30 q * m₃'
31 else if hTailLen : 0 < tailLen then
32 tail ⟨(i.val - (2 + p)) % tailLen, Nat.mod_lt _ hTailLen⟩
33 else
34 m₁'
35@[local simp]
37 {tailLen p q : ℕ}
38 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
39 secondReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) (q := q)
40 m₁' m₂' m₃' tail ⟨0, by omega⟩ = m₁' := by
41 simp only [secondReductionCanonicalSourcePeriod, ↓reduceDIte]
42@[local simp]
44 {tailLen p q : ℕ}
45 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
46 secondReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) (q := q)
47 m₁' m₂' m₃' tail ⟨1, by omega⟩ = m₂' := by
48 simp only [secondReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte]
49@[local simp]
51 {tailLen p q : ℕ}
52 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) (r : Fin p) :
53 secondReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) (q := q)
54 m₁' m₂' m₃' tail ⟨2 + r.val, by omega⟩ = q * m₃' := by
56 have h0 : 2 + r.val ≠ 0 := by omega
57 have h1 : 2 + r.val ≠ 1 := by omega
58 have hmid : 2 + r.val < 2 + p := by omega
59 simp only [Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceDIte, h1, hmid]
60@[local simp]
62 {tailLen p q : ℕ}
63 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
64 (k : Fin p) (j : Fin tailLen) :
65 secondReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) (q := q)
66 m₁' m₂' m₃' tail
67 ⟨2 + p + k.val * tailLen + j.val, by
68 have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
69 calc
70 k.val * tailLen + j.val < k.val * tailLen + tailLen :=
71 Nat.add_lt_add_left j.isLt _
72 _ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
73 have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
74 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
75 have hmain : k.val * tailLen + j.val < p * tailLen :=
76 lt_of_lt_of_le hblock hle
77 have hcomm : p * tailLen = tailLen * p := Nat.mul_comm p tailLen
78 omega⟩ = tail j := by
80 have h0 : 2 + p + k.val * tailLen + j.val ≠ 0 := by omega
81 have h1 : 2 + p + k.val * tailLen + j.val ≠ 1 := by omega
82 have hmid : ¬ 2 + p + k.val * tailLen + j.val < 2 + p := by omega
83 have hTailLen : 0 < tailLen := lt_of_le_of_lt (Nat.zero_le _) j.isLt
84 simp only [Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, mul_eq_zero, ↓reduceDIte, h1, hmid, hTailLen]
85 have hsub :
86 2 + p + k.val * tailLen + j.val - (2 + p) =
87 k.val * tailLen + j.val := by
88 omega
89 have hmod :
90 (2 + p + k.val * tailLen + j.val - (2 + p)) % tailLen = j.val := by
91 rw [hsub, Nat.mul_comm k.val tailLen, Nat.mul_add_mod_self_left,
92 Nat.mod_eq_of_lt j.isLt]
93 exact congrArg tail (Fin.ext hmod)
95 {tailLen p q : ℕ}
96 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
97 (hp : 2 ≤ p) (hq : 2 ≤ q)
98 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
99 (htail : ∀ j, 2 ≤ tail j) :
100 FuchsianSignature where
101 orbitGenus := 0
102 numCusps := 0
103 numPeriods := 2 + (p + tailLen * p)
104 periods :=
105 secondReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) (q := q)
106 m₁' m₂' m₃' tail
107 period_ge_two := by
108 intro i
110 by_cases h0 : i.val = 0
111 · rw [dif_pos h0]
112 exact hm₁'
113 · by_cases h1 : i.val = 1
114 · rw [dif_neg h0, dif_pos h1]
115 exact hm₂'
116 · by_cases hmid : i.val < 2 + p
117 · rw [dif_neg h0, dif_neg h1, dif_pos hmid]
118 exact le_trans hq
119 (Nat.le_mul_of_pos_right q (lt_of_lt_of_le (by decide : 0 < 2) hm₃'))
120 · by_cases hTailLen : 0 < tailLen
121 · rw [dif_neg h0, dif_neg h1, dif_neg hmid, dif_pos hTailLen]
122 exact htail ⟨(i.val - (2 + p)) % tailLen, Nat.mod_lt _ hTailLen⟩
123 · rw [dif_neg h0, dif_neg h1, dif_neg hmid, dif_neg hTailLen]
124 exact hm₁'
125 numCusps_eq_zero := rfl
126 numPeriods_ge_three := by omega
128 {tailLen p q : ℕ}
129 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
130 (hp : 2 ≤ p) (hq : 2 ≤ q)
131 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
132 (htail : ∀ j, 2 ≤ tail j) :
133 Fin
135 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).numPeriods :=
136 ⟨0, by simp only [secondReductionCanonicalSourceSignature, add_pos_iff, Nat.ofNat_pos, CanonicallyOrderedAdd.mul_pos,
137 true_or]⟩
139 {tailLen p q : ℕ}
140 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
141 (hp : 2 ≤ p) (hq : 2 ≤ q)
142 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
143 (htail : ∀ j, 2 ≤ tail j) :
144 Fin
146 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).numPeriods :=
147 ⟨1, by simp only [secondReductionCanonicalSourceSignature]; omega⟩
149 {tailLen p q : ℕ}
150 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
151 (hp : 2 ≤ p) (hq : 2 ≤ q)
152 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
153 (htail : ∀ j, 2 ≤ tail j) (r : Fin p) :
154 Fin
156 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).numPeriods :=
157 ⟨2 + r.val, by simp only [secondReductionCanonicalSourceSignature, add_lt_add_iff_left]; omega⟩
159 {tailLen p q : ℕ}
160 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
161 (hp : 2 ≤ p) (hq : 2 ≤ q)
162 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
163 (htail : ∀ j, 2 ≤ tail j) (k : Fin p) (j : Fin tailLen) :
164 Fin
166 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).numPeriods :=
167 ⟨2 + p + k.val * tailLen + j.val, by
168 have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
169 calc
170 k.val * tailLen + j.val < k.val * tailLen + tailLen :=
171 Nat.add_lt_add_left j.isLt _
172 _ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
173 have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
174 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
175 have hmain : k.val * tailLen + j.val < p * tailLen :=
176 lt_of_lt_of_le hblock hle
177 have hcomm : p * tailLen = tailLen * p := Nat.mul_comm p tailLen
178 simp only [secondReductionCanonicalSourceSignature, gt_iff_lt]
179 omega⟩
180@[simp 900] theorem secondReductionCanonicalSourceSignature_period_zero
181 {tailLen p q : ℕ}
182 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
183 (hp : 2 ≤ p) (hq : 2 ≤ q)
184 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
185 (htail : ∀ j, 2 ≤ tail j) :
187 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
189 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) =
190 m₁' := by
191 simp only [secondReductionCanonicalSourceSignature, secondReductionCanonicalSourceZeroIndex, Fin.mk_zero',
192 secondReductionCanonicalSourcePeriod, Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceDIte]
193@[simp 900] theorem secondReductionCanonicalSourceSignature_period_one
194 {tailLen p q : ℕ}
195 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
196 (hp : 2 ≤ p) (hq : 2 ≤ q)
197 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
198 (htail : ∀ j, 2 ≤ tail j) :
200 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
202 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) =
203 m₂' := by
205 secondReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte]
206@[simp 900] theorem secondReductionCanonicalSourceSignature_period_middle
207 {tailLen p q : ℕ}
208 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
209 (hp : 2 ≤ p) (hq : 2 ≤ q)
210 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
211 (htail : ∀ j, 2 ≤ tail j) (r : Fin p) :
213 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
215 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r) =
216 q * m₃' := by
219@[simp 900] theorem secondReductionCanonicalSourceSignature_period_tail
220 {tailLen p q : ℕ}
221 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
222 (hp : 2 ≤ p) (hq : 2 ≤ q)
223 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
224 (htail : ∀ j, 2 ≤ tail j) (k : Fin p) (j : Fin tailLen) :
226 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
228 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k j) =
229 tail j := by
233 {tailLen p q : ℕ}
234 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
235 (hp : 2 ≤ p) (hq : 2 ≤ q)
236 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
237 (htail : ∀ j, 2 ≤ tail j) :
238 let σ :=
240 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
241 totalRelation σ =
244 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) *
247 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) *
250 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
251 ⟨0, by omega⟩) *
254 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
255 ⟨1, by omega⟩) *
256 (List.ofFn (fun r : Fin (p - 2) =>
259 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
260 ⟨2 + r.val, by omega⟩))).prod *
261 (List.ofFn (fun b : Fin p =>
262 (List.ofFn (fun j : Fin tailLen =>
265 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j))).prod)).prod := by
266 classical
267 let σ :=
269 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
270 let f : Fin (2 + (p + tailLen * p)) → FreeGroup (FuchsianGenerator σ) :=
272 let middle : Fin p → FreeGroup (FuchsianGenerator σ) :=
273 fun r =>
276 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r)
277 let tailFlat : Fin (tailLen * p) → FreeGroup (FuchsianGenerator σ) :=
278 fun t =>
280 ⟨2 + p + t.val, by
281 have ht : t.val < tailLen * p := t.isLt
282 simp only [secondReductionCanonicalSourceSignature, gt_iff_lt, σ]
283 omega⟩
284 let tailFlat' : Fin (p * tailLen) → FreeGroup (FuchsianGenerator σ) :=
285 fun t =>
287 ⟨2 + p + t.val, by
288 have ht : t.val < p * tailLen := t.isLt
289 have hcomm : p * tailLen = tailLen * p := Nat.mul_comm p tailLen
290 simp only [secondReductionCanonicalSourceSignature, gt_iff_lt, σ]
291 omega⟩
292 have hafter :
293 (List.ofFn (fun j : Fin (p + tailLen * p) => f ⟨2 + j.val, by omega⟩)).prod =
294 (List.ofFn middle).prod * (List.ofFn tailFlat).prod := by
295 have hlist :
296 List.ofFn (fun j : Fin (p + tailLen * p) => f ⟨2 + j.val, by omega⟩) =
297 List.ofFn middle ++ List.ofFn tailFlat := by
298 rw [← List.ofFn_fin_append middle tailFlat]
299 apply List.ofFn_inj.2
300 funext i
301 cases i using Fin.addCases with
302 | left r =>
303 dsimp [f, middle, tailFlat]
304 rw [Fin.append_left]
305 rfl
306 | right t =>
307 dsimp [f, middle, tailFlat]
308 rw [Fin.append_right]
309 congr 1
310 ext
311 simp only
312 omega
313 rw [hlist, List.prod_append]
314 have hmiddle :
315 (List.ofFn middle).prod =
318 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
319 ⟨0, by omega⟩) *
322 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
323 ⟨1, by omega⟩) *
324 (List.ofFn (fun r : Fin (p - 2) =>
327 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
328 ⟨2 + r.val, by omega⟩))).prod := by
329 have hcast :
330 List.ofFn middle =
331 List.ofFn (fun i : Fin (2 + (p - 2)) =>
332 middle ⟨i.val, by omega⟩) := by
333 rw [List.ofFn_congr (show p = 2 + (p - 2) by omega)]
334 rfl
335 rw [hcast]
336 simpa [middle, List.prod_cons, mul_assoc] using
337 congrArg List.prod
338 (list_ofFn_two_add (fun i : Fin (2 + (p - 2)) =>
339 middle ⟨i.val, by omega⟩))
340 have htailCast :
341 (List.ofFn tailFlat).prod = (List.ofFn tailFlat').prod := by
342 have hlist :
343 List.ofFn tailFlat = List.ofFn tailFlat' := by
344 rw [List.ofFn_congr (show tailLen * p = p * tailLen by rw [Nat.mul_comm])]
345 rfl
346 rw [hlist]
347 have htailBlocks :
348 (List.ofFn tailFlat').prod =
349 (List.ofFn (fun b : Fin p =>
350 (List.ofFn (fun j : Fin tailLen =>
353 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j))).prod)).prod := by
354 rw [list_prod_ofFn_mul_blocks tailFlat']
355 congr
356 funext b
357 congr
358 funext j
359 dsimp [tailFlat']
360 congr 1
361 ext
362 simp only [secondReductionCanonicalSourceTailIndex]
363 omega
364 change totalRelation σ =
367 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) *
370 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) *
373 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
374 ⟨0, by omega⟩) *
377 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
378 ⟨1, by omega⟩) *
379 (List.ofFn (fun r : Fin (p - 2) =>
382 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
383 ⟨2 + r.val, by omega⟩))).prod *
384 (List.ofFn (fun b : Fin p =>
385 (List.ofFn (fun j : Fin tailLen =>
388 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j))).prod)).prod
389 have htwo :=
390 congrArg List.prod
391 (list_ofFn_two_add (fun i : Fin (2 + (p + tailLen * p)) => f i))
392 dsimp [f] at htwo
393 have hprod :
397 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) *
400 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) *
403 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
404 ⟨0, by omega⟩) *
407 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
408 ⟨1, by omega⟩) *
409 (List.ofFn (fun r : Fin (p - 2) =>
412 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
413 ⟨2 + r.val, by omega⟩))).prod *
414 (List.ofFn (fun b : Fin p =>
415 (List.ofFn (fun j : Fin tailLen =>
418 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j))).prod)).prod := by
419 rw [htwo, hafter, hmiddle, htailCast, htailBlocks]
420 simp only [mul_assoc, secondReductionCanonicalSourceZeroIndex, secondReductionCanonicalSourceOneIndex,
421 mul_left_inj, σ]
422 congr 1
423 rw [totalRelation]
424 simpa [σ, secondReductionCanonicalSourceSignature, List.ofFn_eq_map,
425 List.prod_cons, mul_assoc] using hprod
427 (tailLen p : ℕ) :
428 FirstSecondInputIndex tailLen p ≃ Fin (2 + (p + tailLen * p)) :=
429 (Equiv.sumCongr (Equiv.refl (Fin 2))
430 ((Equiv.sumCongr (Equiv.refl (Fin p))
431 ((Equiv.prodComm (Fin tailLen) (Fin p)).trans finProdFinEquiv)).trans
432 (finSumFinEquiv.trans (finCongr (by rw [Nat.mul_comm p tailLen]))))).trans
433 finSumFinEquiv
434@[local simp]
436 (tailLen p : ℕ) :
437 firstSecondInputIndexEquivCanonicalSecondSourceFin tailLen p (.inl (0 : Fin 2)) =
438 (⟨0, by omega⟩ : Fin (2 + (p + tailLen * p))) := by
439 ext
440 simp only [firstSecondInputIndexEquivCanonicalSecondSourceFin, Fin.isValue, Equiv.trans_apply,
441 Equiv.sumCongr_apply, Equiv.coe_refl, Equiv.coe_trans, Sum.map_inl, id_eq, finSumFinEquiv_apply_left,
442 Fin.val_castAdd, Fin.coe_ofNat_eq_mod, Nat.zero_mod]
443@[local simp]
445 (tailLen p : ℕ) :
446 firstSecondInputIndexEquivCanonicalSecondSourceFin tailLen p (.inl (1 : Fin 2)) =
447 (⟨1, by omega⟩ : Fin (2 + (p + tailLen * p))) := by
448 ext
449 simp only [firstSecondInputIndexEquivCanonicalSecondSourceFin, Fin.isValue, Equiv.trans_apply,
450 Equiv.sumCongr_apply, Equiv.coe_refl, Equiv.coe_trans, Sum.map_inl, id_eq, finSumFinEquiv_apply_left,
451 Fin.val_castAdd, Fin.coe_ofNat_eq_mod, Nat.mod_succ]
452@[local simp]
454 {tailLen p : ℕ} (r : Fin p) :
455 firstSecondInputIndexEquivCanonicalSecondSourceFin tailLen p (.inr (.inl r)) =
456 (⟨2 + r.val, by omega⟩ : Fin (2 + (p + tailLen * p))) := by
457 ext
458 simp only [firstSecondInputIndexEquivCanonicalSecondSourceFin, Equiv.trans_apply, Equiv.sumCongr_apply,
459 Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr, Function.comp_apply, Equiv.coe_prodComm, Sum.map_inl, id_eq,
460 finSumFinEquiv_apply_left, finCongr_apply, Fin.cast_castAdd_right, finSumFinEquiv_apply_right, Fin.val_natAdd,
461 Fin.val_castAdd]
462@[local simp]
464 {tailLen p : ℕ} (j : Fin tailLen) (k : Fin p) :
465 firstSecondInputIndexEquivCanonicalSecondSourceFin tailLen p (.inr (.inr (j, k))) =
466 (⟨2 + p + k.val * tailLen + j.val, by
467 have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
468 calc
469 k.val * tailLen + j.val < k.val * tailLen + tailLen :=
470 Nat.add_lt_add_left j.isLt _
471 _ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
472 have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
473 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
474 have hmain : k.val * tailLen + j.val < p * tailLen :=
475 lt_of_lt_of_le hblock hle
476 have hcomm : p * tailLen = tailLen * p := Nat.mul_comm p tailLen
477 omega⟩ : Fin (2 + (p + tailLen * p))) := by
478 ext
479 simp only [firstSecondInputIndexEquivCanonicalSecondSourceFin, finProdFinEquiv, Equiv.trans_apply,
480 Equiv.sumCongr_apply, Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr, Function.comp_apply, Equiv.coe_fn_mk,
481 Equiv.coe_prodComm, Prod.swap_prod_mk, finSumFinEquiv_apply_right, Fin.natAdd_mk, finCongr_apply, Fin.cast_mk,
482 Nat.mul_comm]
483 omega
485 {tailLen p : ℕ} (hp : 2 ≤ p) :
486 SecondReductionSourceIndex tailLen p ≃ Fin (2 + (p + tailLen * p)) :=
487 (firstSecondInputIndexEquivSecondReductionSourceIndex (tailLen := tailLen) hp).symm.trans
489@[local simp]
491 {tailLen p : ℕ} (hp : 2 ≤ p) :
492 secondReductionSourceIndexEquivCanonicalSourceFin (tailLen := tailLen) hp (.inl (0 : Fin 2)) =
493 (⟨0, by omega⟩ : Fin (2 + (p + tailLen * p))) := by
494 ext
495 simp only [secondReductionSourceIndexEquivCanonicalSourceFin,
496 firstSecondInputIndexEquivSecondReductionSourceIndex, Equiv.sumCongr_symm, Equiv.refl_symm, Fin.isValue,
497 Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inl, id_eq,
498 firstSecondInputIndexEquivCanonicalSecondSourceFin_inl_zero, Fin.mk_zero', Fin.coe_ofNat_eq_mod, Nat.zero_mod]
499@[local simp]
501 {tailLen p : ℕ} (hp : 2 ≤ p) :
502 secondReductionSourceIndexEquivCanonicalSourceFin (tailLen := tailLen) hp (.inl (1 : Fin 2)) =
503 (⟨1, by omega⟩ : Fin (2 + (p + tailLen * p))) := by
504 ext
505 simp only [secondReductionSourceIndexEquivCanonicalSourceFin,
506 firstSecondInputIndexEquivSecondReductionSourceIndex, Equiv.sumCongr_symm, Equiv.refl_symm, Fin.isValue,
507 Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inl, id_eq,
509@[local simp]
511 {tailLen p : ℕ} (hp : 2 ≤ p) (i : Fin 2) :
512 secondReductionSourceIndexEquivCanonicalSourceFin (tailLen := tailLen) hp (.inr (.inl i)) =
513 (⟨2 + i.val, by omega⟩ : Fin (2 + (p + tailLen * p))) := by
514 ext
515 fin_cases i <;>
516 simp only [secondReductionSourceIndexEquivCanonicalSourceFin,
517 firstSecondInputIndexEquivSecondReductionSourceIndex, finTwoRestEquiv, Equiv.sumCongr_symm, Equiv.refl_symm,
518 Fin.mk_one, Fin.isValue, Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr,
519 Equiv.symm_trans_apply, Equiv.sumAssoc_symm_apply_inl, Sum.map_inl, finCongr_symm, Equiv.symm_symm,
520 finSumFinEquiv_apply_left, finCongr_apply, firstSecondInputIndexEquivCanonicalSecondSourceFin_middle, Fin.val_cast,
521 Fin.val_castAdd, Fin.coe_ofNat_eq_mod, Nat.mod_succ, Nat.reduceAdd]
522@[local simp]
524 {tailLen p : ℕ} (hp : 2 ≤ p) (r : Fin (p - 2)) :
526 (tailLen := tailLen) hp (.inr (.inr (.inl r))) =
527 (⟨4 + r.val, by omega⟩ : Fin (2 + (p + tailLen * p))) := by
528 ext
529 simp only [secondReductionSourceIndexEquivCanonicalSourceFin,
530 firstSecondInputIndexEquivSecondReductionSourceIndex, finTwoRestEquiv, Equiv.sumCongr_symm, Equiv.refl_symm,
531 Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, Equiv.symm_trans_apply,
532 Equiv.sumAssoc_symm_apply_inr_inl, Sum.map_inl, finCongr_symm, Equiv.symm_symm, finSumFinEquiv_apply_right,
533 finCongr_apply, firstSecondInputIndexEquivCanonicalSecondSourceFin_middle, Fin.val_cast, Fin.val_natAdd]
534 omega
535@[local simp]
537 {tailLen p : ℕ} (hp : 2 ≤ p) (j : Fin tailLen) (k : Fin p) :
539 (tailLen := tailLen) hp (.inr (.inr (.inr (j, k)))) =
540 (⟨2 + p + k.val * tailLen + j.val, by
541 have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
542 calc
543 k.val * tailLen + j.val < k.val * tailLen + tailLen :=
544 Nat.add_lt_add_left j.isLt _
545 _ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
546 have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
547 Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
548 have hmain : k.val * tailLen + j.val < p * tailLen :=
549 lt_of_lt_of_le hblock hle
550 have hcomm : p * tailLen = tailLen * p := Nat.mul_comm p tailLen
551 omega⟩ : Fin (2 + (p + tailLen * p))) := by
552 ext
553 simp only [secondReductionSourceIndexEquivCanonicalSourceFin,
554 firstSecondInputIndexEquivSecondReductionSourceIndex, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.trans_apply,
555 Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, Equiv.symm_trans_apply, Equiv.sumAssoc_symm_apply_inr_inr, id_eq,
556 firstSecondInputIndexEquivCanonicalSecondSourceFin_tail, Nat.mul_comm]
558 {tailLen p q : ℕ}
559 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
560 (hp : 2 ≤ p) (hq : 2 ≤ q)
561 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
562 (htail : ∀ j, 2 ≤ tail j) :
563 Nonempty
565 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
566 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail)
567 ≃*
570 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)) := by
571 classical
572 refine
574 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
575 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail)
577 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
578 ?_ ?_
579 (Fintype.equivFin (SecondReductionSourceIndex tailLen p))
580 (secondReductionSourceIndexEquivCanonicalSourceFin (tailLen := tailLen) hp) ?_
581 · simp only [secondReductionSourceSignature, familyFuchsianSignature]
582 · simp only [secondReductionCanonicalSourceSignature]
583 · intro x
584 cases x with
585 | inl i =>
586 fin_cases i
587 · calc
588 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
589 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail).periods
590 ((Fintype.equivFin (SecondReductionSourceIndex tailLen p)) (.inl (0 : Fin 2))) =
591 m₁' := by
592 simp only [secondReductionSourceSignature, familyFuchsianSignature, secondReductionSourcePeriods, twoPeriods,
593 Nat.reduceAdd, Fin.isValue, Equiv.symm_apply_apply, Fin.cases_zero]
594 _ =
596 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
598 (tailLen := tailLen) hp (.inl (0 : Fin 2))) := by
599 simpa [secondReductionCanonicalSourceZeroIndex] using
601 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm
602 · calc
603 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
604 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail).periods
605 ((Fintype.equivFin (SecondReductionSourceIndex tailLen p)) (.inl (1 : Fin 2))) =
606 m₂' := by
607 simp only [secondReductionSourceSignature, familyFuchsianSignature, secondReductionSourcePeriods, twoPeriods,
608 Nat.reduceAdd, Fin.isValue, Equiv.symm_apply_apply, fin_cases_const_one]
609 _ =
611 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
613 (tailLen := tailLen) hp (.inl (1 : Fin 2))) := by
614 simpa [secondReductionCanonicalSourceOneIndex] using
616 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm
617 | inr s =>
618 cases s with
619 | inl i =>
620 fin_cases i
621 · calc
622 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
623 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail).periods
624 ((Fintype.equivFin (SecondReductionSourceIndex tailLen p))
625 (.inr (.inl (0 : Fin 2)))) =
626 q * m₃' := by
627 simp only [secondReductionSourceSignature, familyFuchsianSignature, secondReductionSourcePeriods, Fin.isValue,
628 Equiv.symm_apply_apply]
629 _ =
631 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
633 (tailLen := tailLen) hp (.inr (.inl (0 : Fin 2)))) := by
634 simpa [secondReductionCanonicalSourceMiddleIndex] using
636 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
637 ⟨0, by omega⟩).symm
638 · calc
639 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
640 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail).periods
641 ((Fintype.equivFin (SecondReductionSourceIndex tailLen p))
642 (.inr (.inl (1 : Fin 2)))) =
643 q * m₃' := by
644 simp only [secondReductionSourceSignature, familyFuchsianSignature, secondReductionSourcePeriods, Fin.isValue,
645 Equiv.symm_apply_apply]
646 _ =
648 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
650 (tailLen := tailLen) hp (.inr (.inl (1 : Fin 2)))) := by
651 simpa [secondReductionCanonicalSourceMiddleIndex] using
653 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
654 ⟨1, by omega⟩).symm
655 | inr s =>
656 cases s with
657 | inl r =>
658 calc
659 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
660 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail).periods
661 ((Fintype.equivFin (SecondReductionSourceIndex tailLen p))
662 (.inr (.inr (.inl r)))) =
663 q * m₃' := by
664 simp only [secondReductionSourceSignature, familyFuchsianSignature, secondReductionSourcePeriods,
665 Equiv.symm_apply_apply]
666 _ =
668 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
670 (tailLen := tailLen) hp (.inr (.inr (.inl r)))) := by
671 simpa [secondReductionCanonicalSourceMiddleIndex, Nat.add_assoc,
672 Nat.add_comm, Nat.add_left_comm] using
674 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
675 ⟨2 + r.val, by omega⟩).symm
676 | inr jk =>
677 rcases jk with ⟨j, k⟩
678 calc
679 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
680 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') htail).periods
681 ((Fintype.equivFin (SecondReductionSourceIndex tailLen p))
682 (.inr (.inr (.inr (j, k))))) =
683 tail j := by
684 simp only [secondReductionSourceSignature, familyFuchsianSignature, secondReductionSourcePeriods,
685 Equiv.symm_apply_apply]
686 _ =
688 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
690 (tailLen := tailLen) hp (.inr (.inr (.inr (j, k))))) := by
691 simpa [secondReductionCanonicalSourceTailIndex] using
693 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k j).symm
694noncomputable def secondReductionCanonicalSourceQuotientImage
695 {tailLen p q : ℕ}
696 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
697 (hp : 2 ≤ p) (hq : 2 ≤ q)
698 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
699 (htail : ∀ j, 2 ≤ tail j) :
700 (let σ :=
701 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
702 Fin σ.numPeriods → Multiplicative (ZMod q)) :=
703 fun i =>
704 if i.val = 2 then Multiplicative.ofAdd (1 : ZMod q)
705 else if i.val = 3 then Multiplicative.ofAdd (-1 : ZMod q)
706 else 1
708 {tailLen p q : ℕ}
709 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
710 (hp : 2 ≤ p) (hq : 2 ≤ q)
711 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
712 (htail : ∀ j, 2 ≤ tail j) :
713 let σ :=
714 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
715 ∀ i : Fin σ.numPeriods,
717 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i ^
718 σ.periods i = 1 := by
719 classical
720 dsimp
721 intro i
722 by_cases h2 : i.val = 2
723 · have hi :
724 i =
726 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
727 ⟨0, by omega⟩ := by
728 ext
729 simpa [secondReductionCanonicalSourceMiddleIndex] using h2
730 rw [hi]
731 have hval :
733 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
734 ⟨0, by omega⟩).val = 2 := by
735 simp only [secondReductionCanonicalSourceMiddleIndex, add_zero]
736 rw [secondReductionCanonicalSourceQuotientImage, if_pos hval]
737 apply (Multiplicative.toAdd : Multiplicative (ZMod q) ≃ ZMod q).injective
738 simp only [secondReductionCanonicalSourceSignature_period_middle, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul,
739 Nat.cast_mul, CharP.cast_eq_zero, zero_mul, mul_one, toAdd_one]
740 · by_cases h3 : i.val = 3
741 · have hp1 : 1 < p := by omega
742 have hi :
743 i =
745 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
746 ⟨1, hp1⟩ := by
747 ext
748 simpa [secondReductionCanonicalSourceMiddleIndex] using h3
749 rw [hi]
750 have hnot2 :
752 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
753 ⟨1, hp1⟩).val ≠ 2 := by
754 simp only [secondReductionCanonicalSourceMiddleIndex, Nat.reduceAdd, ne_eq, Nat.succ_ne_self,
755 not_false_eq_true]
756 have hval :
758 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
759 ⟨1, hp1⟩).val = 3 := by
760 simp only [secondReductionCanonicalSourceMiddleIndex, Nat.reduceAdd]
761 rw [secondReductionCanonicalSourceQuotientImage, if_neg hnot2, if_pos hval]
762 apply (Multiplicative.toAdd : Multiplicative (ZMod q) ≃ ZMod q).injective
763 simp only [ofAdd_neg, secondReductionCanonicalSourceSignature_period_middle, inv_pow, toAdd_inv, toAdd_pow,
764 toAdd_ofAdd, nsmul_eq_mul, Nat.cast_mul, CharP.cast_eq_zero, zero_mul, mul_one, neg_zero, toAdd_one]
765 · simp only [secondReductionCanonicalSourceQuotientImage, h2, ↓reduceIte, h3, one_pow]
767 {tailLen p q : ℕ}
768 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
769 (hp : 2 ≤ p) (hq : 2 ≤ q)
770 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
771 (htail : ∀ j, 2 ≤ tail j) :
772 let σ :=
773 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
774 ∏ i : Fin σ.numPeriods,
776 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i = 1 := by
777 classical
778 dsimp
779 let σ :=
780 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
781 let ξ : Fin σ.numPeriods → Multiplicative (ZMod q) :=
783 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
784 change ∏ i : Fin σ.numPeriods, ξ i = 1
785 have hnum : σ.numPeriods = 2 + (p + tailLen * p) := by
786 simp only [secondReductionCanonicalSourceSignature, σ]
787 let n := 2 + (p + tailLen * p)
788 let f : Fin n → Multiplicative (ZMod q) := fun i =>
789 if i.val = 2 then Multiplicative.ofAdd (1 : ZMod q)
790 else if i.val = 3 then Multiplicative.ofAdd (-1 : ZMod q)
791 else 1
792 change ∏ i : Fin n, f i = 1
793 let i2 : Fin n := ⟨2, by omega⟩
794 let i3 : Fin n := ⟨3, by omega⟩
795 rw [← Finset.mul_prod_erase Finset.univ f (Finset.mem_univ i2)]
796 have hprod3 : (∏ x ∈ Finset.univ.erase i2, f x) = f i3 := by
797 refine Finset.prod_eq_single_of_mem i3 ?hmem ?hone
798 · simp only [Finset.mem_erase, ne_eq, Fin.mk.injEq, Nat.succ_ne_self, not_false_eq_true, Finset.mem_univ,
799 and_self, i2, i3]
800 · intro b hb hbne
801 have hb_ne_i2 : b ≠ i2 := (Finset.mem_erase.mp hb).1
802 have hb2 : b.val ≠ 2 := by
803 intro h
804 apply hb_ne_i2
805 ext
806 simpa [i2] using h
807 have hb3 : b.val ≠ 3 := by
808 intro h
809 apply hbne
810 ext
811 simpa [i3] using h
812 simp only [ofAdd_neg, hb2, ↓reduceIte, hb3, f]
813 rw [hprod3]
814 simp only [ofAdd_neg, ↓reduceIte, Nat.succ_ne_self, mul_inv_cancel, f, i2, i3]
815noncomputable def secondReductionCanonicalSourceQuotientHom
816 {tailLen p q : ℕ}
817 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
818 (hp : 2 ≤ p) (hq : 2 ≤ q)
819 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
820 (htail : ∀ j, 2 ≤ tail j) :
823 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) →*
824 Multiplicative (ZMod q) := by
825 classical
826 let σ :=
827 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
828 exact
831 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
833 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
835 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
836@[local simp]
838 {tailLen p q : ℕ}
839 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
840 (hp : 2 ≤ p) (hq : 2 ≤ q)
841 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
842 (htail : ∀ j, 2 ≤ tail j) :
844 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
845 (PresentedGroup.of
848 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
849 (FuchsianGenerator.elliptic
851 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨0, by omega⟩))) =
852 Multiplicative.ofAdd (1 : ZMod q) := by
853 classical
855 secondReductionCanonicalSourceMiddleIndex, add_zero, PresentedGroup.toGroup.of, ellipticQuotientGeneratorImage,
856 secondReductionCanonicalSourceQuotientImage, ↓reduceIte]