Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/TransportMaps.lean
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/TransportMaps/Source

FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/TransportMaps.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.QuotientAndBasis
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/TransportMaps.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# First compact zero-genus reduction
14The first explicit finite quotient reduction for compact zero-genus Fuchsian presentations, including quotient maps, basis transport, signatures, and relator verification.
15-/
17namespace FenchelNielsen
19 {tailLen p : ℕ}
20 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
21 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
22 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
23 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
24 let σ :=
25 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
26 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
27 let hT :=
29 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
30 Set (FreeGroup ↥(schreierGeneratorSet hT)) :=
31 by
32 classical
33 exact
36 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
40 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
42 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
43 (rels := relators
45 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
47 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
49 {tailLen p : ℕ}
50 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
51 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
52 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
53 (k : Fin (p - 1)) :
54 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
55 let σ :=
56 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
57 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
58 let e :=
60 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
61 e.symm
63 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
64 ⟨k.val + 1, by omega⟩) *
65 (List.ofFn (fun j : Fin tailLen =>
66 e.symm
68 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
69 ⟨k.val, by omega⟩))).prod ∈
70 Subgroup.normalClosure
72 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
73 classical
74 dsimp
75 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
76 let σ :=
77 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
78 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
79 let φ :=
81 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
82 let x : FuchsianGenerator σ :=
84 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
85 let y : FuchsianGenerator σ :=
86 FuchsianGenerator.elliptic
88 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
89 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
90 FuchsianGenerator.elliptic
92 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
93 let T :=
95 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
96 let hT :=
98 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
99 let e :=
101 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
102 let hrels :=
104 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
105 let k0 : Fin p := ⟨k.val, by omega⟩
106 let k1 : Fin p := ⟨k.val + 1, by omega⟩
107 let t : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ k.val
108 let r : FreeGroup (FuchsianGenerator σ) := totalRelation σ
109 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
110 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
111 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
112 have ht : t ∈ T := by
115 φ x hx (m := k.val) (by omega)
116 have hr : r ∈ relators σ := by
117 exact Or.inr rfl
118 have hrel :
119 e.symm
120 (⟨t * r * t⁻¹, by
121 change φ (t * r * t⁻¹) = 1
122 have hrφ : φ r = 1 := hrels r hr
123 simp only [Lean.Elab.WF.paramLet, map_mul, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) ∈
124 Subgroup.normalClosure
126 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
127 have h :=
129 hrels e ht hr
131 have hprodCoe :
132 (((List.ofFn (fun j : Fin tailLen =>
134 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod : φ.ker) :
135 FreeGroup (FuchsianGenerator σ)) =
136 (List.ofFn (fun j : Fin tailLen =>
138 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0 : φ.ker) :
139 FreeGroup (FuchsianGenerator σ)))).prod := by
140 change
141 φ.ker.subtype
142 ((List.ofFn (fun j : Fin tailLen =>
144 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod) =
145 (List.ofFn (fun j : Fin tailLen =>
146 φ.ker.subtype
148 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0))).prod
149 rw [map_list_prod, List.map_ofFn]
150 rfl
151 have htailList :
152 (List.ofFn (fun j : Fin tailLen =>
154 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0 : φ.ker) :
155 FreeGroup (FuchsianGenerator σ)))) =
156 List.ofFn (fun j : Fin tailLen =>
157 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
158 ((FreeGroup.of x) ^ k.val)⁻¹) := by
159 apply List.ofFn_inj.2
160 funext j
161 simpa [σ, φ, x, tailGen, k0] using
163 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0
164 have htailConj :
165 (List.ofFn (fun j : Fin tailLen =>
166 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
167 ((FreeGroup.of x) ^ k.val)⁻¹)).prod =
168 (FreeGroup.of x) ^ k.val *
169 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
170 ((FreeGroup.of x) ^ k.val)⁻¹ := by
171 calc
172 (List.ofFn (fun j : Fin tailLen =>
173 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
174 ((FreeGroup.of x) ^ k.val)⁻¹)).prod =
175 (List.map
176 (fun u =>
177 (FreeGroup.of x) ^ k.val * u * ((FreeGroup.of x) ^ k.val)⁻¹)
178 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))).prod := by
179 rw [List.map_ofFn]
180 rfl
181 _ =
182 (FreeGroup.of x) ^ k.val *
183 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
184 ((FreeGroup.of x) ^ k.val)⁻¹ := by
185 rw [← ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod
186 ((FreeGroup.of x) ^ k.val)
187 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))]
188 have hkerEq :
189 (⟨t * r * t⁻¹, by
190 change φ (t * r * t⁻¹) = 1
191 have hrφ : φ r = 1 := hrels r hr
192 simp only [Lean.Elab.WF.paramLet, map_mul, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) =
194 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1 *
195 (List.ofFn (fun j : Fin tailLen =>
197 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod := by
198 apply Subtype.ext
199 change
200 t * r * t⁻¹ =
202 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1 : φ.ker) :
203 FreeGroup (FuchsianGenerator σ)) *
204 (((List.ofFn (fun j : Fin tailLen =>
206 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod : φ.ker) :
207 FreeGroup (FuchsianGenerator σ))
208 rw [hprodCoe, htailList, htailConj]
210 have hTotal :=
212 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
213 dsimp [r]
214 rw [hTotal]
215 simp only [t, x, tailGen, xWord,
217 group
218 have hmap :
219 e.symm
221 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1 *
222 (List.ofFn (fun j : Fin tailLen =>
224 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod) =
225 e.symm
227 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1) *
228 (List.ofFn (fun j : Fin tailLen =>
229 e.symm
231 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0))).prod := by
232 rw [map_mul, map_list_prod, List.map_ofFn]
233 rfl
234 have hrel' :
235 e.symm
237 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k1 *
238 (List.ofFn (fun j : Fin tailLen =>
240 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k0)).prod) ∈
241 Subgroup.normalClosure
243 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
244 simpa [hkerEq] using hrel
245 simpa [k0, k1, hmap] using hrel'
247 {tailLen p : ℕ}
248 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
249 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
250 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
251 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
252 let σ :=
253 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
254 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
255 let e :=
257 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
258 e.symm
260 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
261 e.symm
263 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
264 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩) *
265 (List.ofFn (fun j : Fin tailLen =>
266 e.symm
268 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
269 ⟨p - 1, by omega⟩))).prod ∈
270 Subgroup.normalClosure
272 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
273 classical
274 dsimp
275 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
276 let σ :=
277 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
278 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
279 let φ :=
281 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
282 let x : FuchsianGenerator σ :=
284 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
285 let y : FuchsianGenerator σ :=
286 FuchsianGenerator.elliptic
288 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
289 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
290 FuchsianGenerator.elliptic
292 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
293 let T :=
295 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
296 let hT :=
298 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
299 let e :=
301 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
302 let hrels :=
304 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
305 let kLast : Fin p := ⟨p - 1, by omega⟩
306 let kZero : Fin p := ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩
307 let t : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ (p - 1)
308 let r : FreeGroup (FuchsianGenerator σ) := totalRelation σ
309 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
310 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
311 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
312 have ht : t ∈ T := by
315 φ x hx (m := p - 1) (by omega)
316 have hr : r ∈ relators σ := by
317 exact Or.inr rfl
318 have hrel :
319 e.symm
320 (⟨t * r * t⁻¹, by
321 change φ (t * r * t⁻¹) = 1
322 have hrφ : φ r = 1 := hrels r hr
323 simp only [Lean.Elab.WF.paramLet, map_mul, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) ∈
324 Subgroup.normalClosure
326 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
327 have h :=
329 hrels e ht hr
331 have hprodCoe :
332 (((List.ofFn (fun j : Fin tailLen =>
334 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod : φ.ker) :
335 FreeGroup (FuchsianGenerator σ)) =
336 (List.ofFn (fun j : Fin tailLen =>
338 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast : φ.ker) :
339 FreeGroup (FuchsianGenerator σ)))).prod := by
340 change
341 φ.ker.subtype
342 ((List.ofFn (fun j : Fin tailLen =>
344 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod) =
345 (List.ofFn (fun j : Fin tailLen =>
346 φ.ker.subtype
348 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast))).prod
349 rw [map_list_prod, List.map_ofFn]
350 rfl
351 have htailList :
352 (List.ofFn (fun j : Fin tailLen =>
354 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast : φ.ker) :
355 FreeGroup (FuchsianGenerator σ)))) =
356 List.ofFn (fun j : Fin tailLen =>
357 (FreeGroup.of x) ^ (p - 1) * FreeGroup.of (tailGen j) *
358 ((FreeGroup.of x) ^ (p - 1))⁻¹) := by
359 apply List.ofFn_inj.2
360 funext j
361 simpa [σ, φ, x, tailGen, kLast] using
363 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast
364 have htailConj :
365 (List.ofFn (fun j : Fin tailLen =>
366 (FreeGroup.of x) ^ (p - 1) * FreeGroup.of (tailGen j) *
367 ((FreeGroup.of x) ^ (p - 1))⁻¹)).prod =
368 (FreeGroup.of x) ^ (p - 1) *
369 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
370 ((FreeGroup.of x) ^ (p - 1))⁻¹ := by
371 calc
372 (List.ofFn (fun j : Fin tailLen =>
373 (FreeGroup.of x) ^ (p - 1) * FreeGroup.of (tailGen j) *
374 ((FreeGroup.of x) ^ (p - 1))⁻¹)).prod =
375 (List.map
376 (fun u =>
377 (FreeGroup.of x) ^ (p - 1) * u *
378 ((FreeGroup.of x) ^ (p - 1))⁻¹)
379 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))).prod := by
380 rw [List.map_ofFn]
381 rfl
382 _ =
383 (FreeGroup.of x) ^ (p - 1) *
384 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod *
385 ((FreeGroup.of x) ^ (p - 1))⁻¹ := by
386 rw [← ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod
387 ((FreeGroup.of x) ^ (p - 1))
388 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j)))]
389 have hkerEq :
390 (⟨t * r * t⁻¹, by
391 change φ (t * r * t⁻¹) = 1
392 have hrφ : φ r = 1 := hrels r hr
393 simp only [Lean.Elab.WF.paramLet, map_mul, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) =
395 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen *
397 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero *
398 (List.ofFn (fun j : Fin tailLen =>
400 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod := by
401 apply Subtype.ext
402 change
403 t * r * t⁻¹ =
405 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen : φ.ker) :
406 FreeGroup (FuchsianGenerator σ)) *
408 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero : φ.ker) :
409 FreeGroup (FuchsianGenerator σ)) *
410 (((List.ofFn (fun j : Fin tailLen =>
412 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod : φ.ker) :
413 FreeGroup (FuchsianGenerator σ))
414 rw [hprodCoe, htailList, htailConj]
417 have hTotal :=
419 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
420 dsimp [r]
421 rw [hTotal]
422 simp only [t, x, tailGen, xWord,
424 rw [← mul_assoc]
425 rw [← pow_succ]
426 have hsuccNat : p - 1 + 1 = p := by
427 omega
428 rw [hsuccNat]
429 group
430 have htailMap :
431 e.symm
432 ((List.ofFn (fun j : Fin tailLen =>
434 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod) =
435 (List.ofFn (fun j : Fin tailLen =>
436 e.symm
438 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast))).prod := by
439 rw [map_list_prod, List.map_ofFn]
440 rfl
441 have hrel' :
442 e.symm
444 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen *
446 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen kZero *
447 (List.ofFn (fun j : Fin tailLen =>
449 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j kLast)).prod) ∈
450 Subgroup.normalClosure
452 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
453 simpa [hkerEq] using hrel
454 simpa [kLast, kZero, map_mul, htailMap, mul_assoc] using hrel'
456 {tailLen p : ℕ}
457 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
458 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
459 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
460 (k : Fin (p - 1)) :
461 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
462 let σ :=
463 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
464 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
465 let e :=
467 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
468 (List.ofFn (fun j : Fin tailLen =>
469 e.symm
471 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
472 ⟨k.val, by omega⟩))).prod *
473 e.symm
475 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
476 ⟨k.val + 1, by omega⟩) ∈
477 Subgroup.normalClosure
479 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
480 classical
481 dsimp
482 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
483 let σ :=
484 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
485 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
486 let e :=
488 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
489 have h :=
491 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k
492 simpa [σ, e, mul_assoc] using
493 (ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_mem_normalClosure
495 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
496 (a := e.symm
498 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
499 ⟨k.val + 1, by omega⟩))
500 (b := (List.ofFn (fun j : Fin tailLen =>
501 e.symm
503 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
504 ⟨k.val, by omega⟩))).prod)
505 h)
507 {tailLen p : ℕ}
508 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
509 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
510 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
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 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
515 let e :=
517 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
518 (List.ofFn (fun j : Fin tailLen =>
519 e.symm
521 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
522 ⟨p - 1, by omega⟩))).prod *
523 e.symm
525 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
526 e.symm
528 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
529 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩) ∈
530 Subgroup.normalClosure
532 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
533 classical
534 dsimp
535 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
536 let σ :=
537 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
538 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
539 let e :=
541 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
542 let a :=
543 e.symm
545 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
546 let b :=
547 e.symm
549 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
550 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩)
551 let c :=
552 (List.ofFn (fun j : Fin tailLen =>
553 e.symm
555 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
556 ⟨p - 1, by omega⟩))).prod
557 have habc : a * b * c ∈
558 Subgroup.normalClosure
560 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
561 simpa [σ, e, a, b, c, mul_assoc] using
563 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
564 have hbc_a : b * c * a ∈
565 Subgroup.normalClosure
567 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
568 have hrot :=
569 ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_mem_normalClosure
571 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
572 (a := a) (b := b * c)
573 (by simpa [mul_assoc] using habc)
574 simpa [mul_assoc] using hrot
575 have hca_b : c * a * b ∈
576 Subgroup.normalClosure
578 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
579 have hrot :=
580 ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_mem_normalClosure
582 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
583 (a := b) (b := c * a)
584 (by simpa [mul_assoc] using hbc_a)
585 simpa [mul_assoc] using hrot
586 simpa [a, b, c, mul_assoc] using hca_b
588 {tailLen p : ℕ}
589 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
590 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
591 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
592 let τ :=
593 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
594 let A :=
597 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
598 let B :=
601 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
602 let C :=
603 (List.ofFn (fun k : Fin p =>
604 (List.ofFn (fun j : Fin tailLen =>
607 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod
608 A⁻¹ * C⁻¹ * B⁻¹ ∈ Subgroup.normalClosure (relators τ) := by
609 classical
610 dsimp
611 let τ :=
612 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
613 let A :=
616 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
617 let B :=
620 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
621 let C :=
622 (List.ofFn (fun k : Fin p =>
623 (List.ofFn (fun j : Fin tailLen =>
626 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod
627 let N : Subgroup (FreeGroup (FuchsianGenerator τ)) :=
628 Subgroup.normalClosure (relators τ)
629 have htotal : A * B * C ∈ N := by
630 have hmem : totalRelation τ ∈ relators τ := Or.inr rfl
631 have hmemN : totalRelation τ ∈ N := Subgroup.subset_normalClosure hmem
632 have hTotal :=
634 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
635 simpa [N, τ, A, B, C, hTotal] using hmemN
636 have hinv : (A * B * C)⁻¹ ∈ N := N.inv_mem htotal
637 have hCBA : C⁻¹ * B⁻¹ * A⁻¹ ∈ N := by
638 simpa [N, mul_assoc] using hinv
639 have hBA_C : B⁻¹ * A⁻¹ * C⁻¹ ∈ N := by
640 have hrot :=
641 ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_mem_normalClosure
642 (R := relators τ) (a := C⁻¹) (b := B⁻¹ * A⁻¹)
643 (by simpa [N, mul_assoc] using hCBA)
644 simpa [N, mul_assoc] using hrot
645 have hA_CB : A⁻¹ * C⁻¹ * B⁻¹ ∈ N := by
646 have hrot :=
647 ReidemeisterSchreier.Discrete.Presentations.cyclic_rotation_mem_normalClosure
648 (R := relators τ) (a := B⁻¹) (b := A⁻¹ * C⁻¹)
649 (by simpa [N, mul_assoc] using hBA_C)
650 simpa [N, mul_assoc] using hrot
651 simpa [N, τ, A, B, C, mul_assoc] using hA_CB
653 {tailLen p : ℕ}
654 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
655 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
656 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
657 let τ :=
658 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
659 Fin p → FreeGroup (FuchsianGenerator τ) := by
660 classical
661 dsimp
662 let τ :=
663 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
664 intro k
665 exact
666 (List.ofFn (fun j : Fin tailLen =>
669 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod
671 {tailLen p : ℕ}
672 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
673 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
674 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
675 let τ :=
676 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
677 Fin p → FreeGroup (FuchsianGenerator τ) := by
678 classical
679 dsimp
680 let τ :=
681 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
682 let A :=
685 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
686 let block :=
688 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
689 intro k
690 if h0 : k.val = 0 then
691 exact block ⟨p - 1, by omega⟩ * A
692 else
693 exact block ⟨k.val - 1, by omega⟩
695 {tailLen p : ℕ}
696 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
697 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
698 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
699 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
700 let σ :=
701 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
702 let τ :=
703 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
704 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
705 let hT :=
707 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
708 ↥(schreierGeneratorSet hT) → FreeGroup (FuchsianGenerator τ) := by
709 classical
710 dsimp
711 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
712 let σ :=
713 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
714 let τ :=
715 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
716 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
717 let φ :=
719 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
720 let hT :=
722 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
723 let A :=
726 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
727 let secondWord :=
729 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
730 intro z
731 if hFirst :
732 (z : φ.ker) =
734 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen then
735 exact A⁻¹
736 else if hSecond :
737 ∃ k : Fin p,
738 (z : φ.ker) =
740 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k then
741 exact secondWord (Classical.choose hSecond)
742 else if hTail :
743 ∃ j : Fin tailLen, ∃ k : Fin p,
744 (z : φ.ker) =
746 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k then
747 let j : Fin tailLen := Classical.choose hTail
748 let hk : ∃ k : Fin p,
749 (z : φ.ker) =
751 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k :=
752 Classical.choose_spec hTail
753 let k : Fin p := Classical.choose hk
754 exact
757 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))⁻¹
758 else
759 exact 1
761 {tailLen p : ℕ}
762 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
763 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
764 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
765 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
766 let σ :=
767 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
768 let τ :=
769 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
770 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
771 let hT :=
773 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
774 FreeGroup ↥(schreierGeneratorSet hT) →* FreeGroup (FuchsianGenerator τ) :=
775 FreeGroup.lift
777 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
779 {tailLen p : ℕ}
780 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
781 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
782 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
783 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
784 let σ :=
785 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
786 let τ :=
787 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
788 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
789 let e :=
791 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
792 let η :=
794 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
795 η
796 (e.symm
798 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) =
801 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
802 classical
803 dsimp
804 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
805 let σ :=
806 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
807 let τ :=
808 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
809 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
810 let φ :=
812 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
813 let hT :=
815 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
816 let e :=
818 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
819 let η :=
821 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
822 let z : ↥(schreierGeneratorSet hT) :=
824 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen,
826 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen⟩
827 have hzWord :
828 e.symm
830 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
831 (FreeGroup.of z)⁻¹ := by
832 simpa [σ, φ, hT, e, z] using
834 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen z
835 have hFirst :
836 (z : φ.ker) =
838 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := rfl
839 have hzImage :
840 η (FreeGroup.of z) =
843 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))⁻¹ := by
844 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSchreierToTargetHom,
845 firstReductionCanonicalSchreierToTargetGeneratorImage, dite_eq_ite, id_eq, FreeGroup.lift_apply_of, ↓reduceIte, η,
846 z, τ, σ]
847 calc
848 η
849 (e.symm
851 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) =
852 η ((FreeGroup.of z)⁻¹) := by rw [hzWord]
853 _ = (η (FreeGroup.of z))⁻¹ := by simp only [Lean.Elab.WF.paramLet, map_inv]
854 _ =
855 ((xWord τ
857 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))⁻¹)⁻¹ := by
858 rw [hzImage]
859 _ =
862 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
863 simp only [inv_inv]
865 {tailLen p : ℕ}
866 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
867 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
868 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
869 (j : Fin tailLen) (k : Fin p) :
870 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
871 let σ :=
872 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
873 let τ :=
874 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
875 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
876 let e :=
878 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
879 let η :=
881 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
882 η
883 (e.symm
885 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k)) =
888 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j) := by
889 classical
890 dsimp
891 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
892 let σ :=
893 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
894 let τ :=
895 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
896 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
897 let φ :=
899 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
900 let hT :=
902 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
903 let e :=
905 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
906 let η :=
908 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
909 let x : FuchsianGenerator σ :=
911 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
912 let y : FuchsianGenerator σ :=
913 FuchsianGenerator.elliptic
915 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
916 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
917 FuchsianGenerator.elliptic
919 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
920 let z : ↥(schreierGeneratorSet hT) :=
922 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k,
924 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k⟩
925 have hzWord :
926 e.symm
928 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k) =
929 (FreeGroup.of z)⁻¹ := by
930 simpa [σ, φ, hT, e, z] using
932 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen z
933 have hxne : x ≠ tailGen j := by
934 intro hEq
936 firstReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, x, tailGen] at hEq
937 omega
938 have hyne : y ≠ tailGen j := by
939 intro hEq
941 FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, y, tailGen] at hEq
942 omega
943 have hFirst :
944 ¬ (z : φ.ker) =
946 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
947 intro hEq
948 have hval := congrArg
949 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
950 have hleft :
951 ((z : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
952 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
953 ((FreeGroup.of x) ^ k.val)⁻¹ := by
954 simpa [z, σ, φ, x, tailGen] using
956 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k
957 have hright :
959 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen : φ.ker) :
960 FreeGroup (FuchsianGenerator σ)) =
961 (FreeGroup.of x) ^ p := by
962 simpa [σ, φ, x] using
964 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
965 have hword :
966 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
967 FreeGroup.of (tailGen j) *
968 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
969 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ p := by
970 simpa [hleft, hright] using hval
971 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
972 fun u => if u = tailGen j then Multiplicative.ofAdd (1 : ℤ) else 1
973 have hmap := congrArg (FreeGroup.lift χ) hword
974 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
975 mul_one, ofAdd_eq_one, one_ne_zero, χ] at hmap
976 have hSecond :
977 ¬ ∃ k' : Fin p,
978 (z : φ.ker) =
980 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k' := by
981 intro h
982 rcases h with ⟨k', hEq⟩
983 have hval := congrArg
984 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
985 have hleft :
986 ((z : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
987 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
988 ((FreeGroup.of x) ^ k.val)⁻¹ := by
989 simpa [z, σ, φ, x, tailGen] using
991 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k
992 let r : ℕ := ((k'.val : ZMod p) - 1).val
993 have hright :
995 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k' : φ.ker) :
996 FreeGroup (FuchsianGenerator σ)) =
997 (FreeGroup.of x) ^ k'.val * FreeGroup.of y *
998 ((FreeGroup.of x) ^ r)⁻¹ := by
999 simp only [firstReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
1001 have hword :
1002 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
1003 FreeGroup.of (tailGen j) *
1004 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
1005 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k'.val *
1006 FreeGroup.of y *
1007 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r)⁻¹ := by
1008 simpa [hleft, hright] using hval
1009 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
1010 fun u => if u = tailGen j then Multiplicative.ofAdd (1 : ℤ) else 1
1011 have hmap := congrArg (FreeGroup.lift χ) hword
1012 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
1013 mul_one, hyne, ofAdd_eq_one, one_ne_zero, χ] at hmap
1014 have hTail :
1015 ∃ j' : Fin tailLen, ∃ k' : Fin p,
1016 (z : φ.ker) =
1018 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j' k' := ⟨j, k, rfl⟩
1019 let j' : Fin tailLen := Classical.choose hTail
1020 let hk' : ∃ k' : Fin p,
1021 (z : φ.ker) =
1023 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j' k' :=
1024 Classical.choose_spec hTail
1025 let k' : Fin p := Classical.choose hk'
1026 have hTailChoose :
1028 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k' j' =
1030 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j := by
1031 have hEqTail :
1033 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k =
1035 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j' k' := by
1036 simpa [z, j', hk', k'] using
1037 Classical.choose_spec hk'
1038 rcases
1040 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hEqTail with
1041 ⟨hj, hk⟩
1042 simp only [hk, hj]
1043 have hzImage :
1044 η (FreeGroup.of z) =
1047 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))⁻¹ := by
1048 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSchreierToTargetHom,
1049 firstReductionCanonicalSchreierToTargetGeneratorImage, dite_eq_ite, id_eq, FreeGroup.lift_apply_of, hFirst,
1050 ↓reduceIte, hSecond, ↓reduceDIte, hTail, hTailChoose, η, z, τ, σ, k', j']
1051 calc
1052 η
1053 (e.symm
1055 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k)) =
1056 η ((FreeGroup.of z)⁻¹) := by rw [hzWord]
1057 _ = (η (FreeGroup.of z))⁻¹ := by simp only [Lean.Elab.WF.paramLet, map_inv]
1058 _ =
1059 ((xWord τ
1061 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))⁻¹)⁻¹ := by
1062 rw [hzImage]
1063 _ =
1066 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j) := by
1067 simp only [inv_inv]
1069 {tailLen p : ℕ}
1070 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1071 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1072 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1073 (k : Fin p) :
1074 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1075 let σ :=
1076 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1077 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1078 let e :=
1080 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1081 let η :=
1083 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1084 η
1085 (e.symm
1087 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k)) =
1089 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k)⁻¹ := by
1090 classical
1091 dsimp
1092 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1093 let σ :=
1094 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1095 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1096 let φ :=
1098 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1099 let hT :=
1101 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1102 let e :=
1104 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1105 let η :=
1107 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1108 let x : FuchsianGenerator σ :=
1110 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1111 let y : FuchsianGenerator σ :=
1112 FuchsianGenerator.elliptic
1114 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1115 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1116 FuchsianGenerator.elliptic
1118 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1119 let z : ↥(schreierGeneratorSet hT) :=
1121 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k,
1123 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k⟩
1124 have hzWord :
1125 e.symm
1127 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k) =
1128 (FreeGroup.of z)⁻¹ := by
1129 simpa [σ, φ, hT, e, z] using
1131 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen z
1132 have hxne : x ≠ y := by
1133 intro hEq
1135 firstReductionCanonicalSourceOneIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, zero_ne_one, x, y] at hEq
1136 have hFirst :
1137 ¬ (z : φ.ker) =
1139 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
1140 intro hEq
1141 have hval := congrArg
1142 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
1143 let r : ℕ := ((k.val : ZMod p) - 1).val
1144 have hleft :
1145 ((z : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1146 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1147 ((FreeGroup.of x) ^ r)⁻¹ := by
1148 simp only [firstReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
1150 have hright :
1152 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen : φ.ker) :
1153 FreeGroup (FuchsianGenerator σ)) =
1154 (FreeGroup.of x) ^ p := by
1155 simpa [σ, φ, x] using
1157 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1158 have hword :
1159 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
1160 FreeGroup.of y *
1161 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r)⁻¹ =
1162 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ p := by
1163 simpa [hleft, hright] using hval
1164 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
1165 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
1166 have hmap := congrArg (FreeGroup.lift χ) hword
1167 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
1168 mul_one, ofAdd_eq_one, one_ne_zero, χ] at hmap
1169 have hTail :
1170 ¬ ∃ j' : Fin tailLen, ∃ k' : Fin p,
1171 (z : φ.ker) =
1173 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j' k' := by
1174 intro h
1175 rcases h with ⟨j', k', hEq⟩
1176 have hval := congrArg
1177 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
1178 let r : ℕ := ((k.val : ZMod p) - 1).val
1179 have hleft :
1180 ((z : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1181 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1182 ((FreeGroup.of x) ^ r)⁻¹ := by
1183 simp only [firstReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
1185 have hright :
1187 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j' k' : φ.ker) :
1188 FreeGroup (FuchsianGenerator σ)) =
1189 (FreeGroup.of x) ^ k'.val * FreeGroup.of (tailGen j') *
1190 ((FreeGroup.of x) ^ k'.val)⁻¹ := by
1191 simpa [σ, φ, x, tailGen] using
1193 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j' k'
1194 have hword :
1195 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
1196 FreeGroup.of y *
1197 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r)⁻¹ =
1198 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k'.val *
1199 FreeGroup.of (tailGen j') *
1200 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k'.val)⁻¹ := by
1201 simpa [hleft, hright] using hval
1202 have hyne : y ≠ tailGen j' := by
1203 intro hEq'
1205 FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, y, tailGen] at hEq'
1206 omega
1207 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
1208 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
1209 have hmap := congrArg (FreeGroup.lift χ) hword
1210 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
1211 mul_one, mul_ite, left_eq_ite_iff, ofAdd_eq_one, one_ne_zero, imp_false, Decidable.not_not, χ] at hmap
1212 exact hyne hmap.symm
1213 have hSecond :
1214 ∃ k' : Fin p,
1215 (z : φ.ker) =
1217 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k' := ⟨k, rfl⟩
1218 let k' : Fin p := Classical.choose hSecond
1219 have hSecondChoose :
1221 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k' =
1223 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k := by
1224 have hEqSecond :
1226 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k =
1228 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k' := by
1229 simpa [z, k'] using Classical.choose_spec hSecond
1230 have hk :=
1232 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hEqSecond
1233 simp only [hk]
1234 have hzImage :
1235 η (FreeGroup.of z) =
1237 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k := by
1238 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSchreierToTargetHom,
1239 firstReductionCanonicalSchreierToTargetGeneratorImage, dite_eq_ite, id_eq, FreeGroup.lift_apply_of, hFirst,
1240 ↓reduceIte, hSecond, ↓reduceDIte, hSecondChoose, η, z, k', σ]
1241 calc
1242 η
1243 (e.symm
1245 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k)) =
1246 η ((FreeGroup.of z)⁻¹) := by rw [hzWord]
1247 _ = (η (FreeGroup.of z))⁻¹ := by simp only [Lean.Elab.WF.paramLet, map_inv]
1248 _ =
1250 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k)⁻¹ := by
1251 rw [hzImage]
1253 {tailLen p : ℕ}
1254 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1255 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1256 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1257 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1258 let σ :=
1259 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1260 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1261 let φ :=
1263 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1264 let x : FuchsianGenerator σ :=
1265 FuchsianGenerator.elliptic
1267 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1268 let y : FuchsianGenerator σ :=
1269 FuchsianGenerator.elliptic
1271 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1272 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1273 FuchsianGenerator.elliptic
1275 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1276 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1277 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1280 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1281 let hT : IsRightSchreierTransversal φ.ker T :=
1283 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1285 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
1286 rw [MonoidHom.mem_ker, map_pow, hx]
1287 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1288 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
1289 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
1290 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
1291 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1293 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
1294 rw [MonoidHom.mem_ker, map_pow, hy]
1295 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1296 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
1297 neg_zero, toAdd_one]⟩
1298 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
1299 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
1300 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
1301 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
1302 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1304 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
1305 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
1306 omega
1307 rw [MonoidHom.mem_ker]
1308 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
1309 e.symm a * e.symm b *
1310 (List.ofFn (fun k : Fin p =>
1311 (List.ofFn (fun j : Fin tailLen => e.symm (c j k))).prod)).prod ∈
1312 Subgroup.normalClosure
1317 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
1318 (rels := relators σ) T)) := by
1319 classical
1320 dsimp
1321 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1322 let σ :=
1323 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1324 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1325 let φ :=
1327 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1328 let x : FuchsianGenerator σ :=
1329 FuchsianGenerator.elliptic
1331 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1332 let y : FuchsianGenerator σ :=
1333 FuchsianGenerator.elliptic
1335 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1336 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1337 FuchsianGenerator.elliptic
1339 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1340 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1341 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1344 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1345 let hT : IsRightSchreierTransversal φ.ker T :=
1347 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1349 let hrels :=
1351 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1352 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
1353 rw [MonoidHom.mem_ker, map_pow, hx]
1354 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1355 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
1356 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
1357 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
1358 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1360 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
1361 rw [MonoidHom.mem_ker, map_pow, hy]
1362 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1363 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
1364 neg_zero, toAdd_one]⟩
1365 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
1366 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
1367 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
1368 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
1369 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1371 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
1372 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
1373 omega
1374 rw [MonoidHom.mem_ker]
1375 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
1376 let kBlock : φ.ker :=
1377 a * b *
1378 (List.ofFn (fun k : Fin p =>
1379 (List.ofFn (fun j : Fin tailLen => c j k)).prod)).prod
1380 have hTailRel :
1381 FreeGroup.of x * FreeGroup.of y *
1382 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod ∈
1383 Subgroup.normalClosure (relators σ) := by
1384 have hTotal :=
1386 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1387 have hTailEq :
1389 FreeGroup.of x * FreeGroup.of y *
1390 (List.ofFn (fun j : Fin tailLen => FreeGroup.of (tailGen j))).prod := by
1391 simpa [σ, x, y, tailGen, xWord] using hTotal
1392 rw [← hTailEq]
1393 exact Subgroup.subset_normalClosure (Or.inr rfl)
1394 have hSourceBlock :
1395 (FreeGroup.of x) ^ p * (FreeGroup.of y) ^ p *
1396 (List.ofFn (fun k : Fin p =>
1397 (List.ofFn (fun j : Fin tailLen =>
1398 (FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
1399 ((FreeGroup.of x) ^ (k : ℕ))⁻¹)).prod)).prod ∈
1400 Subgroup.normalClosure (relators σ) := by
1401 simpa [x, y, tailGen] using
1403 (FreeGroup.of x) (FreeGroup.of y)
1404 (fun j : Fin tailLen => FreeGroup.of (tailGen j)) p hTailRel
1405 have hBlockCoe :
1406 (((List.ofFn (fun k : Fin p =>
1407 (List.ofFn (fun j : Fin tailLen => c j k)).prod)).prod : φ.ker) :
1408 FreeGroup (FuchsianGenerator σ)) =
1409 (List.ofFn (fun k : Fin p =>
1410 (List.ofFn (fun j : Fin tailLen =>
1411 ((c j k : φ.ker) : FreeGroup (FuchsianGenerator σ)))).prod)).prod := by
1412 simpa using
1413 (MonoidHom.map_list_prod_ofFn₂ φ.ker.subtype
1414 (fun k : Fin p => fun j : Fin tailLen => c j k))
1415 have hkSource : (kBlock : FreeGroup (FuchsianGenerator σ)) ∈
1416 Subgroup.normalClosure (relators σ) := by
1417 change
1418 ((a : φ.ker) : FreeGroup (FuchsianGenerator σ)) *
1419 ((b : φ.ker) : FreeGroup (FuchsianGenerator σ)) *
1420 (((List.ofFn (fun k : Fin p =>
1421 (List.ofFn (fun j : Fin tailLen => c j k)).prod)).prod : φ.ker) :
1422 FreeGroup (FuchsianGenerator σ)) ∈
1423 Subgroup.normalClosure (relators σ)
1424 rw [hBlockCoe]
1425 simpa [a, b, c, x, y, tailGen] using hSourceBlock
1426 have hmem :
1427 e.symm kBlock ∈
1428 Subgroup.normalClosure
1433 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
1434 (rels := relators σ) T)) := by
1435 exact
1437 hrels hT.1 e hkSource
1438 have hBlockMap :
1439 e.symm ((List.ofFn (fun k : Fin p =>
1440 (List.ofFn (fun j : Fin tailLen => c j k)).prod)).prod) =
1441 (List.ofFn (fun k : Fin p =>
1442 (List.ofFn (fun j : Fin tailLen => e.symm (c j k))).prod)).prod := by
1443 simpa using
1444 (MonoidHom.map_list_prod_ofFn₂ e.symm.toMonoidHom
1445 (fun k : Fin p => fun j : Fin tailLen => c j k))
1446 have hmem' :
1447 e.symm a * e.symm b *
1448 e.symm
1449 ((List.ofFn (fun k : Fin p =>
1450 (List.ofFn (fun j : Fin tailLen => c j k)).prod)).prod) ∈
1451 Subgroup.normalClosure
1456 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
1457 (rels := relators σ) T)) := by
1458 simpa [kBlock, map_mul] using hmem
1459 rw [hBlockMap] at hmem'
1460 simpa [a, b, c] using hmem'
1462 {tailLen p : ℕ}
1463 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1464 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1465 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1466 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1467 let σ :=
1468 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1469 let τ :=
1470 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1471 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1472 let φ :=
1474 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1475 let x : FuchsianGenerator σ :=
1476 FuchsianGenerator.elliptic
1478 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1479 let y : FuchsianGenerator σ :=
1480 FuchsianGenerator.elliptic
1482 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1483 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1484 FuchsianGenerator.elliptic
1486 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1487 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1488 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1491 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1492 let hT : IsRightSchreierTransversal φ.ker T :=
1494 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1496 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
1497 rw [MonoidHom.mem_ker, map_pow, hx]
1498 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1499 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
1500 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
1501 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
1502 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1504 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
1505 rw [MonoidHom.mem_ker, map_pow, hy]
1506 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1507 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
1508 neg_zero, toAdd_one]⟩
1509 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
1510 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
1511 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
1512 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
1513 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1515 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
1516 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
1517 omega
1518 rw [MonoidHom.mem_ker]
1519 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
1520 ∀ (η :
1521 FreeGroup (FuchsianGenerator τ) →*
1522 FreeGroup ↥(schreierGeneratorSet hT)),
1523 η (xWord τ
1525 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) = e.symm a →
1526 η (xWord τ
1528 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) = e.symm b →
1529 (∀ k : Fin p, ∀ j : Fin tailLen,
1530 η (xWord τ
1532 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j)) = e.symm (c j k)) →
1533 η (totalRelation τ) ∈
1534 Subgroup.normalClosure
1539 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
1540 (rels := relators σ) T)) := by
1541 classical
1542 dsimp
1543 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1544 let σ :=
1545 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1546 let τ :=
1547 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1548 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1549 let φ :=
1551 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1552 let x : FuchsianGenerator σ :=
1553 FuchsianGenerator.elliptic
1555 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1556 let y : FuchsianGenerator σ :=
1557 FuchsianGenerator.elliptic
1559 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1560 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1561 FuchsianGenerator.elliptic
1563 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1564 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1565 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1568 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1569 let hT : IsRightSchreierTransversal φ.ker T :=
1571 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1573 let hrels :=
1575 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1576 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
1577 rw [MonoidHom.mem_ker, map_pow, hx]
1578 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1579 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
1580 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
1581 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
1582 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1584 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
1585 rw [MonoidHom.mem_ker, map_pow, hy]
1586 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1587 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
1588 neg_zero, toAdd_one]⟩
1589 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
1590 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
1591 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
1592 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
1593 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1595 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
1596 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
1597 omega
1598 rw [MonoidHom.mem_ker]
1599 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
1600 intro η hzero hone htailMap
1601 have hImage :
1603 e.symm a * e.symm b *
1604 (List.ofFn (fun k : Fin p =>
1605 (List.ofFn (fun j : Fin tailLen => e.symm (c j k))).prod)).prod := by
1607 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen]
1609 rw [MonoidHom.map_list_prod_ofFn₂ η
1610 (fun k : Fin p => fun j : Fin tailLen =>
1613 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))]
1614 simp only [hzero, hone, htailMap, τ, φ, e, x, a, b, y, c, tailGen]
1615 rw [hImage]
1616 simpa [σ, φ, x, y, tailGen, T, hT, e, hrels, a, b, c] using
1618 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1620 {tailLen p : ℕ}
1621 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1622 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1623 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1624 {G : Type*} [Group G] {S : Set G}
1625 (η :
1626 let τ :=
1627 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1628 FreeGroup (FuchsianGenerator τ) →* G)
1629 (hPower :
1630 let τ :=
1631 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1632 ∀ i : Fin τ.numPeriods,
1633 η ((xWord τ i) ^ τ.periods i) ∈ Subgroup.normalClosure S)
1634 (hTotal :
1635 let τ :=
1636 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1637 η (totalRelation τ) ∈ Subgroup.normalClosure S) :
1638 let τ :=
1639 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1640 ∀ r ∈ relators τ, η r ∈ Subgroup.normalClosure S := by
1641 classical
1642 dsimp
1643 intro r hr
1644 rcases hr with ⟨i, rfl⟩ | rfl
1645 · exact hPower i
1646 · exact hTotal
1648 {tailLen p : ℕ}
1649 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1650 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1651 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1652 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1653 let σ :=
1654 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1655 let τ :=
1656 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1657 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1658 let φ :=
1660 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1661 let x : FuchsianGenerator σ :=
1662 FuchsianGenerator.elliptic
1664 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1665 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1666 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1669 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1670 let hT : IsRightSchreierTransversal φ.ker T :=
1672 FuchsianGenerator τ → FreeGroup ↥(schreierGeneratorSet hT) := by
1673 classical
1674 dsimp
1675 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1676 let σ :=
1677 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1678 let τ :=
1679 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1680 let φ :=
1682 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1683 let x : FuchsianGenerator σ :=
1684 FuchsianGenerator.elliptic
1686 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1687 let y : FuchsianGenerator σ :=
1688 FuchsianGenerator.elliptic
1690 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1691 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1692 FuchsianGenerator.elliptic
1694 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1695 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1696 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1699 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1700 let hT : IsRightSchreierTransversal φ.ker T :=
1702 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1704 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
1705 rw [MonoidHom.mem_ker, map_pow, hx]
1706 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1707 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
1708 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
1709 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
1710 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1712 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
1713 rw [MonoidHom.mem_ker, map_pow, hy]
1714 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1715 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
1716 neg_zero, toAdd_one]⟩
1717 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
1718 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
1719 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
1720 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
1721 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1723 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
1724 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
1725 omega
1726 rw [MonoidHom.mem_ker]
1727 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
1728 intro g
1729 cases g with
1730 | elliptic i =>
1731 by_cases h0 : i.val = 0
1732 · exact e.symm a
1733 · by_cases h1 : i.val = 1
1734 · exact e.symm b
1735 · let r : Fin (p * tailLen) := ⟨i.val - 2, by
1736 have hi : i.val < 2 + p * tailLen := by
1738 exact i.isLt
1739 omega⟩
1740 let k : Fin p := ⟨r.val / tailLen, by
1741 exact Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using r.isLt)⟩
1742 let j : Fin tailLen := ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩
1743 exact e.symm (c j k)
1744 | surfaceA _ => exact 1
1745 | surfaceB _ => exact 1
1747 {tailLen p : ℕ}
1748 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1749 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1750 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1751 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1752 let σ :=
1753 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1754 let τ :=
1755 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1756 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1757 let φ :=
1759 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1760 let x : FuchsianGenerator σ :=
1761 FuchsianGenerator.elliptic
1763 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1764 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1765 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1768 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1769 let hT : IsRightSchreierTransversal φ.ker T :=
1771 FreeGroup (FuchsianGenerator τ) →* FreeGroup ↥(schreierGeneratorSet hT) :=
1772 FreeGroup.lift
1774 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1776 {tailLen p : ℕ}
1777 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1778 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1779 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1780 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1781 let σ :=
1782 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1783 let τ :=
1784 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1785 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1786 let φ :=
1788 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1789 let x : FuchsianGenerator σ :=
1790 FuchsianGenerator.elliptic
1792 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1793 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1794 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1797 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1798 let hT : IsRightSchreierTransversal φ.ker T :=
1800 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1802 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
1803 rw [MonoidHom.mem_ker, map_pow, hx]
1804 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1805 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
1807 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1810 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) =
1811 e.symm a := by
1812 classical
1813 dsimp
1815 Lean.Elab.WF.paramLet, id_eq, xWord, firstReductionCanonicalTargetZeroIndex, FreeGroup.lift_apply_of, ↓reduceDIte]
1817 {tailLen p : ℕ}
1818 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1819 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1820 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1821 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1822 let σ :=
1823 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1824 let τ :=
1825 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1826 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1827 let φ :=
1829 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1830 let x : FuchsianGenerator σ :=
1831 FuchsianGenerator.elliptic
1833 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1834 let y : FuchsianGenerator σ :=
1835 FuchsianGenerator.elliptic
1837 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1838 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1839 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1842 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1843 let hT : IsRightSchreierTransversal φ.ker T :=
1845 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1847 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
1848 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
1849 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1851 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
1852 rw [MonoidHom.mem_ker, map_pow, hy]
1853 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
1854 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
1855 neg_zero, toAdd_one]⟩
1857 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1860 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) =
1861 e.symm b := by
1862 classical
1863 dsimp
1865 Lean.Elab.WF.paramLet, id_eq, xWord, firstReductionCanonicalTargetOneIndex, FreeGroup.lift_apply_of, one_ne_zero,
1866 ↓reduceDIte]
1868 {tailLen p : ℕ}
1869 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1870 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1871 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1872 (k : Fin p) (j : Fin tailLen) :
1873 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1874 let σ :=
1875 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1876 let τ :=
1877 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1878 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1879 let φ :=
1881 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1882 let x : FuchsianGenerator σ :=
1883 FuchsianGenerator.elliptic
1885 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1886 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1887 FuchsianGenerator.elliptic
1889 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1890 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1891 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1894 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
1895 let hT : IsRightSchreierTransversal φ.ker T :=
1897 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
1899 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
1900 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
1901 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
1902 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
1903 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1905 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
1906 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
1907 omega
1908 rw [MonoidHom.mem_ker]
1909 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
1911 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1914 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j)) =
1915 e.symm (c j k) := by
1916 classical
1917 dsimp
1918 have hzero : 2 + k.val * tailLen + j.val ≠ 0 := by omega
1919 have hone : 2 + k.val * tailLen + j.val ≠ 1 := by omega
1920 have hsub :
1921 2 + k.val * tailLen + j.val - 2 = k.val * tailLen + j.val := by
1922 omega
1923 have hdiv : (2 + k.val * tailLen + j.val - 2) / tailLen = k.val := by
1924 rw [hsub, Nat.mul_comm k.val tailLen, Nat.mul_add_div hTailLen,
1925 Nat.div_eq_of_lt j.isLt]
1926 simp only [add_zero]
1927 have hmod : (2 + k.val * tailLen + j.val - 2) % tailLen = j.val := by
1928 rw [hsub, Nat.mul_comm k.val tailLen, Nat.mul_add_mod_self_left,
1929 Nat.mod_eq_of_lt j.isLt]
1931 Lean.Elab.WF.paramLet, id_eq, xWord, firstReductionCanonicalTargetTailIndex, FreeGroup.lift_apply_of,
1932 Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, mul_eq_zero, false_and, ↓reduceDIte, hone, hdiv, hmod, Fin.eta]
1934 {tailLen p : ℕ}
1935 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1936 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1937 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1938 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1939 let σ :=
1940 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1941 let τ :=
1942 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1943 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1944 let e :=
1946 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1948 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1951 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) =
1952 e.symm
1954 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
1955 classical
1956 dsimp
1961 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1963 {tailLen p : ℕ}
1964 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1965 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1966 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1967 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1968 let σ :=
1969 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1970 let τ :=
1971 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1972 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1973 let e :=
1975 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1977 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1980 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) =
1981 e.symm
1983 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
1984 classical
1985 dsimp
1990 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1992 {tailLen p : ℕ}
1993 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1994 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1995 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1996 (k : Fin p) (j : Fin tailLen) :
1997 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1998 let σ :=
1999 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2000 let τ :=
2001 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2002 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2003 let e :=
2005 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2007 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2010 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j)) =
2011 e.symm
2013 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k) := by
2014 classical
2015 dsimp
2020 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j
2022 {tailLen p : ℕ}
2023 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2024 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2025 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2026 (k : Fin p) :
2027 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2028 let σ :=
2029 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2030 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2031 let e :=
2033 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2035 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2037 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k) =
2038 (List.ofFn (fun j : Fin tailLen =>
2039 e.symm
2041 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k))).prod := by
2042 classical
2043 dsimp
2044 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2045 let σ :=
2046 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2047 let τ :=
2048 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2049 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2050 let e :=
2052 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2053 let θ :=
2055 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2056 change
2057 θ
2058 ((List.ofFn (fun j : Fin tailLen =>
2061 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod) =
2062 (List.ofFn (fun j : Fin tailLen =>
2063 e.symm
2065 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k))).prod
2066 rw [map_list_prod, List.map_ofFn]
2067 apply congrArg List.prod
2068 apply List.ofFn_inj.2
2069 funext j
2070 simpa [σ, τ, e, θ] using
2072 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j
2074 {tailLen p : ℕ}
2075 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2076 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2077 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
2078 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2079 let σ :=
2080 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2081 let τ :=
2082 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2083 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2084 let θ :=
2086 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2087 let η :=
2089 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2090 η
2091 (θ
2094 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))) *
2097 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))⁻¹ ∈
2098 Subgroup.normalClosure (relators τ) := by
2099 classical
2100 dsimp
2101 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2102 let σ :=
2103 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2104 let τ :=
2105 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2106 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2107 let θ :=
2109 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2110 let η :=
2112 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2115 simp only [mul_inv_cancel, one_mem]
2117 {tailLen p : ℕ}
2118 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2119 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2120 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2121 (k : Fin p) (j : Fin tailLen) :
2122 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2123 let σ :=
2124 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2125 let τ :=
2126 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2127 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2128 let θ :=
2130 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2131 let η :=
2133 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2134 η
2135 (θ
2138 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))) *
2141 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))⁻¹ ∈
2142 Subgroup.normalClosure (relators τ) := by
2143 classical
2144 dsimp
2145 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2146 let σ :=
2147 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2148 let τ :=
2149 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2150 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2153 simp only [mul_inv_cancel, one_mem]
2155 {tailLen p : ℕ}
2156 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2157 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2158 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
2159 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2160 let σ :=
2161 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2162 let τ :=
2163 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2164 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2165 let θ :=
2167 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2168 let η :=
2170 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2171 η
2172 (θ
2175 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))) *
2178 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))⁻¹ ∈
2179 Subgroup.normalClosure (relators τ) := by
2180 classical
2181 dsimp
2182 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2183 let n := p - 1
2184 let σ :=
2185 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2186 let τ :=
2187 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2188 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2189 let e :=
2191 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2192 let θ :=
2194 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2195 let η :=
2197 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2198 let A :=
2201 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
2202 let B :=
2205 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
2206 let C :=
2207 (List.ofFn (fun k : Fin p =>
2209 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k)).prod
2210 let secondWord :=
2212 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2213 have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
2214 have hTheta :
2215 θ B =
2216 e.symm
2218 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
2219 simpa [σ, τ, e, θ, B] using
2221 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2222 have hcycle :
2223 e.symm
2225 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2226 ⟨0, hp_pos⟩) *
2227 (List.ofFn (fun i : Fin n =>
2228 e.symm
2230 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2231 ⟨n - i.val, by omega⟩))).prod =
2232 e.symm
2234 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
2235 simpa [n, σ, e] using
2237 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2238 have hImage :
2239 η
2240 (e.symm
2242 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) =
2243 (secondWord ⟨0, hp_pos⟩)⁻¹ *
2244 (List.ofFn (fun i : Fin n =>
2245 (secondWord ⟨n - i.val, by omega⟩)⁻¹)).prod := by
2246 rw [← hcycle]
2249 rw [map_list_prod, List.map_ofFn]
2250 congr 1
2251 apply congrArg List.prod
2252 apply List.ofFn_inj.2
2253 funext i
2254 simpa [σ, e, η, secondWord] using
2256 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2257 ⟨n - i.val, by omega⟩
2258 have hDesc :
2259 (secondWord ⟨0, hp_pos⟩)⁻¹ *
2260 (List.ofFn (fun i : Fin n =>
2261 (secondWord ⟨n - i.val, by omega⟩)⁻¹)).prod =
2262 A⁻¹ * C⁻¹ := by
2263 let block :=
2265 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2266 have hleft :
2267 (secondWord ⟨0, hp_pos⟩)⁻¹ *
2268 (List.ofFn (fun i : Fin n =>
2269 (secondWord ⟨n - i.val, by omega⟩)⁻¹)).prod =
2270 (block ⟨p - 1, by omega⟩ * A)⁻¹ *
2271 (List.ofFn (fun i : Fin (p - 1) =>
2272 (block ⟨p - 2 - i.val, by omega⟩)⁻¹)).prod := by
2273 subst n
2275 congr 1
2276 apply congrArg List.prod
2277 apply List.ofFn_inj.2
2278 funext i
2279 have hne : ¬p - 1 - i.val = 0 := by omega
2280 rw [if_neg hne]
2281 congr 1
2282 apply congrArg block
2283 ext
2284 simp only
2285 omega
2286 have hdesc :
2287 (block ⟨p - 1, by omega⟩ * A)⁻¹ *
2288 (List.ofFn (fun i : Fin (p - 1) =>
2289 (block ⟨p - 2 - i.val, by omega⟩)⁻¹)).prod =
2290 A⁻¹ * (List.ofFn block).prod⁻¹ :=
2292 calc
2293 (secondWord ⟨0, hp_pos⟩)⁻¹ *
2294 (List.ofFn (fun i : Fin n =>
2295 (secondWord ⟨n - i.val, by omega⟩)⁻¹)).prod =
2296 (block ⟨p - 1, by omega⟩ * A)⁻¹ *
2297 (List.ofFn (fun i : Fin (p - 1) =>
2298 (block ⟨p - 2 - i.val, by omega⟩)⁻¹)).prod := hleft
2299 _ = A⁻¹ * (List.ofFn block).prod⁻¹ := hdesc
2300 have hTarget :
2301 (A⁻¹ * C⁻¹) * B⁻¹ ∈ Subgroup.normalClosure (relators τ) := by
2302 simpa [τ, A, B, C, mul_assoc] using
2304 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2305 rw [show xWord τ
2307 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) = B by rfl]
2308 rw [hTheta, hImage]
2309 rw [hDesc]
2310 simpa [mul_assoc] using hTarget
2312 {tailLen p : ℕ}
2313 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2314 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2315 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2316 (hOne :
2317 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2318 let σ :=
2319 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2320 let τ :=
2321 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2322 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2323 let θ :=
2325 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2326 let η :=
2328 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2329 η
2330 (θ
2333 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))) *
2336 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))⁻¹ ∈
2337 Subgroup.normalClosure (relators τ)) :
2338 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2339 let σ :=
2340 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2341 let τ :=
2342 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2343 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2344 let θ :=
2346 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2347 let η :=
2349 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2351 η (θ (FreeGroup.of y)) * (FreeGroup.of y)⁻¹ ∈
2352 Subgroup.normalClosure (relators τ) := by
2353 classical
2354 dsimp
2355 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2356 let σ :=
2357 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2358 let τ :=
2359 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2360 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2361 intro y
2362 cases y with
2363 | elliptic i =>
2364 by_cases h0 : i.val = 0
2365 · have hi :
2366 i =
2368 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
2369 ext
2371 subst i
2372 simpa [τ, xWord] using
2374 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2375 · by_cases h1 : i.val = 1
2376 · have hi :
2377 i =
2379 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
2380 ext
2382 subst i
2383 simpa [τ, xWord] using hOne
2384 · let r : Fin (p * tailLen) := ⟨i.val - 2, by
2385 have hi : i.val < 2 + p * tailLen := by
2387 exact i.isLt
2388 omega⟩
2389 let k : Fin p := ⟨r.val / tailLen, by
2390 exact Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using r.isLt)⟩
2391 let j : Fin tailLen := ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩
2392 have hiTail :
2393 i =
2395 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j := by
2396 simpa [r, k, j] using
2398 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i h0 h1
2399 rw [hiTail]
2400 simpa [τ, xWord, r, k, j] using
2402 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j
2403 | surfaceA i =>
2404 exact Fin.elim0 (by
2406 | surfaceB i =>
2407 exact Fin.elim0 (by
2410 {tailLen p : ℕ}
2411 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2412 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2413 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
2414 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2415 let σ :=
2416 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2417 let τ :=
2418 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2419 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2420 let θ :=
2422 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2423 let η :=
2425 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2427 η (θ (FreeGroup.of y)) * (FreeGroup.of y)⁻¹ ∈
2428 Subgroup.normalClosure (relators τ) :=
2430 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2432 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
2434 {tailLen p : ℕ}
2435 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2436 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2437 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
2438 let τ :=
2439 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2441 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2442 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩ =
2444 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2445 ⟨p - 1, by omega⟩ *
2448 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
2449 classical
2452 {tailLen p : ℕ}
2453 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2454 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2455 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2456 (k : Fin p) (h0 : k.val ≠ 0) :
2458 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k =
2460 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2461 ⟨k.val - 1, by omega⟩ := by
2462 classical
2464 rw [if_neg h0]
2466 {tailLen p : ℕ}
2467 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2468 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2469 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2470 (k : Fin (p - 1)) :
2471 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2472 let σ :=
2473 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2474 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2475 let e :=
2477 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2478 let η :=
2480 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2481 η
2482 (e.symm
2484 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2485 ⟨k.val + 1, by omega⟩) *
2486 (List.ofFn (fun j : Fin tailLen =>
2487 e.symm
2489 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2490 ⟨k.val, by omega⟩))).prod) = 1 := by
2491 classical
2492 dsimp
2493 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2494 let σ :=
2495 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2496 let τ :=
2497 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2498 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2499 let e :=
2501 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2502 let η :=
2504 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2505 let block :=
2507 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2510 rw [map_list_prod, List.map_ofFn]
2511 have hne : (⟨k.val + 1, by omega⟩ : Fin p).val ≠ 0 := by
2512 simp only [ne_eq, Nat.add_eq_zero_iff, one_ne_zero, and_false, not_false_eq_true]
2514 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2515 ⟨k.val + 1, by omega⟩ hne]
2516 have hprev :
2517 block ⟨(⟨k.val + 1, by omega⟩ : Fin p).val - 1, by omega⟩ =
2518 block ⟨k.val, by omega⟩ := by
2519 apply congrArg block
2520 ext
2521 simp only [add_tsub_cancel_right]
2522 have htailMap :
2523 (List.ofFn (fun j : Fin tailLen =>
2524 η
2525 (e.symm
2527 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2528 ⟨k.val, by omega⟩)))) =
2529 List.ofFn (fun j : Fin tailLen =>
2532 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2533 ⟨k.val, by omega⟩ j)) := by
2534 apply List.ofFn_inj.2
2535 funext j
2536 simpa [σ, τ, e, η] using
2538 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2539 ⟨k.val, by omega⟩
2540 change
2541 (block ⟨(⟨k.val + 1, by omega⟩ : Fin p).val - 1, by omega⟩)⁻¹ *
2542 (List.ofFn (fun j : Fin tailLen =>
2543 η
2544 (e.symm
2546 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2547 ⟨k.val, by omega⟩)))).prod = 1
2548 rw [htailMap]
2549 change
2550 (block ⟨(⟨k.val + 1, by omega⟩ : Fin p).val - 1, by omega⟩)⁻¹ *
2551 block ⟨k.val, by omega⟩ = 1
2552 rw [hprev]
2553 simp only [inv_mul_cancel]
2555 {tailLen p : ℕ}
2556 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2557 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2558 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
2559 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2560 let σ :=
2561 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2562 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2563 let e :=
2565 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2566 let η :=
2568 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2569 η
2570 ((List.ofFn (fun j : Fin tailLen =>
2571 e.symm
2573 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2574 ⟨p - 1, by omega⟩))).prod *
2575 e.symm
2577 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
2578 e.symm
2580 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2581 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩)) = 1 := by
2582 classical
2583 dsimp
2584 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2585 let σ :=
2586 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2587 let τ :=
2588 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2589 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2590 let e :=
2592 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2593 let η :=
2595 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2596 let A :=
2599 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
2600 let block :=
2602 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2604 rw [map_list_prod, List.map_ofFn]
2605 have htailMap :
2606 (List.ofFn (fun j : Fin tailLen =>
2607 η
2608 (e.symm
2610 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2611 ⟨p - 1, by omega⟩)))) =
2612 List.ofFn (fun j : Fin tailLen =>
2615 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2616 ⟨p - 1, by omega⟩ j)) := by
2617 apply List.ofFn_inj.2
2618 funext j
2619 simpa [σ, τ, e, η] using
2621 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2622 ⟨p - 1, by omega⟩
2623 change
2624 (List.ofFn (fun j : Fin tailLen =>
2625 η
2626 (e.symm
2628 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
2629 ⟨p - 1, by omega⟩)))).prod *
2630 η
2631 (e.symm
2633 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) *
2634 η
2635 (e.symm
2637 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2638 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩)) = 1
2639 rw [htailMap]
2643 change block ⟨p - 1, by omega⟩ * A *
2644 (block ⟨p - 1, by omega⟩ * A)⁻¹ = 1
2645 group
2647 {tailLen p : ℕ}
2648 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2649 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2650 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2651 (k : Fin p) :
2652 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2653 let σ :=
2654 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2655 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2656 let e :=
2658 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2660 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2662 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k) *
2663 e.symm
2665 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k) ∈
2666 Subgroup.normalClosure
2668 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
2669 classical
2670 dsimp
2671 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2672 let σ :=
2673 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2674 let τ :=
2675 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2676 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2677 let e :=
2679 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2680 let θ :=
2682 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2683 by_cases h0 : k.val = 0
2684 · have hk :
2685 k = ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩ := by
2686 ext
2687 simpa using h0
2688 subst k
2693 simpa [σ, τ, e, θ, mul_assoc] using
2695 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2696 · let i : Fin (p - 1) := ⟨k.val - 1, by
2697 have hklt := k.isLt
2698 omega⟩
2699 have hkSucc :
2700 (⟨i.val + 1, by omega⟩ : Fin p) = k := by
2701 ext
2702 simp only [i]
2703 omega
2705 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k h0]
2707 simpa [σ, τ, e, θ, i, hkSucc, mul_assoc] using
2709 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i
2711 {tailLen p : ℕ}
2712 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2713 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2714 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2715 (z :
2716 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2717 let σ :=
2718 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2719 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2720 let hT :=
2722 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2724 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2725 let σ :=
2726 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2727 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2728 let θ :=
2730 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2731 let η :=
2733 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2734 θ (η (FreeGroup.of z)) * (FreeGroup.of z)⁻¹ ∈
2735 Subgroup.normalClosure
2737 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
2738 classical
2739 dsimp
2740 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2741 let σ :=
2742 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2743 let τ :=
2744 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2745 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2746 let φ :=
2748 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2749 let hT :=
2751 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2752 let e :=
2754 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2755 let θ :=
2757 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2758 let η :=
2760 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2761 have hzWord :
2762 (FreeGroup.of z)⁻¹ = e.symm (z : φ.ker) := by
2763 symm
2764 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSchreierBasisEquiv_symm_apply, e]
2765 by_cases hFirst :
2766 (z : φ.ker) =
2768 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2769 · have hzFirst :
2770 (FreeGroup.of z)⁻¹ =
2771 e.symm
2773 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
2774 rw [hzWord, hFirst]
2776 Lean.Elab.WF.paramLet, dite_eq_ite, id_eq, FreeGroup.lift_apply_of, hFirst, ↓reduceIte, map_inv,
2777 firstReductionCanonicalTargetToSchreierHom_zero_named, hzFirst, inv_mul_cancel, one_mem, e, σ]
2778 · by_cases hSecond :
2779 ∃ k : Fin p,
2780 (z : φ.ker) =
2782 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k
2783 · rcases hSecond with ⟨k, hzK⟩
2784 let k' : Fin p := Classical.choose (show ∃ k : Fin p,
2785 (z : φ.ker) =
2787 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k from ⟨k, hzK⟩)
2788 have hzK' :
2789 (z : φ.ker) =
2791 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k' :=
2792 Classical.choose_spec (show ∃ k : Fin p,
2793 (z : φ.ker) =
2795 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k from ⟨k, hzK⟩)
2796 have hzKWord :
2797 (FreeGroup.of z)⁻¹ =
2798 e.symm
2800 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k') := by
2801 rw [hzWord, hzK']
2802 have hSecond' :
2803 ∃ k : Fin p,
2804 (z : φ.ker) =
2806 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k := ⟨k, hzK⟩
2807 simpa [σ, τ, φ, hT, e, θ, η,
2810 hFirst, hSecond', k', hzKWord] using
2812 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k'
2813 · rcases
2815 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen z with
2816 hFirstCase | hSecondCase | hTailCase
2817 · exact False.elim (hFirst hFirstCase)
2818 · exact False.elim (hSecond hSecondCase)
2819 · let j : Fin tailLen := Classical.choose hTailCase
2820 let hk : ∃ k : Fin p,
2821 (z : φ.ker) =
2823 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k :=
2824 Classical.choose_spec hTailCase
2825 let k : Fin p := Classical.choose hk
2826 have hzTail :
2827 (z : φ.ker) =
2829 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k :=
2830 Classical.choose_spec hk
2831 have hzTailWord :
2832 (FreeGroup.of z)⁻¹ =
2833 e.symm
2835 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k) := by
2836 rw [hzWord, hzTail]
2838 Lean.Elab.WF.paramLet, dite_eq_ite, id_eq, FreeGroup.lift_apply_of, hFirst, ↓reduceIte, hSecond, ↓reduceDIte,
2839 hTailCase, map_inv, firstReductionCanonicalTargetToSchreierHom_tail_named, hzTailWord, inv_mul_cancel, one_mem, e,
2840 j, k, σ]
2842 {tailLen p : ℕ}
2843 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2844 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2845 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
2846 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2847 let σ :=
2848 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2849 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2850 let hT :=
2852 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2853 let θ :=
2855 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2856 let η :=
2858 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2859 ∀ w : FreeGroup ↥(schreierGeneratorSet hT),
2860 θ (η w) * w⁻¹ ∈
2861 Subgroup.normalClosure
2863 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
2864 classical
2865 dsimp
2866 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2867 let σ :=
2868 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2869 let τ :=
2870 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2871 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2872 let hT :=
2874 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2875 let θ :=
2877 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2878 let η :=
2880 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2881 let R :=
2883 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2884 let F : FreeGroup ↥(schreierGeneratorSet hT) →* FreeGroup ↥(schreierGeneratorSet hT) :=
2885 θ.comp η
2886 have hgen :
2887 ∀ z : ↥(schreierGeneratorSet hT),
2888 F (FreeGroup.of z) * (FreeGroup.of z)⁻¹ ∈ Subgroup.normalClosure R := by
2889 intro z
2890 simpa [σ, τ, hT, θ, η, R, F] using
2892 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen z
2893 intro w
2894 simpa [R, F] using
2895 ReidemeisterSchreier.Discrete.Presentations.freeGroup_endomorph_mul_inv_mem_normalClosure_of_generator_mul_inv R F hgen w
2897 {tailLen p : ℕ}
2898 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2899 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2900 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
2901 (hgen :
2902 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2903 let σ :=
2904 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2905 let τ :=
2906 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2907 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2908 let θ :=
2910 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2911 let η :=
2913 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2915 η (θ (FreeGroup.of y)) * (FreeGroup.of y)⁻¹ ∈
2916 Subgroup.normalClosure (relators τ)) :
2917 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2918 let σ :=
2919 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2920 let τ :=
2921 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2922 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2923 let θ :=
2925 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2926 let η :=
2928 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2929 ∀ y : FreeGroup (FuchsianGenerator τ),
2930 η (θ y) * y⁻¹ ∈ Subgroup.normalClosure (relators τ) := by
2931 classical
2932 dsimp
2933 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2934 let σ :=
2935 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2936 let τ :=
2937 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2938 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2939 let θ :=
2941 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2942 let η :=
2944 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2945 let F : FreeGroup (FuchsianGenerator τ) →* FreeGroup (FuchsianGenerator τ) := η.comp θ
2946 have hgen' :
2948 F (FreeGroup.of y) * (FreeGroup.of y)⁻¹ ∈
2949 Subgroup.normalClosure (relators τ) := by
2950 intro y
2951 simpa [σ, τ, θ, η, F] using hgen y
2952 intro y
2953 simpa [F] using
2954 ReidemeisterSchreier.Discrete.Presentations.freeGroup_endomorph_mul_inv_mem_normalClosure_of_generator_mul_inv
2955 (relators τ) F hgen' y
2957 {tailLen p : ℕ}
2958 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
2959 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
2960 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
2961 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2962 let σ :=
2963 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2964 let τ :=
2965 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2966 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2967 let e :=
2969 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2970 let η :=
2972 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2973 η
2974 ((e.symm
2976 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) ^ m₁') ∈
2977 Subgroup.normalClosure (relators τ) := by
2978 classical
2979 dsimp
2980 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
2981 let σ :=
2982 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2983 let τ :=
2984 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2985 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2986 let e :=
2988 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2989 let η :=
2991 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
2993 exact
2994 Subgroup.subset_normalClosure
2995 (Or.inl
2997 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, by
3000 {tailLen p : ℕ}
3001 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3002 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3003 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
3004 (j : Fin tailLen) (k : Fin p) :
3005 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3006 let σ :=
3007 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3008 let τ :=
3009 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3010 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3011 let e :=
3013 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3014 let η :=
3016 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3017 η
3018 ((e.symm
3020 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k)) ^ tail j) ∈
3021 Subgroup.normalClosure (relators τ) := by
3022 classical
3023 dsimp
3024 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3025 let σ :=
3026 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3027 let τ :=
3028 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3029 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3030 let e :=
3032 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3033 let η :=
3035 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3037 exact
3038 Subgroup.subset_normalClosure
3039 (Or.inl
3041 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j, by
3044 {tailLen p : ℕ}
3045 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3046 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3047 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
3048 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3049 let σ :=
3050 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3051 let τ :=
3052 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3053 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3054 let e :=
3056 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3057 let η :=
3059 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3060 η
3061 ((e.symm
3063 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) ^ m₂') ∈
3064 Subgroup.normalClosure (relators τ) := by
3065 classical
3066 dsimp
3067 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3068 let σ :=
3069 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3070 let τ :=
3071 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3072 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3073 let e :=
3075 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3076 let η :=
3078 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3079 let B :=
3082 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3083 have hcongr :
3084 η
3085 (e.symm
3087 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) *
3088 B⁻¹ ∈ Subgroup.normalClosure (relators τ) := by
3089 have hTheta :
3091 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen B =
3092 e.symm
3094 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
3095 simpa [σ, τ, e, B] using
3097 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3098 have hOne :
3099 η
3101 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen B) *
3102 B⁻¹ ∈ Subgroup.normalClosure (relators τ) := by
3103 simpa [σ, τ, η, B] using
3105 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3106 rwa [hTheta] at hOne
3107 have hBpow : B ^ m₂' ∈ Subgroup.normalClosure (relators τ) :=
3108 Subgroup.subset_normalClosure
3109 (Or.inl
3111 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, by
3113 rw [map_pow]
3114 exact ReidemeisterSchreier.Discrete.Presentations.pow_mem_normalClosure_of_mul_inv_mem hcongr hBpow
3116 {tailLen p : ℕ}
3117 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3118 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3119 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
3120 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3121 let σ :=
3122 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3123 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3124 let φ :=
3126 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3127 let x : FuchsianGenerator σ :=
3128 FuchsianGenerator.elliptic
3130 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3131 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3132 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3135 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3136 let hT : IsRightSchreierTransversal φ.ker T :=
3138 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3140 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
3141 rw [MonoidHom.mem_ker, map_pow, hx]
3142 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
3143 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
3144 (e.symm a) ^ m₁' ∈
3145 Subgroup.normalClosure
3150 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3151 (rels := relators σ) T)) := by
3152 classical
3153 dsimp
3154 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3155 let σ :=
3156 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3157 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3158 let φ :=
3160 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3161 let x : FuchsianGenerator σ :=
3162 FuchsianGenerator.elliptic
3164 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3165 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3166 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3169 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3170 let hT : IsRightSchreierTransversal φ.ker T :=
3172 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3174 let hrels :=
3176 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3177 let a : φ.ker := ⟨(FreeGroup.of x) ^ p, by
3178 rw [MonoidHom.mem_ker, map_pow, hx]
3179 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
3180 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩
3181 let i₀ :=
3183 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3184 let r := (xWord σ i₀) ^ σ.periods i₀
3185 have ht : (1 : FreeGroup (FuchsianGenerator σ)) ∈ T := by
3186 have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
3187 simpa [T] using
3189 φ x hx (m := 0) hp_pos
3190 have hr : r ∈ relators σ := Or.inl ⟨i₀, rfl⟩
3191 have hrel :
3192 e.symm
3193 (⟨(1 : FreeGroup (FuchsianGenerator σ)) * r * 1⁻¹, by
3194 change φ ((1 : FreeGroup (FuchsianGenerator σ)) * r * 1⁻¹) = 1
3195 have hrφ : φ r = 1 := hrels r hr
3196 simp only [Lean.Elab.WF.paramLet, one_mul, inv_one, mul_one, hrφ]⟩ : φ.ker) ∈
3197 Subgroup.normalClosure
3202 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3203 (rels := relators σ) T)) :=
3205 change
3206 (e.symm a) ^ m₁' ∈
3207 Subgroup.normalClosure
3212 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3213 (rels := relators σ) T))
3214 have hpow : (e.symm a) ^ m₁' = e.symm (a ^ m₁') :=
3215 (map_pow e.symm a m₁').symm
3216 rw [hpow]
3219 pow_mul] using hrel
3221 {tailLen p : ℕ}
3222 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3223 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3224 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
3225 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3226 let σ :=
3227 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3228 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3229 let φ :=
3231 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3232 let x : FuchsianGenerator σ :=
3233 FuchsianGenerator.elliptic
3235 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3236 let y : FuchsianGenerator σ :=
3237 FuchsianGenerator.elliptic
3239 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3240 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3241 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3244 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3245 let hT : IsRightSchreierTransversal φ.ker T :=
3247 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3249 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
3250 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
3251 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3253 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
3254 rw [MonoidHom.mem_ker, map_pow, hy]
3255 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
3256 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
3257 neg_zero, toAdd_one]⟩
3258 (e.symm b) ^ m₂' ∈
3259 Subgroup.normalClosure
3264 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3265 (rels := relators σ) T)) := by
3266 classical
3267 dsimp
3268 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3269 let σ :=
3270 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3271 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3272 let φ :=
3274 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3275 let x : FuchsianGenerator σ :=
3276 FuchsianGenerator.elliptic
3278 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3279 let y : FuchsianGenerator σ :=
3280 FuchsianGenerator.elliptic
3282 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3283 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3284 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3287 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3288 let hT : IsRightSchreierTransversal φ.ker T :=
3290 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3292 let hrels :=
3294 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3295 let b : φ.ker := ⟨(FreeGroup.of y) ^ p, by
3296 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
3297 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3299 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
3300 rw [MonoidHom.mem_ker, map_pow, hy]
3301 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
3302 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
3303 neg_zero, toAdd_one]⟩
3304 let i₁ :=
3306 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3307 let r := (xWord σ i₁) ^ σ.periods i₁
3308 have ht : (1 : FreeGroup (FuchsianGenerator σ)) ∈ T := by
3309 have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
3310 simpa [T] using
3312 φ x hx (m := 0) hp_pos
3313 have hr : r ∈ relators σ := Or.inl ⟨i₁, rfl⟩
3314 have hrel :
3315 e.symm
3316 (⟨(1 : FreeGroup (FuchsianGenerator σ)) * r * 1⁻¹, by
3317 change φ ((1 : FreeGroup (FuchsianGenerator σ)) * r * 1⁻¹) = 1
3318 have hrφ : φ r = 1 := hrels r hr
3319 simp only [Lean.Elab.WF.paramLet, one_mul, inv_one, mul_one, hrφ]⟩ : φ.ker) ∈
3320 Subgroup.normalClosure
3325 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3326 (rels := relators σ) T)) :=
3328 change
3329 (e.symm b) ^ m₂' ∈
3330 Subgroup.normalClosure
3335 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3336 (rels := relators σ) T))
3337 have hpow : (e.symm b) ^ m₂' = e.symm (b ^ m₂') :=
3338 (map_pow e.symm b m₂').symm
3339 rw [hpow]
3342 pow_mul] using hrel
3344 {tailLen p : ℕ}
3345 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3346 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3347 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
3348 (j : Fin tailLen) (k : Fin p) :
3349 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3350 let σ :=
3351 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3352 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3353 let φ :=
3355 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3356 let x : FuchsianGenerator σ :=
3357 FuchsianGenerator.elliptic
3359 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3360 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
3361 FuchsianGenerator.elliptic
3363 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
3364 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3365 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3368 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3369 let hT : IsRightSchreierTransversal φ.ker T :=
3371 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3373 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
3374 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
3375 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
3376 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
3377 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3379 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
3380 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
3381 omega
3382 rw [MonoidHom.mem_ker]
3383 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
3384 (e.symm (c j k)) ^ tail j ∈
3385 Subgroup.normalClosure
3390 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3391 (rels := relators σ) T)) := by
3392 classical
3393 dsimp
3394 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3395 let σ :=
3396 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3397 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3398 let φ :=
3400 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3401 let x : FuchsianGenerator σ :=
3402 FuchsianGenerator.elliptic
3404 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3405 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
3406 FuchsianGenerator.elliptic
3408 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
3409 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3410 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3413 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3414 let hT : IsRightSchreierTransversal φ.ker T :=
3416 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3418 let hrels :=
3420 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3421 let c : Fin tailLen → Fin p → φ.ker := fun j k =>
3422 ⟨(FreeGroup.of x) ^ (k : ℕ) * FreeGroup.of (tailGen j) *
3423 ((FreeGroup.of x) ^ (k : ℕ))⁻¹, by
3424 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
3425 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3427 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
3428 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
3429 omega
3430 rw [MonoidHom.mem_ker]
3431 simp only [map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]⟩
3432 let iTail :=
3434 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j
3435 let r := (xWord σ iTail) ^ σ.periods iTail
3436 let t : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ (k : ℕ)
3437 have ht : t ∈ T := by
3438 simpa [T, t] using
3440 φ x hx (m := (k : ℕ)) k.isLt
3441 have hr : r ∈ relators σ := Or.inl ⟨iTail, rfl⟩
3442 have hrel :
3443 e.symm
3444 (⟨t * r * t⁻¹, by
3445 change φ (t * r * t⁻¹) = 1
3446 have hrφ : φ r = 1 := hrels r hr
3447 simp only [Lean.Elab.WF.paramLet, map_mul, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) ∈
3448 Subgroup.normalClosure
3453 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3454 (rels := relators σ) T)) :=
3456 change
3457 (e.symm (c j k)) ^ tail j ∈
3458 Subgroup.normalClosure
3463 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3464 (rels := relators σ) T))
3465 have hpow : (e.symm (c j k)) ^ tail j = e.symm ((c j k) ^ tail j) :=
3466 (map_pow e.symm (c j k) (tail j)).symm
3467 rw [hpow]
3468 have htailZero : 2 + j.val ≠ 0 := by omega
3469 have htailOne : 2 + j.val ≠ 1 := by omega
3470 simpa [c, r, iTail, t, x, tailGen, σ, xWord,
3472 firstReductionCanonicalSourcePeriod, htailZero, htailOne, conj_pow, map_pow] using hrel
3474 {tailLen p : ℕ}
3475 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3476 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3477 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
3478 (i :
3479 Fin
3481 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods) :
3482 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3483 let σ :=
3484 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3485 let τ :=
3486 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3487 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3488 let φ :=
3490 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3491 let x : FuchsianGenerator σ :=
3492 FuchsianGenerator.elliptic
3494 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3495 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3496 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3499 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3500 let hT : IsRightSchreierTransversal φ.ker T :=
3502 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3505 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3506 ((xWord τ i) ^ τ.periods i) ∈
3507 Subgroup.normalClosure
3512 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3513 (rels := relators σ) T)) := by
3514 classical
3515 dsimp
3516 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3517 let σ :=
3518 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3519 let τ :=
3520 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3521 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3522 let φ :=
3524 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3525 let x : FuchsianGenerator σ :=
3526 FuchsianGenerator.elliptic
3528 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3529 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3530 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3533 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3534 let hT : IsRightSchreierTransversal φ.ker T :=
3536 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3538 let hrels :=
3540 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3541 let η :=
3543 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3544 by_cases h0 : i.val = 0
3545 · have hi :
3546 i =
3548 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
3549 ext
3551 subst i
3552 rw [map_pow]
3554 simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η] using
3556 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3557 · by_cases h1 : i.val = 1
3558 · have hi :
3559 i =
3561 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
3562 ext
3564 subst i
3565 rw [map_pow]
3567 simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η] using
3569 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3570 · let r : Fin (p * tailLen) := ⟨i.val - 2, by
3571 have hi : i.val < 2 + p * tailLen := by
3573 exact i.isLt
3574 omega⟩
3575 let k : Fin p := ⟨r.val / tailLen, by
3576 exact Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using r.isLt)⟩
3577 let j : Fin tailLen := ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩
3578 have hiTail :
3579 i =
3581 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j := by
3582 simpa [r, k, j] using
3584 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i h0 h1
3585 rw [hiTail]
3586 rw [map_pow]
3588 simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η, r, k, j] using
3590 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k
3592 {tailLen p : ℕ}
3593 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3594 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3595 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
3596 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3597 let σ :=
3598 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3599 let τ :=
3600 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3601 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3602 let φ :=
3604 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3605 let x : FuchsianGenerator σ :=
3606 FuchsianGenerator.elliptic
3608 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3609 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3610 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3613 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3614 let hT : IsRightSchreierTransversal φ.ker T :=
3616 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3618 ∀ r ∈ relators τ,
3620 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r ∈
3621 Subgroup.normalClosure
3626 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3627 (rels := relators σ) T)) := by
3628 classical
3629 dsimp
3630 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3631 let σ :=
3632 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3633 let τ :=
3634 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3635 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3636 let φ :=
3638 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3639 let x : FuchsianGenerator σ :=
3640 FuchsianGenerator.elliptic
3642 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3643 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3644 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3647 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3648 let hT : IsRightSchreierTransversal φ.ker T :=
3650 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3652 let hrels :=
3654 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3655 let η :=
3657 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3658 refine
3660 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3661 (η := η)
3662 ?_ ?_
3663 · dsimp
3664 intro i
3665 simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η] using
3667 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i
3668 · refine
3670 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3671 η ?_ ?_ ?_
3672 · simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η] using
3674 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3675 · simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η] using
3677 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3678 · intro k j
3679 simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η] using
3681 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j
3683 {tailLen p : ℕ}
3684 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3685 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3686 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) : Type :=
3687 (letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3688 let σ :=
3689 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3690 let τ :=
3691 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3692 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3693 let φ :=
3695 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3696 let x : FuchsianGenerator σ :=
3697 FuchsianGenerator.elliptic
3699 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3700 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3701 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3704 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3705 let hT : IsRightSchreierTransversal φ.ker T :=
3707 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3714 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3715 (rels := relators σ) T))
3718 {tailLen p : ℕ}
3719 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3720 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3721 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) : Type :=
3722 (letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3723 let σ :=
3724 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3725 let τ :=
3726 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3727 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3728 let φ :=
3730 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3731 let x : FuchsianGenerator σ :=
3732 FuchsianGenerator.elliptic
3734 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3735 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3736 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3739 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3740 let hT : IsRightSchreierTransversal φ.ker T :=
3742 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3749 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3750 (rels := relators σ) T))
3753 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3755 {tailLen p : ℕ}
3756 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3757 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3758 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
3759 (hMapsRelators :
3760 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3761 let σ :=
3762 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3763 let τ :=
3764 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3765 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3766 let φ :=
3768 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3769 let x : FuchsianGenerator σ :=
3770 FuchsianGenerator.elliptic
3772 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3773 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3774 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3777 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3778 let hT : IsRightSchreierTransversal φ.ker T :=
3780 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3782 let η :=
3784 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3789 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3790 (rels := relators σ) T),
3791 η r ∈ Subgroup.normalClosure (relators τ))
3792 (hToInv :
3793 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3794 let σ :=
3795 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3796 let τ :=
3797 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3798 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3799 let θ :=
3801 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3802 let η :=
3804 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3805 ∀ y : FreeGroup (FuchsianGenerator τ),
3806 η (θ y) * y⁻¹ ∈ Subgroup.normalClosure (relators τ)) :
3808 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
3809 classical
3810 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3811 let σ :=
3812 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3813 let τ :=
3814 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3815 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3816 let φ :=
3818 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3819 let x : FuchsianGenerator σ :=
3820 FuchsianGenerator.elliptic
3822 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3823 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3824 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3827 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3828 let hT : IsRightSchreierTransversal φ.ker T :=
3830 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3832 let hrels :=
3834 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3835 let θ :=
3837 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3838 let η :=
3840 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3841 refine
3842 { toHom := η
3843 mapsRelators := ?_
3844 inv_toHom := ?_
3845 to_invHom := ?_ }
3846 · intro r hr
3847 simpa [σ, τ, φ, x, hx, T, hT, e, hrels, η] using hMapsRelators r hr
3848 · intro w
3849 simpa [σ, τ, φ, x, hx, T, hT, e, hrels, θ, η] using
3851 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen w
3852 · intro y
3853 simpa [σ, τ, θ, η] using hToInv y
3855 {tailLen p : ℕ}
3856 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3857 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3858 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
3859 (hMapsRelators :
3860 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3861 let σ :=
3862 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3863 let τ :=
3864 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3865 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3866 let φ :=
3868 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3869 let x : FuchsianGenerator σ :=
3870 FuchsianGenerator.elliptic
3872 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3873 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3874 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3877 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3878 let hT : IsRightSchreierTransversal φ.ker T :=
3880 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3882 let η :=
3884 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3889 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3890 (rels := relators σ) T),
3891 η r ∈ Subgroup.normalClosure (relators τ))
3892 (hToInvGenerators :
3893 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3894 let σ :=
3895 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3896 let τ :=
3897 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3898 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3899 let θ :=
3901 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3902 let η :=
3904 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3906 η (θ (FreeGroup.of y)) * (FreeGroup.of y)⁻¹ ∈
3907 Subgroup.normalClosure (relators τ)) :
3909 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen :=
3911 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3912 hMapsRelators
3914 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hToInvGenerators)
3916 {tailLen p : ℕ}
3917 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3918 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3919 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
3920 (hMapsRelators :
3921 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3922 let σ :=
3923 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3924 let τ :=
3925 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3926 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3927 let φ :=
3929 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3930 let x : FuchsianGenerator σ :=
3931 FuchsianGenerator.elliptic
3933 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3934 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3935 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3938 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3939 let hT : IsRightSchreierTransversal φ.ker T :=
3941 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3943 let η :=
3945 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3950 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
3951 (rels := relators σ) T),
3952 η r ∈ Subgroup.normalClosure (relators τ)) :
3954 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen :=
3956 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3957 hMapsRelators
3959 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3961 {tailLen p : ℕ}
3962 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
3963 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
3964 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
3965 (D :
3967 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) :
3969 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
3970 classical
3971 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
3972 let σ :=
3973 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3974 let τ :=
3975 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3976 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3977 let φ :=
3979 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3980 let x : FuchsianGenerator σ :=
3981 FuchsianGenerator.elliptic
3983 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
3984 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
3985 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
3988 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
3989 let hT : IsRightSchreierTransversal φ.ker T :=
3991 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
3993 let hrels :=
3995 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
3996 simpa [FirstReductionCanonicalSchreierRelatorData, σ, τ, φ, x, hx, T, hT, e, hrels] using
4002 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
4003 (rels := relators σ) T))
4004 (S := relators τ)
4005 (invHom :=
4007 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
4009 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
4010 D)
4012 {tailLen p : ℕ}
4013 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
4014 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
4015 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
4016 (D :
4018 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) :
4019 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
4020 let σ :=
4021 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4022 let τ :=
4023 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4024 let ξ :=
4026 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4027 let hrels : ∀ r ∈ relators σ,
4028 FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ) r = 1 := by
4031 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4032 (PresentedGroup.toGroup (rels := relators σ)
4033 (f := ellipticQuotientGeneratorImage σ ξ) hrels).ker ≃*
4035 classical
4036 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
4037 let σ :=
4038 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4039 let τ :=
4040 firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4041 let ξ :=
4043 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4044 let hpow : ∀ i, ξ i ^ σ.periods i = 1 :=
4046 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4047 let hprod : ∏ i : Fin σ.numPeriods, ξ i = 1 :=
4049 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4050 let hrels : ∀ r ∈ relators σ,
4051 FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ) r = 1 := by
4054 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4055 let i₀ :=
4057 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4058 have hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p) := by
4060 i₀]
4061 have hData :
4066 simpa [ellipticQuotientHom, σ, τ, ξ, hpow, hprod, hrels] using
4068 σ τ ξ hpow hprod i₀ hi₀ hData
4070 {tailLen p : ℕ}
4071 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
4072 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
4073 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
4074 (D :
4076 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) :=
4078 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
4080 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen D)
4081end FenchelNielsen