FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/RelatorProofs.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.TransportMaps
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/RelatorProofs.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 cyclic_rotate_three_eq_one {G : Type*} [Group G] {a b c : G}
19 (h : a * b * c = 1) :
20 b * c * a = 1 := by
21 have ha : a = (b * c)⁻¹ := by
22 calc
23 a = (a * b * c) * (b * c)⁻¹ := by group
24 _ = (b * c)⁻¹ := by rw [h]; simp only [mul_inv_rev, one_mul]
25 rw [ha]
26 group
27theorem negOneCycleSegmentProduct_eq {G : Type*} [Group G]
28 (x y : G) : ∀ (n l : ℕ), l ≤ n →
29 (List.ofFn (fun i : Fin l =>
30 x ^ (n - i.val) * y * (x ^ (n - 1 - i.val))⁻¹)).prod =
31 x ^ n * y ^ l * (x ^ (n - l))⁻¹
32 | n, 0, _ => by
33 simp only [List.ofFn_zero, List.prod_nil, pow_zero, mul_one, tsub_zero, mul_inv_cancel]
34 | n, l + 1, h => by
35 have hl : l ≤ n - 1 := by omega
36 rw [List.ofFn_succ, List.prod_cons]
37 simp only [Fin.val_zero, tsub_zero]
38 change
39 x ^ n * y * (x ^ (n - 1))⁻¹ *
40 (List.ofFn (fun i : Fin l =>
41 x ^ (n - (i.val + 1)) * y * (x ^ (n - 1 - (i.val + 1)))⁻¹)).prod =
42 x ^ n * y ^ (l + 1) * (x ^ (n - (l + 1)))⁻¹
43 have htail :
44 (List.ofFn (fun i : Fin l =>
45 x ^ (n - (i.val + 1)) * y * (x ^ (n - 1 - (i.val + 1)))⁻¹)).prod =
46 (List.ofFn (fun i : Fin l =>
47 x ^ (n - 1 - i.val) * y * (x ^ (n - 1 - 1 - i.val))⁻¹)).prod := by
48 congr
49 funext i
50 have h1 : n - (i.val + 1) = n - 1 - i.val := by omega
51 have h2 : n - 1 - (i.val + 1) = n - 1 - 1 - i.val := by omega
52 simp only [h1, h2]
53 rw [htail]
54 rw [negOneCycleSegmentProduct_eq x y (n - 1) l hl]
55 have hnl : n - 1 - l = n - (l + 1) := by omega
56 rw [hnl]
57 rw [pow_succ']
58 group
59theorem list_ofFn_desc_split {α : Type*} {p k : ℕ} (hk : k < p)
60 (f : Fin p → α) :
61 List.ofFn (fun i : Fin (p - 1) => f ⟨p - 1 - i.val, by omega⟩) =
62 List.ofFn (fun i : Fin (p - 1 - k) => f ⟨p - 1 - i.val, by omega⟩) ++
63 List.ofFn (fun i : Fin k => f ⟨k - i.val, by omega⟩) := by
64 let a : Fin (p - 1 - k) → α :=
65 fun i => f ⟨p - 1 - i.val, by omega⟩
66 let b : Fin k → α :=
67 fun i => f ⟨k - i.val, by omega⟩
68 have hlen : p - 1 = (p - 1 - k) + k := by omega
69 rw [List.ofFn_congr hlen]
70 rw [← List.ofFn_fin_append a b]
71 congr
72 funext i
73 cases i using Fin.addCases with
74 | left r =>
75 dsimp [a, b]
76 rw [Fin.append_left]
77 | right j =>
78 dsimp [a, b]
79 rw [Fin.append_right]
80 apply congrArg f
81 ext
82 simp only
83 omega
85 {tailLen p : ℕ}
86 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
87 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
88 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
89 (hFirst :
90 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
91 let σ :=
92 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
93 let τ :=
94 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
95 let φ :=
97 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
98 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
99 let e :=
101 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
102 let η :=
104 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
105 let x : FuchsianGenerator σ :=
107 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
108 let i₀ :=
110 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
111 ∀ k : Fin p,
112 η
113 (e.symm
115 ((FreeGroup.of x) ^ k.val)⁻¹, by
116 change φ
118 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
119 have hrφ :
122 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
124 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
126 (hSecond :
127 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
128 let σ :=
129 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
130 let τ :=
131 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
132 let φ :=
134 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
135 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
136 let e :=
138 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
139 let η :=
141 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
142 let x : FuchsianGenerator σ :=
144 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
145 let i₁ :=
147 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
148 ∀ k : Fin p,
149 η
150 (e.symm
152 ((FreeGroup.of x) ^ k.val)⁻¹, by
153 change φ
155 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
156 have hrφ :
159 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
161 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
163 (hTail :
164 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
165 let σ :=
166 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
167 let τ :=
168 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
169 let φ :=
171 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
172 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
173 let e :=
175 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
176 let η :=
178 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
179 let x : FuchsianGenerator σ :=
181 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
182 ∀ j : Fin tailLen, ∀ k : Fin p,
183 let iTail :=
185 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
186 η
187 (e.symm
189 ((FreeGroup.of x) ^ k.val)⁻¹, by
190 change φ
192 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
193 have hrφ :
196 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
198 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
200 (hTotal :
201 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
202 let σ :=
203 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
204 let τ :=
205 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
206 let φ :=
208 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
209 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
210 let e :=
212 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
213 let η :=
215 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
216 let x : FuchsianGenerator σ :=
218 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
219 ∀ k : Fin p,
220 η
221 (e.symm
222 (⟨(FreeGroup.of x) ^ k.val * totalRelation σ *
223 ((FreeGroup.of x) ^ k.val)⁻¹, by
224 change φ
225 ((FreeGroup.of x) ^ k.val * totalRelation σ *
226 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
227 have hrφ : φ (totalRelation σ) = 1 :=
229 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
230 (totalRelation σ) (Or.inr rfl)
231 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
233 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
234 let σ :=
235 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
236 let τ :=
237 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
238 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
239 let φ :=
241 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
242 let x : FuchsianGenerator σ :=
244 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
245 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
246 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
247 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
248 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
249 let hT : IsRightSchreierTransversal φ.ker T :=
251 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
253 let η :=
255 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
256 ∀ r ∈
259 (f := ellipticQuotientGeneratorImage σ
261 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
264 classical
265 dsimp
266 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
267 let σ :=
268 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
269 let τ :=
270 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
271 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
272 let φ :=
274 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
275 let x : FuchsianGenerator σ :=
277 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
278 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
279 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
280 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
281 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
282 let hT : IsRightSchreierTransversal φ.ker T :=
284 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
286 let hrels :=
288 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
289 let η :=
291 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
292 intro r hr
293 have hrImage :
295 (f := ellipticQuotientGeneratorImage σ
297 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
299 simpa [e] using
302 (f := ellipticQuotientGeneratorImage σ
304 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
306 (y := r)).1 hr
307 rcases hrImage with ⟨t, ht, r₀, hr₀, hval⟩
308 have htPower : ∃ k : Fin p, t = (FreeGroup.of x) ^ k.val := by
309 simpa [T] using
310 (mem_range_cyclicQuotientRightRep_iff_generatorPower φ (x := x) hx).1 ht
311 rcases htPower with ⟨k, rfl⟩
312 let tPow : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ k.val
313 have relator_eq :
314 r =
315 e.symm
316 (⟨tPow * r₀ * tPow⁻¹, by
317 change φ (tPow * r₀ * tPow⁻¹) = 1
318 have hrφ : φ r₀ = 1 := hrels r₀ hr₀
319 simp only [Lean.Elab.WF.paramLet, map_mul, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) := by
320 let zRel : φ.ker :=
321 ⟨tPow * r₀ * tPow⁻¹, by
322 change φ (tPow * r₀ * tPow⁻¹) = 1
323 have hrφ : φ r₀ = 1 := hrels r₀ hr₀
325 have hz : e r = zRel := by
326 apply Subtype.ext
327 simpa [tPow, zRel] using hval
328 calc
329 r = e.symm (e r) := by simp only [MulEquiv.symm_apply_apply]
330 _ = e.symm zRel := by rw [hz]
331 rcases hr₀ with ⟨i, rfl⟩ | rfl
332 · by_cases h0 : i.val = 0
333 · have hi :
334 i =
336 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
337 ext
338 simpa [firstReductionCanonicalSourceZeroIndex] using h0
339 subst i
340 rw [relator_eq]
341 simpa [σ, τ, φ, e, η, x, tPow] using hFirst k
342 · by_cases h1 : i.val = 1
343 · have hi :
344 i =
346 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
347 ext
348 simpa [firstReductionCanonicalSourceOneIndex] using h1
349 subst i
350 rw [relator_eq]
351 simpa [σ, τ, φ, e, η, x, tPow] using hSecond k
352 · let j : Fin tailLen := ⟨i.val - 2, by
353 have hi_lt : i.val < 2 + tailLen := by
354 change i.val < 2 + tailLen
355 exact i.isLt
356 omega⟩
357 have hiTail :
358 i =
360 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j := by
361 ext
362 simp only [firstReductionCanonicalSourceTailIndex, j]
363 omega
364 rw [relator_eq]
365 simpa [σ, τ, φ, e, η, x, tPow, hiTail] using hTail j k
366 · rw [relator_eq]
367 simpa [σ, τ, φ, e, η, x, tPow] using hTotal k
369 {tailLen p : ℕ}
370 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
371 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
372 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
373 (k : Fin p) :
374 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
375 let σ :=
376 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
377 let τ :=
378 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
379 let φ :=
381 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
382 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
383 let e :=
385 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
386 let η :=
388 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
389 let x : FuchsianGenerator σ :=
391 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
392 let i₀ :=
394 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
395 η
396 (e.symm
398 ((FreeGroup.of x) ^ k.val)⁻¹, by
399 change φ
401 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
402 have hrφ :
405 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
407 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
409 classical
410 dsimp
411 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
412 let σ :=
413 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
414 let τ :=
415 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
416 let φ :=
418 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
419 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
420 let e :=
422 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
423 let η :=
425 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
426 let x : FuchsianGenerator σ :=
428 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
429 let i₀ :=
431 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
432 let a :=
434 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
435 let z : φ.ker :=
437 ((FreeGroup.of x) ^ k.val)⁻¹, by
438 change φ
440 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
443 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
446 have hz : z = a ^ m₁' := by
447 apply Subtype.ext
448 change
449 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
451 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
452 ((a ^ m₁' : φ.ker) : FreeGroup (FuchsianGenerator σ))
453 rw [show ((a ^ m₁' : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
454 ((a : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ m₁' by
455 exact (map_pow (φ.ker.subtype) a m₁')]
457 simp only [firstReductionCanonicalSourceSignature, firstReductionCanonicalDistinguishedGenerator,
458 firstReductionCanonicalSourceZeroIndex, Fin.mk_zero', xWord, firstReductionCanonicalSourcePeriod,
459 Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceDIte, pow_mul, x, i₀, σ]
460 group
461 have hmain :=
463 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
465 rw [hz, map_pow]
466 simpa [σ, τ, φ, e, η, a] using hmain
468 {tailLen p : ℕ}
469 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
470 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
471 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
472 (k : Fin p) :
473 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
474 let σ :=
475 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
476 let φ :=
478 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
479 let x : FuchsianGenerator σ :=
481 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
482 let y : FuchsianGenerator σ :=
483 FuchsianGenerator.elliptic
485 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
486 let edge : Fin p → φ.ker :=
488 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
489 let lower :=
490 (List.ofFn (fun i : Fin k.val => edge ⟨k.val - i.val, by omega⟩)).prod
491 let wrap := edge ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩
492 let upper :=
493 (List.ofFn (fun i : Fin (p - 1 - k.val) => edge ⟨p - 1 - i.val, by omega⟩)).prod
494 lower * wrap * upper =
495 (⟨(FreeGroup.of x) ^ k.val * (FreeGroup.of y) ^ p *
496 ((FreeGroup.of x) ^ k.val)⁻¹, by
497 rw [MonoidHom.mem_ker]
498 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
499 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
500 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
501 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
502 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
503 firstReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
504 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
506 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
507 simp only [ofAdd_neg, inv_pow, mul_inv_cancel_comm, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul,
508 CharP.cast_eq_zero, mul_one, neg_zero, toAdd_one]⟩ : φ.ker) := by
509 classical
510 dsimp
511 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
512 let σ :=
513 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
514 let φ :=
516 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
517 let x : FuchsianGenerator σ :=
519 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
520 let y : FuchsianGenerator σ :=
521 FuchsianGenerator.elliptic
523 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
524 let edge : Fin p → φ.ker :=
526 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
527 let lower :=
528 (List.ofFn (fun i : Fin k.val => edge ⟨k.val - i.val, by omega⟩)).prod
529 let wrap := edge ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩
530 let upper :=
531 (List.ofFn (fun i : Fin (p - 1 - k.val) => edge ⟨p - 1 - i.val, by omega⟩)).prod
532 apply Subtype.ext
533 change
534 ((lower * wrap * upper : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
535 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
536 (FreeGroup.of y) ^ p *
537 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹
538 have hlowerCoe :
539 ((lower : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
540 (List.ofFn (fun i : Fin k.val =>
541 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (k.val - i.val) *
542 FreeGroup.of y *
543 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
544 (k.val - 1 - i.val))⁻¹)).prod := by
545 change
546 φ.ker.subtype lower =
547 (List.ofFn (fun i : Fin k.val =>
548 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (k.val - i.val) *
549 FreeGroup.of y *
550 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
551 (k.val - 1 - i.val))⁻¹)).prod
552 simp only [Subgroup.subtype_apply, Subgroup.val_list_prod, List.map_ofFn, lower, edge]
553 apply congrArg List.prod
554 apply List.ofFn_inj.2
555 funext i
556 let i' : Fin (p - 1) := ⟨k.val - 1 - i.val, by omega⟩
557 have hidx :
558 (⟨i'.val + 1, by omega⟩ : Fin p) = ⟨k.val - i.val, by omega⟩ := by
559 ext
560 simp only [i']
561 omega
562 have hs : k.val - 1 - i.val + 1 = k.val - i.val := by omega
563 simpa [σ, φ, x, y, edge, i', hidx, hs] using
565 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i'
566 have hwrapCoe :
567 ((wrap : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
568 FreeGroup.of y *
569 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (p - 1))⁻¹ := by
570 simpa [σ, φ, x, y, edge, wrap] using
572 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
573 have hupperCoe :
574 ((upper : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
575 (List.ofFn (fun i : Fin (p - 1 - k.val) =>
576 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (p - 1 - i.val) *
577 FreeGroup.of y *
578 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
579 (p - 1 - 1 - i.val))⁻¹)).prod := by
580 change
581 φ.ker.subtype upper =
582 (List.ofFn (fun i : Fin (p - 1 - k.val) =>
583 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (p - 1 - i.val) *
584 FreeGroup.of y *
585 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
586 (p - 1 - 1 - i.val))⁻¹)).prod
587 simp only [Subgroup.subtype_apply, Subgroup.val_list_prod, List.map_ofFn, upper, edge]
588 apply congrArg List.prod
589 apply List.ofFn_inj.2
590 funext i
591 let i' : Fin (p - 1) := ⟨i.val, by omega⟩
592 simpa [σ, φ, x, y, edge, i'] using
594 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i'
595 change
596 ((lower : φ.ker) : FreeGroup (FuchsianGenerator σ)) *
597 ((wrap : φ.ker) : FreeGroup (FuchsianGenerator σ)) *
598 ((upper : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
599 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
600 (FreeGroup.of y) ^ p *
601 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹
602 rw [hlowerCoe, hwrapCoe, hupperCoe]
603 rw [negOneCycleSegmentProduct_eq (FreeGroup.of x) (FreeGroup.of y) k.val k.val
604 (by omega)]
605 rw [negOneCycleSegmentProduct_eq (FreeGroup.of x) (FreeGroup.of y)
606 (p - 1) (p - 1 - k.val) (by omega)]
607 have hkk : k.val - k.val = 0 := by omega
608 have hlast : p - 1 - (p - 1 - k.val) = k.val := by omega
609 rw [hkk, hlast]
610 simp only [pow_zero, inv_one, mul_one]
611 have hkadd : k.val + 1 + (p - 1 - k.val) = p := by omega
612 calc
613 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
614 (FreeGroup.of y) ^ k.val *
615 (FreeGroup.of y * ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (p - 1))⁻¹) *
616 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (p - 1) *
617 (FreeGroup.of y) ^ (p - 1 - k.val) *
618 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹)
619 =
620 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
621 ((FreeGroup.of y) ^ k.val * FreeGroup.of y *
622 (FreeGroup.of y) ^ (p - 1 - k.val)) *
623 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ := by
624 group
625 _ =
626 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
627 (FreeGroup.of y) ^ p *
628 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ := by
629 rw [← pow_succ (FreeGroup.of y) k.val]
630 rw [← pow_add (FreeGroup.of y) (k.val + 1) (p - 1 - k.val)]
631 rw [hkadd]
633 {tailLen p : ℕ}
634 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
635 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
636 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
637 (k : Fin p) :
638 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
639 let σ :=
640 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
641 let τ :=
642 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
643 let φ :=
645 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
646 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
647 let e :=
649 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
650 let η :=
652 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
653 let x : FuchsianGenerator σ :=
655 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
656 let i₁ :=
658 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
659 η
660 (e.symm
662 ((FreeGroup.of x) ^ k.val)⁻¹, by
663 change φ
665 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
666 have hrφ :
669 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
671 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
673 classical
674 dsimp
675 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
676 let σ :=
677 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
678 let τ :=
679 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
680 let φ :=
682 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
683 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
684 let e :=
686 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
687 let η :=
689 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
690 let x : FuchsianGenerator σ :=
692 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
693 let i₁ :=
695 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
696 let y : FuchsianGenerator σ := FuchsianGenerator.elliptic i₁
697 let edge : Fin p → φ.ker :=
699 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
700 let lower :=
701 (List.ofFn (fun i : Fin k.val => edge ⟨k.val - i.val, by omega⟩)).prod
702 let wrap := edge ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩
703 let upper :=
704 (List.ofFn (fun i : Fin (p - 1 - k.val) => edge ⟨p - 1 - i.val, by omega⟩)).prod
705 let cycle := lower * wrap * upper
706 let base :=
708 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
709 let z : φ.ker :=
711 ((FreeGroup.of x) ^ k.val)⁻¹, by
712 change φ
714 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
717 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
720 have hcycleSource :
721 cycle =
722 (⟨(FreeGroup.of x) ^ k.val * (FreeGroup.of y) ^ p *
723 ((FreeGroup.of x) ^ k.val)⁻¹, by
724 rw [MonoidHom.mem_ker]
725 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
726 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
727 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
728 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
729 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
730 firstReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
731 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y, i₁]
733 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
734 simp only [ofAdd_neg, inv_pow, mul_inv_cancel_comm, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul,
735 CharP.cast_eq_zero, mul_one, neg_zero, toAdd_one]⟩ : φ.ker) := by
736 simpa [σ, φ, x, y, i₁, edge, lower, wrap, upper, cycle] using
738 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k
739 have hz : z = cycle ^ m₂' := by
740 apply Subtype.ext
741 change
742 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
744 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
745 ((cycle ^ m₂' : φ.ker) : FreeGroup (FuchsianGenerator σ))
746 rw [show ((cycle ^ m₂' : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
747 ((cycle : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ m₂' by
748 exact (map_pow (φ.ker.subtype) cycle m₂')]
749 have hcycleCoe :=
750 congrArg (fun u : φ.ker => (u : FreeGroup (FuchsianGenerator σ))) hcycleSource
751 have hcycleCoe' :
752 ((cycle : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
753 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
754 (FreeGroup.of y) ^ p *
755 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ := by
756 simpa using hcycleCoe
757 rw [hcycleCoe']
758 simp only [firstReductionCanonicalSourceSignature, firstReductionCanonicalDistinguishedGenerator, xWord,
759 firstReductionCanonicalSourceOneIndex, firstReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte, pow_mul,
760 conj_pow, x, i₁, y, σ]
762 have hmain :=
764 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
765 have hmain' :
767 simpa [σ, τ, φ, e, η, base] using hmain
768 rw [map_pow] at hmain'
769 simpa using hmain'
770 have htailSplit :
771 (List.ofFn (fun i : Fin (p - 1) => edge ⟨p - 1 - i.val, by omega⟩)).prod =
772 upper * lower := by
773 have hlist := list_ofFn_desc_split (p := p) (k := k.val) k.isLt edge
774 simpa [upper, lower] using congrArg List.prod hlist
775 have hbaseEq : base = (wrap * upper) * lower := by
776 have hdesc :
777 wrap *
778 (List.ofFn (fun i : Fin (p - 1) =>
779 edge ⟨p - 1 - i.val, by omega⟩)).prod =
780 base := by
781 simpa [σ, φ, edge, wrap, base] using
783 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
784 rw [htailSplit] at hdesc
785 calc
786 base = wrap * (upper * lower) := hdesc.symm
787 _ = (wrap * upper) * lower := by group
788 let a := η (e.symm (wrap * upper))
789 let b := η (e.symm lower)
791 rw [hbaseEq] at hbasePower
793 have hrot :
795 ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_pow_mem_normalClosure
797 have hcycleTarget :
799 have hcycleImage : η (e.symm cycle) = b * a := by
801 simpa [hcycleImage] using hrot
803 rw [hz, map_pow]
804 simpa [cycle] using hcycleTarget
806 {tailLen p : ℕ}
807 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
808 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
809 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
810 (j : Fin tailLen) (k : Fin p) :
811 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
812 let σ :=
813 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
814 let τ :=
815 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
816 let φ :=
818 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
819 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
820 let e :=
822 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
823 let η :=
825 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
826 let x : FuchsianGenerator σ :=
828 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
829 let iTail :=
831 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
832 η
833 (e.symm
835 ((FreeGroup.of x) ^ k.val)⁻¹, by
836 change φ
838 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
839 have hrφ :
842 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
844 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
846 classical
847 dsimp
848 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
849 let σ :=
850 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
851 let τ :=
852 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
853 let φ :=
855 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
856 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
857 let e :=
859 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
860 let η :=
862 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
863 let x : FuchsianGenerator σ :=
865 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
866 let iTail :=
868 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
869 let c :=
871 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k
872 let z : φ.ker :=
874 ((FreeGroup.of x) ^ k.val)⁻¹, by
875 change φ
877 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
880 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
883 have hz : z = c ^ tail j := by
884 apply Subtype.ext
885 change
886 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
888 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
889 ((c ^ tail j : φ.ker) : FreeGroup (FuchsianGenerator σ))
890 rw [show ((c ^ tail j : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
891 ((c : φ.ker) : FreeGroup (FuchsianGenerator σ)) ^ tail j by
892 exact (map_pow (φ.ker.subtype) c (tail j))]
894 have htailOne : 2 + j.val ≠ 1 := by omega
895 simp only [firstReductionCanonicalSourceSignature, firstReductionCanonicalDistinguishedGenerator, xWord,
896 firstReductionCanonicalSourceTailIndex, firstReductionCanonicalSourcePeriod, Nat.add_eq_zero_iff,
897 OfNat.ofNat_ne_zero, false_and, ↓reduceDIte, htailOne, add_tsub_cancel_left, Fin.eta, conj_pow, x, iTail, σ]
898 have hmain :=
900 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k
902 rw [hz, map_pow]
903 simpa [σ, τ, φ, e, η, c] using hmain
905 {tailLen p : ℕ}
906 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
907 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
908 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
909 (k : Fin p) :
910 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
911 let σ :=
912 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
913 let τ :=
914 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
915 let φ :=
917 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
918 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
919 let e :=
921 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
922 let η :=
924 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
925 let x : FuchsianGenerator σ :=
927 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
928 η
929 (e.symm
930 (⟨(FreeGroup.of x) ^ k.val * totalRelation σ *
931 ((FreeGroup.of x) ^ k.val)⁻¹, by
932 change φ
933 ((FreeGroup.of x) ^ k.val * totalRelation σ *
934 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
935 have hrφ : φ (totalRelation σ) = 1 :=
937 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
938 (totalRelation σ) (Or.inr rfl)
939 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
941 classical
942 dsimp
943 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
944 let σ :=
945 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
946 let τ :=
947 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
948 let φ :=
950 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
951 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
952 let e :=
954 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
955 let η :=
957 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
958 let x : FuchsianGenerator σ :=
960 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
961 let z : φ.ker :=
962 ⟨(FreeGroup.of x) ^ k.val * totalRelation σ *
963 ((FreeGroup.of x) ^ k.val)⁻¹, by
964 change φ
965 ((FreeGroup.of x) ^ k.val * totalRelation σ *
966 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
967 have hrφ : φ (totalRelation σ) = 1 :=
969 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
970 (totalRelation σ) (Or.inr rfl)
973 by_cases hlast : k.val = p - 1
974 · let y : FuchsianGenerator σ :=
975 FuchsianGenerator.elliptic
977 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
978 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
979 FuchsianGenerator.elliptic
981 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
982 let kLast : Fin p := ⟨p - 1, by omega⟩
983 let kZero : Fin p := ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩
984 let t : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ k.val
985 let r : FreeGroup (FuchsianGenerator σ) := totalRelation σ
986 have hprodCoe :
987 (((List.ofFn (fun j : Fin tailLen =>
989 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod : φ.ker) :
990 FreeGroup (FuchsianGenerator σ)) =
991 (List.ofFn (fun j : Fin tailLen =>
993 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast : φ.ker) :
994 FreeGroup (FuchsianGenerator σ)))).prod := by
995 change
996 φ.ker.subtype
997 ((List.ofFn (fun j : Fin tailLen =>
999 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod) =
1000 (List.ofFn (fun j : Fin tailLen =>
1001 φ.ker.subtype
1003 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast))).prod
1004 rw [map_list_prod, List.map_ofFn]
1005 rfl
1006 have htailList :
1007 (List.ofFn (fun j : Fin tailLen =>
1009 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast : φ.ker) :
1010 FreeGroup (FuchsianGenerator σ)))) =
1011 List.ofFn (fun j : Fin tailLen =>
1012 (FreeGroup.of x) ^ (p - 1) * FreeGroup.of (tailGen j) *
1013 ((FreeGroup.of x) ^ (p - 1))⁻¹) := by
1014 apply List.ofFn_inj.2
1015 funext j
1016 simpa [σ, φ, x, tailGen, kLast] using
1018 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast
1019 have htailConj :
1020 (List.ofFn (fun j : Fin tailLen =>
1021 (FreeGroup.of x) ^ (p - 1) * FreeGroup.of (tailGen j) *
1022 ((FreeGroup.of x) ^ (p - 1))⁻¹)).prod =
1023 (FreeGroup.of x) ^ (p - 1) *
1024 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
1025 ((FreeGroup.of x) ^ (p - 1))⁻¹ := by
1026 calc
1027 (List.ofFn (fun j : Fin tailLen =>
1028 (FreeGroup.of x) ^ (p - 1) * FreeGroup.of (tailGen j) *
1029 ((FreeGroup.of x) ^ (p - 1))⁻¹)).prod =
1030 (List.map
1031 (fun u =>
1032 (FreeGroup.of x) ^ (p - 1) * u *
1033 ((FreeGroup.of x) ^ (p - 1))⁻¹)
1034 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))).prod := by
1035 rw [List.map_ofFn]
1036 rfl
1037 _ =
1038 (FreeGroup.of x) ^ (p - 1) *
1039 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
1040 ((FreeGroup.of x) ^ (p - 1))⁻¹ := by
1041 rw [← ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod
1042 ((FreeGroup.of x) ^ (p - 1))
1043 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))]
1044 have hkerEq :
1045 z =
1047 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen *
1049 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero *
1050 (List.ofFn (fun j : Fin tailLen =>
1052 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod := by
1053 apply Subtype.ext
1054 change
1055 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val * totalRelation σ *
1056 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
1058 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen : φ.ker) :
1059 FreeGroup (FuchsianGenerator σ)) *
1061 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero : φ.ker) :
1062 FreeGroup (FuchsianGenerator σ)) *
1063 (((List.ofFn (fun j : Fin tailLen =>
1065 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod : φ.ker) :
1066 FreeGroup (FuchsianGenerator σ))
1067 rw [hprodCoe, htailList, htailConj]
1070 have hTotal :=
1072 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1073 rw [hTotal]
1075 firstReductionCanonicalDistinguishedGenerator, mul_assoc]
1076 rw [hlast]
1077 rw [← mul_assoc]
1078 rw [← pow_succ]
1079 have hsuccNat : p - 1 + 1 = p := by
1080 omega
1081 rw [hsuccNat]
1082 group
1083 have htailMap :
1084 e.symm
1085 ((List.ofFn (fun j : Fin tailLen =>
1087 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod) =
1088 (List.ofFn (fun j : Fin tailLen =>
1089 e.symm
1091 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast))).prod := by
1092 rw [map_list_prod, List.map_ofFn]
1093 rfl
1094 have hmap :
1095 e.symm
1097 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen *
1099 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero *
1100 (List.ofFn (fun j : Fin tailLen =>
1102 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod) =
1103 e.symm
1105 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
1106 e.symm
1108 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero) *
1109 (List.ofFn (fun j : Fin tailLen =>
1110 e.symm
1112 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast))).prod := by
1114 let tailWord :=
1115 (List.ofFn (fun j : Fin tailLen =>
1116 e.symm
1118 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast))).prod
1119 let firstWord :=
1120 e.symm
1122 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1123 let secondWord :=
1124 e.symm
1126 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero)
1127 have hwrap :=
1129 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1130 have hwrap' : η tailWord * η firstWord * η secondWord = 1 := by
1132 have hrot : η firstWord * η secondWord * η tailWord = 1 :=
1133 cyclic_rotate_three_eq_one hwrap'
1134 rw [hkerEq, hmap]
1137 rw [hrot]
1138 exact Subgroup.one_mem _
1139 · let y : FuchsianGenerator σ :=
1140 FuchsianGenerator.elliptic
1142 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1143 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1144 FuchsianGenerator.elliptic
1146 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1147 let knw : Fin (p - 1) := ⟨k.val, by omega⟩
1148 let k0 : Fin p := ⟨knw.val, by omega⟩
1149 let k1 : Fin p := ⟨knw.val + 1, by omega⟩
1150 let t : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ k.val
1151 let r : FreeGroup (FuchsianGenerator σ) := totalRelation σ
1152 have hprodCoe :
1153 (((List.ofFn (fun j : Fin tailLen =>
1155 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod : φ.ker) :
1156 FreeGroup (FuchsianGenerator σ)) =
1157 (List.ofFn (fun j : Fin tailLen =>
1159 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0 : φ.ker) :
1160 FreeGroup (FuchsianGenerator σ)))).prod := by
1161 change
1162 φ.ker.subtype
1163 ((List.ofFn (fun j : Fin tailLen =>
1165 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod) =
1166 (List.ofFn (fun j : Fin tailLen =>
1167 φ.ker.subtype
1169 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0))).prod
1170 rw [map_list_prod, List.map_ofFn]
1171 rfl
1172 have htailList :
1173 (List.ofFn (fun j : Fin tailLen =>
1175 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0 : φ.ker) :
1176 FreeGroup (FuchsianGenerator σ)))) =
1177 List.ofFn (fun j : Fin tailLen =>
1178 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
1179 ((FreeGroup.of x) ^ k.val)⁻¹) := by
1180 apply List.ofFn_inj.2
1181 funext j
1182 simpa [σ, φ, x, tailGen, k0, knw] using
1184 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0
1185 have htailConj :
1186 (List.ofFn (fun j : Fin tailLen =>
1187 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
1188 ((FreeGroup.of x) ^ k.val)⁻¹)).prod =
1189 (FreeGroup.of x) ^ k.val *
1190 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
1191 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1192 calc
1193 (List.ofFn (fun j : Fin tailLen =>
1194 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
1195 ((FreeGroup.of x) ^ k.val)⁻¹)).prod =
1196 (List.map
1197 (fun u =>
1198 (FreeGroup.of x) ^ k.val * u * ((FreeGroup.of x) ^ k.val)⁻¹)
1199 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))).prod := by
1200 rw [List.map_ofFn]
1201 rfl
1202 _ =
1203 (FreeGroup.of x) ^ k.val *
1204 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
1205 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1206 rw [← ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod
1207 ((FreeGroup.of x) ^ k.val)
1208 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))]
1209 have hkerEq :
1210 z =
1212 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1 *
1213 (List.ofFn (fun j : Fin tailLen =>
1215 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod := by
1216 apply Subtype.ext
1217 change
1218 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val * totalRelation σ *
1219 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
1221 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1 : φ.ker) :
1222 FreeGroup (FuchsianGenerator σ)) *
1223 (((List.ofFn (fun j : Fin tailLen =>
1225 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod : φ.ker) :
1226 FreeGroup (FuchsianGenerator σ))
1227 rw [hprodCoe, htailList, htailConj]
1229 have hTotal :=
1231 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1232 rw [hTotal]
1234 firstReductionCanonicalDistinguishedGenerator, mul_assoc]
1235 simp only [inv_mul_cancel_left, knw]
1236 group
1237 have hmap :
1238 e.symm
1240 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1 *
1241 (List.ofFn (fun j : Fin tailLen =>
1243 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod) =
1244 e.symm
1246 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1) *
1247 (List.ofFn (fun j : Fin tailLen =>
1248 e.symm
1250 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0))).prod := by
1252 rfl
1253 have hnonwrap :=
1255 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen knw
1256 have hEqOne :
1257 η
1258 (e.symm
1260 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1) *
1261 (List.ofFn (fun j : Fin tailLen =>
1262 e.symm
1264 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0))).prod) = 1 := by
1265 simpa [σ, τ, e, η, knw, k0, k1] using hnonwrap
1266 rw [hkerEq, hmap]
1267 rw [hEqOne]
1268 exact Subgroup.one_mem _
1269private theorem firstReductionCanonicalSchreierToTarget_mapsRelators
1270 {tailLen p : ℕ}
1271 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1272 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1273 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1274 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1275 let σ :=
1276 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1277 let τ :=
1278 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1279 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1280 let φ :=
1282 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1283 let x : FuchsianGenerator σ :=
1285 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1286 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1287 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
1288 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
1289 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1290 let hT : IsRightSchreierTransversal φ.ker T :=
1292 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1294 let η :=
1296 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1297 ∀ r ∈
1300 (f := ellipticQuotientGeneratorImage σ
1302 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
1306 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1308 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1310 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1312 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1314 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1315noncomputable def firstReductionCanonicalForwardMapData
1316 {tailLen p : ℕ}
1317 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1318 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1319 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1321 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen :=
1323 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1324 (by
1325 simpa [firstReductionCanonicalDistinguishedGenerator] using
1327 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1328noncomputable def firstReductionCanonicalKernelEquiv
1329 {tailLen p : ℕ}
1330 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1331 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1332 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :=
1334 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1336 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1337end FenchelNielsen