FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/QuotientAndBasis.lean
1import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicProductIdentities
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.OrderedTargetSignature
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/QuotientAndBasis.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.
16-/
18namespace FenchelNielsen
19noncomputable def secondReductionCanonicalSourceFreeQuotientHom
20 {tailLen p q : ℕ}
21 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
22 (hp : 2 ≤ p) (hq : 2 ≤ q)
23 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
24 (htail : ∀ j, 2 ≤ tail j) :
25 let σ :=
26 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
27 FreeGroup (FuchsianGenerator σ) →* Multiplicative (ZMod q) := by
28 classical
29 dsimp
30 let σ :=
31 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
32 exact
33 FreeGroup.lift
36 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
37@[simp 900] theorem secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished
38 {tailLen p q : ℕ}
39 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
40 (hp : 2 ≤ p) (hq : 2 ≤ q)
41 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
42 (htail : ∀ j, 2 ≤ tail j) :
44 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
45 (FreeGroup.of
46 (FuchsianGenerator.elliptic
48 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨0, by omega⟩))) =
49 Multiplicative.ofAdd (1 : ZMod q) := by
50 classical
51 dsimp
52 simp only [secondReductionCanonicalSourceFreeQuotientHom, Lean.Elab.WF.paramLet, id_eq,
53 secondReductionCanonicalSourceMiddleIndex, add_zero, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
54 secondReductionCanonicalSourceQuotientImage, ↓reduceIte]
56 {tailLen p q : ℕ}
57 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
58 (hp : 2 ≤ p) (hq : 2 ≤ q)
59 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
60 (htail : ∀ j, 2 ≤ tail j) :
61 let σ :=
62 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
65 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r = 1 := by
66 classical
67 dsimp
68 let σ :=
69 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
70 simpa [secondReductionCanonicalSourceFreeQuotientHom, σ] using
73 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
75 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
77 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
78noncomputable abbrev secondReductionCanonicalDistinguishedGenerator
79 {tailLen p q : ℕ}
80 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
81 (hp : 2 ≤ p) (hq : 2 ≤ q)
82 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
83 (htail : ∀ j, 2 ≤ tail j) :
86 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) :=
87 FuchsianGenerator.elliptic
89 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨0, by omega⟩)
90noncomputable def secondReductionCanonicalSchreierTransversal
91 {tailLen p q : ℕ}
92 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
93 (hp : 2 ≤ p) (hq : 2 ≤ q)
94 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
95 (htail : ∀ j, 2 ≤ tail j) :
96 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
97 let σ :=
98 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
99 Set (FreeGroup (FuchsianGenerator σ)) := by
100 classical
101 dsimp
102 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
103 let σ :=
104 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
105 let φ :=
107 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
108 let x : FuchsianGenerator σ :=
110 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
111 exact Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
113 {tailLen p q : ℕ}
114 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
115 (hp : 2 ≤ p) (hq : 2 ≤ q)
116 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
117 (htail : ∀ j, 2 ≤ tail j) :
118 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
119 let σ :=
120 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
121 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
122 let φ :=
124 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
127 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) := by
128 classical
129 dsimp
130 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
131 let σ :=
132 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
133 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
134 let φ :=
136 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
137 let x : FuchsianGenerator σ :=
139 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
140 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
141 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
142 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
143 simpa [secondReductionCanonicalSchreierTransversal, σ, φ, x] using
145noncomputable def secondReductionCanonicalSchreierBasisEquiv
146 {tailLen p q : ℕ}
147 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
148 (hp : 2 ≤ p) (hq : 2 ≤ q)
149 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
150 (htail : ∀ j, 2 ≤ tail j) :
151 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
152 let σ :=
153 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
154 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
155 let φ :=
157 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
158 let hT :=
160 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
161 FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker := by
162 classical
163 dsimp
164 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
165 let σ :=
166 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
167 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
168 let φ :=
170 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
171 let x : FuchsianGenerator σ :=
173 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
174 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
175 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
176 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
177 simpa [secondReductionCanonicalSchreierTransversal, σ, φ, x] using
179@[simp 900] theorem secondReductionCanonicalSchreierBasisEquiv_symm_apply
180 {tailLen p q : ℕ}
181 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
182 (hp : 2 ≤ p) (hq : 2 ≤ q)
183 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
184 (htail : ∀ j, 2 ≤ tail j) :
185 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
186 let σ :=
187 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
188 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
189 let φ :=
191 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
192 let hT :=
194 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
195 ∀ z : ↥(schreierGeneratorSet hT),
197 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm (z : φ.ker) =
198 (FreeGroup.of z)⁻¹ := by
199 classical
200 dsimp
201 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
202 let σ :=
203 secondReductionCanonicalSourceSignature m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
204 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
205 let φ :=
207 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
208 let x : FuchsianGenerator σ :=
210 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
211 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
212 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
213 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
214 intro z
215 let e :=
217 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
218 apply e.injective
219 simp only [secondReductionCanonicalSchreierTransversal, Lean.Elab.WF.paramLet, id_eq,
220 secondReductionCanonicalSchreierBasisEquiv, MulEquiv.apply_symm_apply, map_inv,
221 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator_of φ x hx z, inv_inv, e, φ, x]
224 {tailLen p q : ℕ}
225 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
226 (hp : 2 ≤ p) (hq : 2 ≤ q)
227 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
228 (htail : ∀ j, 2 ≤ tail j)
229 (τ : FuchsianSignature)
230 (η :
231 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
232 let σ :=
234 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
235 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
236 let hT :=
238 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
239 FreeGroup ↥(schreierGeneratorSet hT) →* FreeGroup (FuchsianGenerator τ))
240 (targetRelators : Set (FreeGroup (FuchsianGenerator τ)))
241 (hZero :
242 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
243 let σ :=
245 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
246 let φ :=
248 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
249 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
250 let e :=
252 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
253 let x : FuchsianGenerator σ :=
255 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
256 let i₀ :=
258 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
259 ∀ k : Fin q,
260 η
261 (e.symm
263 ((FreeGroup.of x) ^ k.val)⁻¹, by
264 change φ
266 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
267 have hrφ :
270 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
272 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
273 Subgroup.normalClosure targetRelators)
274 (hOne :
275 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
276 let σ :=
278 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
279 let φ :=
281 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
282 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
283 let e :=
285 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
286 let x : FuchsianGenerator σ :=
288 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
289 let i₁ :=
291 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
292 ∀ k : Fin q,
293 η
294 (e.symm
296 ((FreeGroup.of x) ^ k.val)⁻¹, by
297 change φ
299 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
300 have hrφ :
303 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
305 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
306 Subgroup.normalClosure targetRelators)
307 (hMiddle :
308 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
309 let σ :=
311 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
312 let φ :=
314 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
315 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
316 let e :=
318 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
319 let x : FuchsianGenerator σ :=
321 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
322 ∀ r : Fin p, ∀ k : Fin q,
323 let iMiddle :=
325 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r
326 η
327 (e.symm
329 ((FreeGroup.of x) ^ k.val)⁻¹, by
330 change φ
332 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
333 have hrφ :
336 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
338 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
339 Subgroup.normalClosure targetRelators)
340 (hTail :
341 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
342 let σ :=
344 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
345 let φ :=
347 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
348 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
349 let e :=
351 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
352 let x : FuchsianGenerator σ :=
354 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
355 ∀ b : Fin p, ∀ j : Fin tailLen, ∀ k : Fin q,
356 let iTail :=
358 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j
359 η
360 (e.symm
362 ((FreeGroup.of x) ^ k.val)⁻¹, by
363 change φ
365 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
366 have hrφ :
369 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
371 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
372 Subgroup.normalClosure targetRelators)
373 (hTotal :
374 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
375 let σ :=
377 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
378 let φ :=
380 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
381 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
382 let e :=
384 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
385 let x : FuchsianGenerator σ :=
387 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
388 ∀ k : Fin q,
389 η
390 (e.symm
391 (⟨(FreeGroup.of x) ^ k.val * totalRelation σ *
392 ((FreeGroup.of x) ^ k.val)⁻¹, by
393 change φ
394 ((FreeGroup.of x) ^ k.val * totalRelation σ *
395 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
396 have hrφ : φ (totalRelation σ) = 1 :=
398 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
399 (totalRelation σ) (Or.inr rfl)
400 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈
401 Subgroup.normalClosure targetRelators) :
402 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
403 let σ :=
405 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
406 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
407 let φ :=
409 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
410 let x : FuchsianGenerator σ :=
412 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
413 let hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
414 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
415 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
416 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
417 let hT : IsRightSchreierTransversal φ.ker T :=
419 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
423 (f := ellipticQuotientGeneratorImage σ
425 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
427 η r ∈ Subgroup.normalClosure targetRelators := by
428 classical
429 dsimp
430 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
431 let σ :=
433 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
434 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
435 let φ :=
437 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
438 let x : FuchsianGenerator σ :=
440 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
441 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
442 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
443 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
444 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
445 let hT : IsRightSchreierTransversal φ.ker T :=
447 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
449 let hrels :=
451 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
452 intro r hr
453 have hrImage :
454 e r ∈
456 (f := ellipticQuotientGeneratorImage σ
458 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
460 simpa [e] using
463 (f := ellipticQuotientGeneratorImage σ
465 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
467 (y := r)).1 hr
468 rcases hrImage with ⟨t, ht, r₀, hr₀, hval⟩
469 have htPower : ∃ k : Fin q, t = (FreeGroup.of x) ^ k.val := by
470 simpa [T] using
471 (mem_range_cyclicQuotientRightRep_iff_generatorPower φ (x := x) hx).1 ht
472 rcases htPower with ⟨k, rfl⟩
473 let tPow : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ k.val
474 have relator_eq :
475 r =
476 e.symm
477 (⟨tPow * r₀ * tPow⁻¹, by
478 change φ (tPow * r₀ * tPow⁻¹) = 1
479 have hrφ : φ r₀ = 1 := hrels r₀ hr₀
480 simp only [Lean.Elab.WF.paramLet, map_mul, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) := by
481 let zRel : φ.ker :=
482 ⟨tPow * r₀ * tPow⁻¹, by
483 change φ (tPow * r₀ * tPow⁻¹) = 1
484 have hrφ : φ r₀ = 1 := hrels r₀ hr₀
486 have hz : e r = zRel := by
487 apply Subtype.ext
488 simpa [tPow, zRel] using hval
489 calc
490 r = e.symm (e r) := by simp only [MulEquiv.symm_apply_apply]
491 _ = e.symm zRel := by rw [hz]
492 rcases hr₀ with ⟨i, rfl⟩ | rfl
493 · by_cases h0 : i.val = 0
494 · have hi :
495 i =
497 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
498 ext
499 simpa [secondReductionCanonicalSourceZeroIndex] using h0
500 subst i
501 rw [relator_eq]
502 simpa [σ, φ, e, x, tPow] using hZero k
503 · by_cases h1 : i.val = 1
504 · have hi :
505 i =
507 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
508 ext
509 simpa [secondReductionCanonicalSourceOneIndex] using h1
510 subst i
511 rw [relator_eq]
512 simpa [σ, φ, e, x, tPow] using hOne k
513 · by_cases hmid : i.val < 2 + p
514 · let rMid : Fin p := ⟨i.val - 2, by omega⟩
515 have hiMid :
516 i =
518 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail rMid := by
519 ext
520 simp only [secondReductionCanonicalSourceMiddleIndex, rMid]
521 omega
522 rw [relator_eq]
523 simpa [σ, φ, e, x, tPow, hiMid] using hMiddle rMid k
524 · have htailLen_pos : 0 < tailLen := by
525 by_contra htl
526 have htl0 : tailLen = 0 := Nat.eq_zero_of_not_pos htl
527 have hlt : i.val < 2 + p := by
528 have hi_lt : i.val < 2 + (p + tailLen * p) := by
529 change i.val < 2 + (p + tailLen * p)
530 exact i.isLt
531 have hprod0 : tailLen * p = 0 := by
532 rw [htl0]
533 simp only [zero_mul]
534 omega
535 exact hmid hlt
536 let n : ℕ := i.val - (2 + p)
537 have hnlt : n < tailLen * p := by
538 have hi_lt : i.val < 2 + (p + tailLen * p) := by
539 change i.val < 2 + (p + tailLen * p)
540 exact i.isLt
541 dsimp [n]
542 omega
543 let b : Fin p := ⟨n / tailLen, by
544 have hdiv : n / tailLen < p := by
545 rw [Nat.div_lt_iff_lt_mul htailLen_pos]
546 simpa [Nat.mul_comm] using hnlt
547 exact hdiv⟩
548 let j : Fin tailLen := ⟨n % tailLen, Nat.mod_lt _ htailLen_pos⟩
549 have hn_eq : n = b.val * tailLen + j.val := by
550 dsimp [b, j]
551 rw [Nat.mul_comm, Nat.add_comm]
552 exact (Nat.mod_add_div n tailLen).symm
553 have hi_val : i.val = 2 + p + b.val * tailLen + j.val := by
554 dsimp [n] at hn_eq
555 omega
556 have hiTail :
557 i =
559 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j := by
560 ext
561 simp only [hi_val, secondReductionCanonicalSourceTailIndex]
562 rw [relator_eq]
563 simpa [σ, φ, e, x, tPow, hiTail] using hTail b j k
564 · rw [relator_eq]
565 simpa [σ, φ, e, x, tPow] using hTotal k
567abbrev SecondReductionCanonicalOrderedTargetIndex (tailLen p q : ℕ) :=
568 Fin 2 ⊕
569 (Fin q × (Fin (p - 2) ⊕ ((Fin p × Fin tailLen) ⊕ Fin 2)))
572 (tailLen p q : ℕ) :
573 SecondReductionTransportIndex tailLen p q ≃
574 SecondReductionCanonicalOrderedTargetIndex tailLen p q where
575 toFun
576 | ⟨.inl h, k⟩ => .inr (k, .inr (.inr h))
577 | ⟨.inr (.inl d), _⟩ => .inl d
578 | ⟨.inr (.inr (.inl r)), k⟩ => .inr (k, .inl r)
579 | ⟨.inr (.inr (.inr jk)), k⟩ => .inr (k, .inr (.inl (jk.2, jk.1)))
580 invFun
581 | .inl d => ⟨.inr (.inl d), (0 : Fin 1)⟩
582 | .inr (k, .inl r) => ⟨.inr (.inr (.inl r)), k⟩
583 | .inr (k, .inr (.inl bj)) => ⟨.inr (.inr (.inr (bj.2, bj.1))), k⟩
584 | .inr (k, .inr (.inr h)) => ⟨.inl h, k⟩
585 left_inv x := by
586 rcases x with ⟨src, k⟩
587 cases src with
588 | inl _ => rfl
589 | inr rest =>
590 cases rest with
591 | inl _ =>
592 fin_cases k
593 rfl
594 | inr rest =>
595 cases rest with
596 | inl _ => rfl
597 | inr _ => rfl
598 right_inv x := by
599 cases x with
600 | inl _ => rfl
601 | inr rest =>
602 rcases rest with ⟨_, block⟩
603 cases block with
604 | inl _ => rfl
605 | inr rest =>
606 cases rest with
607 | inl bj =>
608 rcases bj with ⟨_, _⟩
609 rfl
610 | inr _ => rfl
612 (tailLen p : ℕ) :
613 (Fin (p - 2) ⊕ ((Fin p × Fin tailLen) ⊕ Fin 2)) ≃
614 Fin (secondReductionCanonicalOrderedTargetBlockLen tailLen p) :=
615 ((Equiv.sumCongr (Equiv.refl (Fin (p - 2)))
616 ((Equiv.sumCongr finProdFinEquiv (Equiv.refl (Fin 2))).trans
617 finSumFinEquiv)).trans finSumFinEquiv).trans
618 (finCongr (by
620 omega))
622 (tailLen p q : ℕ) :
623 SecondReductionCanonicalOrderedTargetIndex tailLen p q ≃
624 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
625 (Equiv.sumCongr (Equiv.refl (Fin 2))
626 ((Equiv.prodCongr (Equiv.refl (Fin q))
627 (secondReductionCanonicalOrderedTargetBlockIndexEquivFin tailLen p)).trans
628 finProdFinEquiv)).trans
629 finSumFinEquiv
631 (tailLen p q : ℕ) :
632 SecondReductionTransportIndex tailLen p q ≃
633 Fin (secondReductionCanonicalOrderedTargetNumPeriods tailLen p q) :=
634 (secondReductionTransportIndexEquivCanonicalOrderedTargetIndex tailLen p q).trans
635 (secondReductionCanonicalOrderedTargetIndexEquivFin tailLen p q)
636private theorem secondReduction_negOneCycleSegmentProduct_eq {G : Type*} [Group G]
637 (x y : G) : ∀ (n l : ℕ), l ≤ n →
638 (List.ofFn (fun i : Fin l =>
639 x ^ (n - i.val) * y * (x ^ (n - 1 - i.val))⁻¹)).prod =
640 x ^ n * y ^ l * (x ^ (n - l))⁻¹
641 | n, 0, _ => by
642 simp only [List.ofFn_zero, List.prod_nil, pow_zero, mul_one, tsub_zero, mul_inv_cancel]
643 | n, l + 1, h => by
644 have hl : l ≤ n - 1 := by omega
645 rw [List.ofFn_succ, List.prod_cons]
646 simp only [Fin.val_zero, tsub_zero]
647 change
648 x ^ n * y * (x ^ (n - 1))⁻¹ *
649 (List.ofFn (fun i : Fin l =>
650 x ^ (n - (i.val + 1)) * y * (x ^ (n - 1 - (i.val + 1)))⁻¹)).prod =
651 x ^ n * y ^ (l + 1) * (x ^ (n - (l + 1)))⁻¹
652 have htail :
653 (List.ofFn (fun i : Fin l =>
654 x ^ (n - (i.val + 1)) * y * (x ^ (n - 1 - (i.val + 1)))⁻¹)).prod =
655 (List.ofFn (fun i : Fin l =>
656 x ^ (n - 1 - i.val) * y * (x ^ (n - 1 - 1 - i.val))⁻¹)).prod := by
657 congr
658 funext i
659 have h1 : n - (i.val + 1) = n - 1 - i.val := by omega
660 have h2 : n - 1 - (i.val + 1) = n - 1 - 1 - i.val := by omega
661 simp only [h1, h2]
662 rw [htail]
663 rw [secondReduction_negOneCycleSegmentProduct_eq x y (n - 1) l hl]
664 have hnl : n - 1 - l = n - (l + 1) := by omega
665 rw [hnl]
666 rw [pow_succ']
667 group
668theorem secondReduction_list_ofFn_desc_split {α : Type*} {p k : ℕ} (hk : k < p)
669 (f : Fin p → α) :
670 List.ofFn (fun i : Fin (p - 1) => f ⟨p - 1 - i.val, by omega⟩) =
671 List.ofFn (fun i : Fin (p - 1 - k) => f ⟨p - 1 - i.val, by omega⟩) ++
672 List.ofFn (fun i : Fin k => f ⟨k - i.val, by omega⟩) := by
673 let a : Fin (p - 1 - k) → α :=
674 fun i => f ⟨p - 1 - i.val, by omega⟩
675 let b : Fin k → α :=
676 fun i => f ⟨k - i.val, by omega⟩
677 have hlen : p - 1 = (p - 1 - k) + k := by omega
678 rw [List.ofFn_congr hlen]
679 rw [← List.ofFn_fin_append a b]
680 congr
681 funext i
682 cases i using Fin.addCases with
683 | left r =>
684 dsimp [a, b]
685 rw [Fin.append_left]
686 | right j =>
687 dsimp [a, b]
688 rw [Fin.append_right]
689 apply congrArg f
690 ext
691 simp only
692 omega
694 {G : Type*} [Group G] {R : Set G}
695 (x y h₀ h₁ : G) {middleLen tailLen p q : ℕ}
696 (middle : Fin middleLen → G) (tail : Fin p → Fin tailLen → G)
697 (h :
698 x * y *
699 ((List.ofFn middle).prod *
700 (List.ofFn (fun b : Fin p =>
701 (List.ofFn (fun j : Fin tailLen => tail b j)).prod)).prod *
702 h₀ * h₁) ∈
703 Subgroup.normalClosure R) :
704 x ^ q * y ^ q *
705 (List.ofFn (fun k : Fin q =>
706 (List.ofFn (fun r : Fin middleLen =>
707 x ^ k.val * middle r * (x ^ k.val)⁻¹)).prod *
708 (List.ofFn (fun b : Fin p =>
709 (List.ofFn (fun j : Fin tailLen =>
710 x ^ k.val * tail b j * (x ^ k.val)⁻¹)).prod)).prod *
711 (x ^ k.val * h₀ * (x ^ k.val)⁻¹) *
712 (x ^ k.val * h₁ * (x ^ k.val)⁻¹))).prod ∈
713 Subgroup.normalClosure R := by
714 classical
715 let N : Subgroup G := Subgroup.normalClosure R
716 let Q : G →* G ⧸ N := QuotientGroup.mk' N
717 let z : G :=
718 (List.ofFn middle).prod *
719 (List.ofFn (fun b : Fin p =>
720 (List.ofFn (fun j : Fin tailLen => tail b j)).prod)).prod *
721 h₀ * h₁
722 have hzRel : Q x * Q y * Q z = 1 := by
723 have hq : Q (x * y * z) = 1 :=
724 (QuotientGroup.eq_one_iff (N := N) (x * y * z)).2 (by simpa [N, z] using h)
726 have hcycle :
727 Q x ^ q * Q y ^ q * conjugateRangeProduct (Q x) (Q z) q = 1 :=
728 pow_mul_pow_mul_conjugateRangeProduct_eq_one_of_mul_eq_one (Q x) (Q y) (Q z) q hzRel
729 have hblock :
730 Q
731 (x ^ q * y ^ q *
732 (List.ofFn (fun k : Fin q =>
733 (List.ofFn (fun r : Fin middleLen =>
734 x ^ k.val * middle r * (x ^ k.val)⁻¹)).prod *
735 (List.ofFn (fun b : Fin p =>
736 (List.ofFn (fun j : Fin tailLen =>
737 x ^ k.val * tail b j * (x ^ k.val)⁻¹)).prod)).prod *
738 (x ^ k.val * h₀ * (x ^ k.val)⁻¹) *
739 (x ^ k.val * h₁ * (x ^ k.val)⁻¹))).prod) =
740 Q x ^ q * Q y ^ q * conjugateRangeProduct (Q x) (Q z) q := by
742 congr 2
743 rw [← List.ofFn_eq_map]
744 apply List.ofFn_inj.2
745 funext k
746 have hmiddle :
747 (List.ofFn (fun r : Fin middleLen =>
748 Q x ^ k.val * Q (middle r) * (Q x ^ k.val)⁻¹)).prod =
749 Q x ^ k.val * (List.ofFn (fun r : Fin middleLen => Q (middle r))).prod *
750 (Q x ^ k.val)⁻¹ := by
751 simpa using
752 (ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod (Q x ^ k.val)
753 (List.ofFn (fun r : Fin middleLen => Q (middle r)))).symm
754 have htail :
755 (List.ofFn (fun b : Fin p =>
756 (List.ofFn (fun j : Fin tailLen =>
757 Q x ^ k.val * Q (tail b j) * (Q x ^ k.val)⁻¹)).prod)).prod =
758 Q x ^ k.val *
759 (List.ofFn (fun b : Fin p =>
760 (List.ofFn (fun j : Fin tailLen => Q (tail b j))).prod)).prod *
761 (Q x ^ k.val)⁻¹ := by
762 simpa using
763 ReidemeisterSchreier.Discrete.Presentations.nested_conjugate_list_prod (Q x ^ k.val)
764 (fun b : Fin p => fun j : Fin tailLen => Q (tail b j))
765 simp only [Function.comp_apply, map_mul, map_list_prod, List.map_ofFn, Function.comp_def, map_pow, map_inv,
766 hmiddle, htail, conj_mul, z]
767 have htarget :
768 Q
769 (x ^ q * y ^ q *
770 (List.ofFn (fun k : Fin q =>
771 (List.ofFn (fun r : Fin middleLen =>
772 x ^ k.val * middle r * (x ^ k.val)⁻¹)).prod *
773 (List.ofFn (fun b : Fin p =>
774 (List.ofFn (fun j : Fin tailLen =>
775 x ^ k.val * tail b j * (x ^ k.val)⁻¹)).prod)).prod *
776 (x ^ k.val * h₀ * (x ^ k.val)⁻¹) *
777 (x ^ k.val * h₁ * (x ^ k.val)⁻¹))).prod) = 1 := by
778 rw [hblock, hcycle]
779 exact
780 (QuotientGroup.eq_one_iff
781 (N := N)
782 (x ^ q * y ^ q *
783 (List.ofFn (fun k : Fin q =>
784 (List.ofFn (fun r : Fin middleLen =>
785 x ^ k.val * middle r * (x ^ k.val)⁻¹)).prod *
786 (List.ofFn (fun b : Fin p =>
787 (List.ofFn (fun j : Fin tailLen =>
788 x ^ k.val * tail b j * (x ^ k.val)⁻¹)).prod)).prod *
789 (x ^ k.val * h₀ * (x ^ k.val)⁻¹) *
790 (x ^ k.val * h₁ * (x ^ k.val)⁻¹))).prod)).1
791 (by simpa [N, Q] using htarget)
793 (tailLen p q : ℕ) (d : Fin 2) :
794 SecondReductionTransportIndex tailLen p q :=
795 ⟨Sum.inr (Sum.inl d), ⟨0, by simp only [secondReductionSourceCycleCount, zero_lt_one]⟩⟩
797 (tailLen p q : ℕ) (h : Fin 2) (k : Fin q) :
798 SecondReductionTransportIndex tailLen p q :=
799 ⟨Sum.inl h, by simpa [secondReductionSourceCycleCount] using k⟩
801 (tailLen p q : ℕ) (r : Fin (p - 2)) (k : Fin q) :
802 SecondReductionTransportIndex tailLen p q :=
803 ⟨Sum.inr (Sum.inr (Sum.inl r)), by simpa [secondReductionSourceCycleCount] using k⟩
805 (tailLen p q : ℕ) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
806 SecondReductionTransportIndex tailLen p q :=
807 ⟨Sum.inr (Sum.inr (Sum.inr (j, b))), by simpa [secondReductionSourceCycleCount] using k⟩
808noncomputable def secondReductionCanonicalTransportTargetWord
809 {tailLen p q : ℕ}
810 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
811 (hq : 2 ≤ q)
812 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
813 (htail : ∀ j, 2 ≤ tail j) :
814 let τ :=
815 secondReductionTransportSignature (p := p) hq
816 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
817 SecondReductionTransportIndex tailLen p q →
818 FreeGroup (FuchsianGenerator τ) := by
819 classical
820 dsimp
821 let τ :=
822 secondReductionTransportSignature (p := p) hq
823 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
824 intro idx
825 exact xWord τ ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
826@[local simp]
828 {m n : ℕ} (i : Fin m) (j : Fin n) :
829 (finProdFinEquiv (i, j) : Fin (m * n)).val = i.val * n + j.val := by
830 simp only [finProdFinEquiv, Equiv.coe_fn_mk, Nat.mul_comm, Nat.add_comm]
832 (tailLen p q : ℕ) (d : Fin 2) :
834 (secondReductionCanonicalTransportDistinguishedIndex tailLen p q d) =
835 secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q d := by
836 ext
837 change
838 (finSumFinEquiv (Sum.inl d) :
839 Fin (2 + q * secondReductionCanonicalOrderedTargetBlockLen tailLen p)).val =
840 (secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q d).val
841 simp only [finSumFinEquiv_apply_left, Fin.val_castAdd,
843@[local simp]
844theorem
845 secondReductionCanonicalOrderedTargetBlockIndexEquivFin_middleRest_val
846 (tailLen p : ℕ) (r : Fin (p - 2)) :
847 ((secondReductionCanonicalOrderedTargetBlockIndexEquivFin tailLen p) (Sum.inl r)).val =
848 r.val := by
849 simp only [secondReductionCanonicalOrderedTargetBlockIndexEquivFin, Equiv.trans_apply, Equiv.sumCongr_apply,
850 Equiv.coe_refl, Equiv.coe_trans, Sum.map_inl, id_eq, finSumFinEquiv_apply_left, finCongr_apply, Fin.val_cast,
851 Fin.val_castAdd]
852@[local simp]
853theorem
854 secondReductionCanonicalOrderedTargetBlockIndexEquivFin_tail_val
855 (tailLen p : ℕ) (b : Fin p) (j : Fin tailLen) :
857 (Sum.inr (Sum.inl (b, j)))).val =
858 (p - 2) + b.val * tailLen + j.val := by
859 simp only [secondReductionCanonicalOrderedTargetBlockLen,
860 secondReductionCanonicalOrderedTargetBlockIndexEquivFin, finProdFinEquiv, Equiv.trans_apply, Equiv.sumCongr_apply,
861 Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr, Function.comp_apply, Equiv.coe_fn_mk, Sum.map_inl,
862 finSumFinEquiv_apply_left, Fin.castAdd_mk, finSumFinEquiv_apply_right, Fin.natAdd_mk, Nat.add_comm, Nat.add_assoc,
863 finCongr_apply, Fin.cast_mk, Nat.mul_comm]
864@[local simp]
865theorem
866 secondReductionCanonicalOrderedTargetBlockIndexEquivFin_head_val
867 (tailLen p : ℕ) (h : Fin 2) :
869 (Sum.inr (Sum.inr h))).val =
870 (p - 2) + p * tailLen + h.val := by
871 simp only [secondReductionCanonicalOrderedTargetBlockLen,
872 secondReductionCanonicalOrderedTargetBlockIndexEquivFin, finProdFinEquiv, Equiv.trans_apply, Equiv.sumCongr_apply,
873 Equiv.coe_refl, Equiv.coe_trans, Sum.map_inr, Function.comp_apply, Equiv.coe_fn_mk, id_eq,
874 finSumFinEquiv_apply_right, finCongr_apply, Fin.val_cast, Fin.val_natAdd, Nat.mul_comm, Nat.add_comm, Nat.add_assoc]
876 (tailLen p q : ℕ) (h : Fin 2) (k : Fin q) :
878 (secondReductionCanonicalTransportHeadIndex tailLen p q h k) =
879 secondReductionCanonicalOrderedTargetHeadIndex tailLen p q h k := by
880 ext
881 change
882 2 +
883 (finProdFinEquiv
884 (k, (secondReductionCanonicalOrderedTargetBlockIndexEquivFin tailLen p)
885 (Sum.inr (Sum.inr h))) :
886 Fin (q * secondReductionCanonicalOrderedTargetBlockLen tailLen p)).val =
887 (secondReductionCanonicalOrderedTargetHeadIndex tailLen p q h k).val
889 simp only [secondReductionCanonicalOrderedTargetBlockIndexEquivFin_head_val,
891 omega
893 (tailLen p q : ℕ) (r : Fin (p - 2)) (k : Fin q) :
895 (secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k) =
896 secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k := by
897 ext
898 change
899 2 +
900 (finProdFinEquiv
901 (k, (secondReductionCanonicalOrderedTargetBlockIndexEquivFin tailLen p)
902 (Sum.inl r)) :
903 Fin (q * secondReductionCanonicalOrderedTargetBlockLen tailLen p)).val =
904 (secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k).val
906 simp only [secondReductionCanonicalOrderedTargetBlockIndexEquivFin_middleRest_val,
908 omega
910 (tailLen p q : ℕ) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
912 (secondReductionCanonicalTransportTailIndex tailLen p q b j k) =
913 secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k := by
914 ext
915 change
916 2 +
917 (finProdFinEquiv
918 (k, (secondReductionCanonicalOrderedTargetBlockIndexEquivFin tailLen p)
919 (Sum.inr (Sum.inl (b, j)))) :
920 Fin (q * secondReductionCanonicalOrderedTargetBlockLen tailLen p)).val =
921 (secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k).val
923 simp only [secondReductionCanonicalOrderedTargetBlockIndexEquivFin_tail_val,
925 omega
926private theorem secondReductionCanonicalOrderedTarget_period_transportIndex
927 {tailLen p q : ℕ}
928 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
929 (hp : 2 ≤ p) (hq : 2 ≤ q)
930 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
931 (htail : ∀ j, 2 ≤ tail j)
932 (idx : SecondReductionTransportIndex tailLen p q) :
934 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
935 (secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q idx) =
936 secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail idx := by
937 classical
938 let υ :=
940 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
941 change υ.periods
942 (secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q idx) =
943 secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail idx
944 rcases idx with ⟨src, k⟩
945 cases src with
946 | inl h =>
947 have hidx :
948 secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q ⟨Sum.inl h, k⟩ =
949 secondReductionCanonicalOrderedTargetHeadIndex tailLen p q h k := by
950 simpa [secondReductionCanonicalTransportHeadIndex] using
951 secondReductionTransportIndexEquivCanonicalOrderedTargetFin_head tailLen p q h k
952 rw [hidx]
953 fin_cases h
957 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
961 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
962 | inr rest =>
963 cases rest with
964 | inl d =>
965 fin_cases k
966 change υ.periods
968 ⟨Sum.inr (Sum.inl d), (0 : Fin 1)⟩) =
969 secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail
970 ⟨Sum.inr (Sum.inl d), (0 : Fin 1)⟩
971 have hidx :
973 ⟨Sum.inr (Sum.inl d), (0 : Fin 1)⟩ =
974 secondReductionCanonicalOrderedTargetDistinguishedIndex tailLen p q d := by
975 simpa [secondReductionCanonicalTransportDistinguishedIndex] using
977 rw [hidx]
978 fin_cases d <;>
979 simp only [Fin.mk_one, Fin.isValue, secondReductionCanonicalOrderedTargetSignature_period_distinguished,
980 secondReductionTransportPeriods, singermanTransportPeriodsFamily, secondReductionSourceTransportPeriods, υ]
981 | inr rest =>
982 cases rest with
983 | inl r =>
984 have hidx :
986 ⟨Sum.inr (Sum.inr (Sum.inl r)), k⟩ =
987 secondReductionCanonicalOrderedTargetMiddleRestIndex tailLen p q r k := by
988 simpa [secondReductionCanonicalTransportMiddleRestIndex] using
990 tailLen p q r k
991 rw [hidx]
992 simp only [secondReductionCanonicalOrderedTargetSignature_period_middleRest, secondReductionTransportPeriods,
994 | inr jk =>
995 rcases jk with ⟨j, b⟩
996 have hidx :
998 ⟨Sum.inr (Sum.inr (Sum.inr (j, b))), k⟩ =
999 secondReductionCanonicalOrderedTargetTailIndex tailLen p q b j k := by
1000 simpa [secondReductionCanonicalTransportTailIndex] using
1002 tailLen p q b j k
1003 rw [hidx]
1004 simp only [secondReductionCanonicalOrderedTargetSignature_period_tail, secondReductionTransportPeriods,
1007 {tailLen p q : ℕ}
1008 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1009 (hp : 2 ≤ p) (hq : 2 ≤ q)
1010 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1011 (htail : ∀ j, 2 ≤ tail j) :
1012 Nonempty
1015 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1016 ≃*
1018 (secondReductionTransportSignature (p := p) hq
1019 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)) := by
1020 classical
1021 refine
1024 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1025 (secondReductionTransportSignature (p := p) hq
1026 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
1027 ?_ ?_
1029 (Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) ?_
1030 · simp only [secondReductionCanonicalOrderedTargetSignature]
1031 · simp only [secondReductionTransportSignature, familyFuchsianSignature]
1032 · intro idx
1033 calc
1035 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).periods
1036 (secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q idx) =
1037 secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail idx := by
1038 exact
1040 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail idx
1041 _ =
1042 (secondReductionTransportSignature (p := p) hq
1043 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail).periods
1044 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx) := by
1046noncomputable def secondReductionCanonicalTransportFinEquivOrderedTargetFin
1047 {tailLen p q : ℕ}
1048 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1049 (hp : 2 ≤ p) (hq : 2 ≤ q)
1050 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1051 (htail : ∀ j, 2 ≤ tail j) :
1052 Fin
1053 (secondReductionTransportSignature (p := p) hq
1054 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail).numPeriods ≃
1055 Fin
1057 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).numPeriods := by
1058 let τ :=
1059 secondReductionTransportSignature (p := p) hq
1060 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
1061 let υ :=
1063 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1064 have hτ :
1065 τ.numPeriods = Fintype.card (SecondReductionTransportIndex tailLen p q) := by
1066 simp only [secondReductionTransportSignature, familyFuchsianSignature, Fintype.card_sigma, Fintype.card_fin,
1067 Fintype.sum_sum_type, Fin.sum_univ_two, Fin.isValue, τ]
1068 have hυ :
1069 υ.numPeriods = secondReductionCanonicalOrderedTargetNumPeriods tailLen p q := by
1070 simp only [secondReductionCanonicalOrderedTargetSignature, υ]
1071 exact
1072 (finCongr hτ).trans
1073 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)).symm.trans
1074 ((secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q).trans
1075 (finCongr hυ.symm)))
1077 {tailLen p q : ℕ}
1078 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1079 (hp : 2 ≤ p) (hq : 2 ≤ q)
1080 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1081 (htail : ∀ j, 2 ≤ tail j)
1082 (idx : SecondReductionTransportIndex tailLen p q) :
1084 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1085 ((Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx) =
1086 secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q idx := by
1087 simp only [secondReductionCanonicalTransportFinEquivOrderedTargetFin, finCongr_refl, Equiv.trans_refl,
1088 Equiv.refl_trans, Equiv.trans_apply]
1089 exact congrArg (secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q)
1090 (Equiv.symm_apply_apply
1091 (Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx)
1092noncomputable def secondReductionCanonicalTransportGeneratorEquivOrderedTarget
1093 {tailLen p q : ℕ}
1094 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1095 (hp : 2 ≤ p) (hq : 2 ≤ q)
1096 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1097 (htail : ∀ j, 2 ≤ tail j) :
1099 (secondReductionTransportSignature (p := p) hq
1100 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail) ≃
1103 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) where
1104 toFun
1105 | .elliptic i =>
1106 .elliptic
1108 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i)
1109 | .surfaceA j =>
1110 Fin.elim0 (by
1111 simpa [secondReductionTransportSignature, familyFuchsianSignature] using j)
1112 | .surfaceB j =>
1113 Fin.elim0 (by
1114 simpa [secondReductionTransportSignature, familyFuchsianSignature] using j)
1115 invFun
1116 | .elliptic i =>
1117 .elliptic
1119 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm i)
1120 | .surfaceA j =>
1121 Fin.elim0 (by
1122 simpa [secondReductionCanonicalOrderedTargetSignature] using j)
1123 | .surfaceB j =>
1124 Fin.elim0 (by
1125 simpa [secondReductionCanonicalOrderedTargetSignature] using j)
1126 left_inv := by
1127 intro x
1128 cases x with
1129 | elliptic i =>
1130 simp only
1131 congr
1132 exact Equiv.symm_apply_apply
1134 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) i
1135 | surfaceA j =>
1136 exact Fin.elim0 (by
1137 simpa [secondReductionTransportSignature, familyFuchsianSignature] using j)
1138 | surfaceB j =>
1139 exact Fin.elim0 (by
1140 simpa [secondReductionTransportSignature, familyFuchsianSignature] using j)
1141 right_inv := by
1142 intro x
1143 cases x with
1144 | elliptic i =>
1145 simp only
1146 congr
1147 exact Equiv.apply_symm_apply
1149 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) i
1150 | surfaceA j =>
1151 exact Fin.elim0 (by
1152 simpa [secondReductionCanonicalOrderedTargetSignature] using j)
1153 | surfaceB j =>
1154 exact Fin.elim0 (by
1155 simpa [secondReductionCanonicalOrderedTargetSignature] using j)
1157 {tailLen p q : ℕ}
1158 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1159 (hp : 2 ≤ p) (hq : 2 ≤ q)
1160 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1161 (htail : ∀ j, 2 ≤ tail j)
1162 (i : Fin
1163 (secondReductionTransportSignature (p := p) hq
1164 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail).numPeriods) :
1165 let τ :=
1166 secondReductionTransportSignature (p := p) hq
1167 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
1168 let υ :=
1170 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1171 τ.periods i =
1172 υ.periods
1174 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i) := by
1175 classical
1176 dsimp
1177 let τ :=
1178 secondReductionTransportSignature (p := p) hq
1179 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
1180 let υ :=
1182 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1183 let idx := (Fintype.equivFin (SecondReductionTransportIndex tailLen p q)).symm i
1184 have hi :
1185 (Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) idx = i :=
1186 Equiv.apply_symm_apply (Fintype.equivFin (SecondReductionTransportIndex tailLen p q)) i
1187 have hidx :
1189 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i =
1190 secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q idx := by
1191 rw [← hi]
1192 exact
1194 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail idx
1195 calc
1196 τ.periods i =
1197 secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail idx := by
1198 rw [← hi]
1199 simp only [secondReductionTransportSignature, familyFuchsianSignature_periods, τ]
1200 _ =
1201 υ.periods
1202 (secondReductionTransportIndexEquivCanonicalOrderedTargetFin tailLen p q idx) := by
1203 exact
1205 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail idx).symm
1206 _ =
1207 υ.periods
1209 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i) := by
1210 rw [hidx]
1212 {tailLen p q : ℕ}
1213 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1214 (hp : 2 ≤ p) (hq : 2 ≤ q)
1215 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1216 (htail : ∀ j, 2 ≤ tail j)
1217 (i : Fin
1218 (secondReductionTransportSignature (p := p) hq
1219 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail).numPeriods) :
1220 let τ :=
1221 secondReductionTransportSignature (p := p) hq
1222 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
1223 let υ :=
1225 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1226 FreeGroup.freeGroupCongr
1228 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1232 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i) := by
1233 classical
1235 FreeGroup.freeGroupCongr_apply, Equiv.coe_fn_mk, FreeGroup.map.of]
1237 {tailLen p q : ℕ}
1238 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1239 (hp : 2 ≤ p) (hq : 2 ≤ q)
1240 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1241 (htail : ∀ j, 2 ≤ tail j)
1242 (i : Fin
1244 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).numPeriods) :
1245 let τ :=
1246 secondReductionTransportSignature (p := p) hq
1247 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
1248 let υ :=
1250 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1251 (FreeGroup.freeGroupCongr
1253 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)).symm
1257 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm i) := by
1258 classical
1259 dsimp
1260 change FreeGroup.freeGroupCongr
1262 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm
1265 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) i) =
1267 (secondReductionTransportSignature (p := p) hq
1268 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)
1270 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm i)
1272 FreeGroup.freeGroupCongr_apply, Equiv.coe_fn_symm_mk, FreeGroup.map.of]
1273noncomputable def secondReductionCanonicalFirstPowerKernel
1274 {tailLen p q : ℕ}
1275 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1276 (hp : 2 ≤ p) (hq : 2 ≤ q)
1277 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1278 (htail : ∀ j, 2 ≤ tail j) :
1279 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1280 let φ :=
1282 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1283 φ.ker := by
1284 classical
1285 dsimp
1286 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1287 let σ :=
1289 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1290 let φ :=
1292 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1293 let x : FuchsianGenerator σ :=
1295 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1296 refine ⟨(FreeGroup.of x) ^ q, ?_⟩
1297 rw [MonoidHom.mem_ker, map_pow]
1298 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
1299 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
1300 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
1301 rw [hx]
1302 apply (Multiplicative.toAdd : Multiplicative (ZMod q) ≃ ZMod q).injective
1303 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]
1305 {tailLen p q : ℕ}
1306 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1307 (hp : 2 ≤ p) (hq : 2 ≤ q)
1308 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1309 (htail : ∀ j, 2 ≤ tail j) :
1310 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1311 let σ :=
1313 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1314 let φ :=
1316 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1317 let x : FuchsianGenerator σ :=
1319 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1321 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail :
1322 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1323 (FreeGroup.of x) ^ q := by
1324 classical
1325 dsimp
1326 simp only [secondReductionCanonicalFirstPowerKernel, Lean.Elab.WF.paramLet,
1329 {tailLen p q : ℕ}
1330 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1331 (hp : 2 ≤ p) (hq : 2 ≤ q)
1332 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1333 (htail : ∀ j, 2 ≤ tail j)
1334 {k : ℕ} (hk : k + 1 < q) :
1335 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1336 let σ :=
1338 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1339 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1340 let x :=
1342 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1343 let hT :=
1345 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1346 schreierGenerator hT ((FreeGroup.of x) ^ k) x = 1 := by
1347 classical
1348 dsimp
1349 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1350 let σ :=
1352 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1353 let φ :=
1355 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1356 let x : FuchsianGenerator σ :=
1358 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1359 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
1360 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
1361 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
1362 simpa [secondReductionCanonicalSchreierTransversal, φ, x] using
1365 {tailLen p q : ℕ}
1366 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1367 (hp : 2 ≤ p) (hq : 2 ≤ q)
1368 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1369 (htail : ∀ j, 2 ≤ tail j) :
1370 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1371 let σ :=
1373 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1374 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1375 let x :=
1377 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1378 let hT :=
1380 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1381 schreierGenerator hT ((FreeGroup.of x) ^ (q - 1)) x =
1383 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
1384 classical
1385 dsimp
1386 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1387 let σ :=
1389 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1390 let φ :=
1392 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1393 let x : FuchsianGenerator σ :=
1395 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1396 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
1397 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
1398 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
1400 secondReductionCanonicalFirstPowerKernel, φ, x] using
1403 {tailLen p q : ℕ}
1404 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1405 (hp : 2 ≤ p) (hq : 2 ≤ q)
1406 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1407 (htail : ∀ j, 2 ≤ tail j) :
1408 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1409 let σ :=
1411 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1412 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1413 let φ :=
1415 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1416 let hT :=
1418 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1420 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail : φ.ker) ∈
1421 schreierGeneratorSet hT := by
1422 classical
1423 dsimp
1424 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1425 let σ :=
1427 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1428 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1429 let φ :=
1431 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1432 let x : FuchsianGenerator σ :=
1434 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1435 let T :=
1437 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1438 let hT :=
1440 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1441 refine ⟨(FreeGroup.of x) ^ (q - 1), ?_, x, ?_, ?_⟩
1442 · have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
1443 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
1444 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
1445 simpa [T, secondReductionCanonicalSchreierTransversal, φ, x] using
1447 φ x hx (m := q - 1) (by omega)
1448 · simpa [hT, σ, φ, x, secondReductionCanonicalDistinguishedGenerator] using
1450 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail).symm
1451 · intro h
1452 have hval := congrArg
1453 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) h
1454 have hpow : (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ q = 1 := by
1455 simpa [σ, φ, x, secondReductionCanonicalDistinguishedGenerator,
1457 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail] using hval
1458 exact freeGroup_of_pow_ne_one x (by omega) hpow
1459noncomputable def secondReductionCanonicalZeroImageKernelElement
1460 {tailLen p q : ℕ}
1461 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1462 (hp : 2 ≤ p) (hq : 2 ≤ q)
1463 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1464 (htail : ∀ j, 2 ≤ tail j)
1465 (y :
1468 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
1469 (hy :
1471 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1472 (FreeGroup.of y) = 1)
1473 (k : Fin q) :
1474 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1475 let φ :=
1477 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1478 φ.ker := by
1479 classical
1480 dsimp
1481 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1482 let σ :=
1484 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1485 let φ :=
1487 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1488 let x : FuchsianGenerator σ :=
1490 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1491 refine
1492 ⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y *
1493 ((FreeGroup.of x) ^ k.val)⁻¹, ?_⟩
1494 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
1495 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
1496 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
1497 rw [MonoidHom.mem_ker]
1499private theorem secondReductionCanonicalZeroImageKernelElement_coe
1500 {tailLen p q : ℕ}
1501 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1502 (hp : 2 ≤ p) (hq : 2 ≤ q)
1503 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1504 (htail : ∀ j, 2 ≤ tail j)
1505 (y :
1508 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
1509 (hy :
1511 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1512 (FreeGroup.of y) = 1)
1513 (k : Fin q) :
1514 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1515 let σ :=
1517 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1518 let φ :=
1520 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1521 let x : FuchsianGenerator σ :=
1523 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1525 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k :
1526 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1527 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1528 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1529 classical
1530 dsimp
1531 simp only [secondReductionCanonicalZeroImageKernelElement, Lean.Elab.WF.paramLet,
1533noncomputable def secondReductionCanonicalHeadZeroKernelElement
1534 {tailLen p q : ℕ}
1535 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1536 (hp : 2 ≤ p) (hq : 2 ≤ q)
1537 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1538 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
1539 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1540 let φ :=
1542 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1543 φ.ker := by
1544 classical
1545 dsimp
1546 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1547 let σ :=
1549 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1550 let φ :=
1552 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1553 let y : FuchsianGenerator σ :=
1554 FuchsianGenerator.elliptic
1556 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1557 have hy : φ (FreeGroup.of y) = 1 := by
1558 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1559 secondReductionCanonicalSourceZeroIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1560 secondReductionCanonicalSourceQuotientImage, OfNat.zero_ne_ofNat, ↓reduceIte, φ, y]
1561 exact
1563 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1564noncomputable def secondReductionCanonicalHeadOneKernelElement
1565 {tailLen p q : ℕ}
1566 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1567 (hp : 2 ≤ p) (hq : 2 ≤ q)
1568 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1569 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
1570 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1571 let φ :=
1573 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1574 φ.ker := by
1575 classical
1576 dsimp
1577 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1578 let σ :=
1580 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1581 let φ :=
1583 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1584 let y : FuchsianGenerator σ :=
1585 FuchsianGenerator.elliptic
1587 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1588 have hy : φ (FreeGroup.of y) = 1 := by
1589 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1590 secondReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1591 secondReductionCanonicalSourceQuotientImage, OfNat.one_ne_ofNat, ↓reduceIte, φ, y]
1592 exact
1594 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1595noncomputable def secondReductionCanonicalMiddleRestZeroKernelElement
1596 {tailLen p q : ℕ}
1597 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1598 (hp : 2 ≤ p) (hq : 2 ≤ q)
1599 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1600 (htail : ∀ j, 2 ≤ tail j) (r : Fin (p - 2)) (k : Fin q) :
1601 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1602 let φ :=
1604 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1605 φ.ker := by
1606 classical
1607 dsimp
1608 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1609 let σ :=
1611 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1612 let φ :=
1614 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1615 let y : FuchsianGenerator σ :=
1616 FuchsianGenerator.elliptic
1618 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r.val, by omega⟩)
1619 have hy : φ (FreeGroup.of y) = 1 := by
1620 have hnot3 : ¬ 2 + (2 + r.val) = 3 := by omega
1621 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1622 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1623 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,
1624 ↓reduceIte, hnot3, φ, y]
1625 exact
1627 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1628noncomputable def secondReductionCanonicalTailZeroKernelElement
1629 {tailLen p q : ℕ}
1630 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1631 (hp : 2 ≤ p) (hq : 2 ≤ q)
1632 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1633 (htail : ∀ j, 2 ≤ tail j) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
1634 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1635 let φ :=
1637 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1638 φ.ker := by
1639 classical
1640 dsimp
1641 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1642 let σ :=
1644 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1645 let φ :=
1647 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1648 let y : FuchsianGenerator σ :=
1649 FuchsianGenerator.elliptic
1651 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j)
1652 have hy : φ (FreeGroup.of y) = 1 := by
1653 have hnot2 : ¬ 2 + p + b.val * tailLen + j.val = 2 := by omega
1654 have hnot3 : ¬ 2 + p + b.val * tailLen + j.val = 3 := by omega
1655 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1656 secondReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1657 secondReductionCanonicalSourceQuotientImage, hnot2, ↓reduceIte, hnot3, φ, y]
1658 exact
1660 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1662 {tailLen p q : ℕ}
1663 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1664 (hp : 2 ≤ p) (hq : 2 ≤ q)
1665 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1666 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
1667 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1668 let σ :=
1670 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1671 let φ :=
1673 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1674 let x : FuchsianGenerator σ :=
1676 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1677 let y : FuchsianGenerator σ :=
1678 FuchsianGenerator.elliptic
1680 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1682 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k : φ.ker) :
1683 FreeGroup (FuchsianGenerator σ)) =
1684 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1685 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1686 classical
1687 dsimp
1688 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1689 let σ :=
1691 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1692 let φ :=
1694 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1695 let x : FuchsianGenerator σ :=
1697 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1698 let y : FuchsianGenerator σ :=
1699 FuchsianGenerator.elliptic
1701 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1702 have hy : φ (FreeGroup.of y) = 1 := by
1703 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1704 secondReductionCanonicalSourceZeroIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1705 secondReductionCanonicalSourceQuotientImage, OfNat.zero_ne_ofNat, ↓reduceIte, φ, y]
1706 simpa [σ, φ, x, y, secondReductionCanonicalHeadZeroKernelElement] using
1708 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1710 {tailLen p q : ℕ}
1711 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1712 (hp : 2 ≤ p) (hq : 2 ≤ q)
1713 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1714 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
1715 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1716 let σ :=
1718 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1719 let φ :=
1721 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1722 let x : FuchsianGenerator σ :=
1724 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1725 let y : FuchsianGenerator σ :=
1726 FuchsianGenerator.elliptic
1728 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1730 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k : φ.ker) :
1731 FreeGroup (FuchsianGenerator σ)) =
1732 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1733 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1734 classical
1735 dsimp
1736 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1737 let σ :=
1739 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1740 let φ :=
1742 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1743 let x : FuchsianGenerator σ :=
1745 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1746 let y : FuchsianGenerator σ :=
1747 FuchsianGenerator.elliptic
1749 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
1750 have hy : φ (FreeGroup.of y) = 1 := by
1751 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1752 secondReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1753 secondReductionCanonicalSourceQuotientImage, OfNat.one_ne_ofNat, ↓reduceIte, φ, y]
1754 simpa [σ, φ, x, y, secondReductionCanonicalHeadOneKernelElement] using
1756 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1758 {tailLen p q : ℕ}
1759 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1760 (hp : 2 ≤ p) (hq : 2 ≤ q)
1761 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1762 (htail : ∀ j, 2 ≤ tail j) (r : Fin (p - 2)) (k : Fin q) :
1763 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1764 let σ :=
1766 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1767 let φ :=
1769 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1770 let x : FuchsianGenerator σ :=
1772 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1773 let y : FuchsianGenerator σ :=
1774 FuchsianGenerator.elliptic
1776 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r.val, by omega⟩)
1778 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k : φ.ker) :
1779 FreeGroup (FuchsianGenerator σ)) =
1780 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1781 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1782 classical
1783 dsimp
1784 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1785 let σ :=
1787 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1788 let φ :=
1790 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1791 let x : FuchsianGenerator σ :=
1793 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1794 let y : FuchsianGenerator σ :=
1795 FuchsianGenerator.elliptic
1797 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r.val, by omega⟩)
1798 have hy : φ (FreeGroup.of y) = 1 := by
1799 have hnot3 : ¬ 2 + (2 + r.val) = 3 := by omega
1800 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1801 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1802 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,
1803 ↓reduceIte, hnot3, φ, y]
1804 simpa [σ, φ, x, y, secondReductionCanonicalMiddleRestZeroKernelElement] using
1806 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1808 {tailLen p q : ℕ}
1809 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1810 (hp : 2 ≤ p) (hq : 2 ≤ q)
1811 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1812 (htail : ∀ j, 2 ≤ tail j) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
1813 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1814 let σ :=
1816 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1817 let φ :=
1819 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1820 let x : FuchsianGenerator σ :=
1822 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1823 let y : FuchsianGenerator σ :=
1824 FuchsianGenerator.elliptic
1826 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j)
1828 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k : φ.ker) :
1829 FreeGroup (FuchsianGenerator σ)) =
1830 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1831 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1832 classical
1833 dsimp
1834 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1835 let σ :=
1837 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1838 let φ :=
1840 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1841 let x : FuchsianGenerator σ :=
1843 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1844 let y : FuchsianGenerator σ :=
1845 FuchsianGenerator.elliptic
1847 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j)
1848 have hy : φ (FreeGroup.of y) = 1 := by
1849 have hnot2 : ¬ 2 + p + b.val * tailLen + j.val = 2 := by omega
1850 have hnot3 : ¬ 2 + p + b.val * tailLen + j.val = 3 := by omega
1851 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
1852 secondReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1853 secondReductionCanonicalSourceQuotientImage, hnot2, ↓reduceIte, hnot3, φ, y]
1854 simpa [σ, φ, x, y, secondReductionCanonicalTailZeroKernelElement] using
1856 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1858 {tailLen p q : ℕ}
1859 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1860 (hp : 2 ≤ p) (hq : 2 ≤ q)
1861 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1862 (htail : ∀ j, 2 ≤ tail j)
1863 (y :
1866 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
1867 (hy :
1869 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1870 (FreeGroup.of y) = 1)
1871 {k₁ k₂ : Fin q}
1872 (hxy :
1874 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y)
1875 (hEq :
1877 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k₁ =
1879 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k₂) :
1880 k₁ = k₂ := by
1881 classical
1882 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1883 let σ :=
1885 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1886 let φ :=
1888 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1889 let x : FuchsianGenerator σ :=
1891 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1892 have hval := congrArg
1893 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
1894 have hleft :
1896 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k₁ :
1897 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1898 (FreeGroup.of x) ^ k₁.val * FreeGroup.of y *
1899 ((FreeGroup.of x) ^ k₁.val)⁻¹ := by
1900 simpa [σ, φ, x] using
1902 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k₁
1903 have hright :
1905 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k₂ :
1906 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1907 (FreeGroup.of x) ^ k₂.val * FreeGroup.of y *
1908 ((FreeGroup.of x) ^ k₂.val)⁻¹ := by
1909 simpa [σ, φ, x] using
1911 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k₂
1912 have hword :
1913 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val * FreeGroup.of y *
1914 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹ =
1915 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val * FreeGroup.of y *
1916 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val)⁻¹ := by
1917 simpa [hleft, hright] using hval
1918 exact Fin.ext
1920 (by simpa [x] using hxy) hword)
1922 {tailLen p q : ℕ}
1923 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1924 (hp : 2 ≤ p) (hq : 2 ≤ q)
1925 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1926 (htail : ∀ j, 2 ≤ tail j)
1927 (y :
1930 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
1931 (hy :
1933 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1934 (FreeGroup.of y) = 1)
1935 (k : Fin q)
1936 (hxy :
1938 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y) :
1940 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k ≠
1942 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
1943 classical
1944 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
1945 let σ :=
1947 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1948 let φ :=
1950 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1951 let x : FuchsianGenerator σ :=
1953 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1954 intro hEq
1955 have hval := congrArg
1956 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
1957 have hleft :
1959 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k :
1960 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1961 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
1962 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1963 simpa [σ, φ, x] using
1965 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
1966 have hright :
1968 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail : φ.ker) :
1969 FreeGroup (FuchsianGenerator σ)) =
1970 (FreeGroup.of x) ^ q := by
1971 simpa [σ, φ, x] using
1973 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1974 have hword :
1975 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val * FreeGroup.of y *
1976 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
1977 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ q := by
1978 simpa [hleft, hright] using hval
1979 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
1980 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
1981 have hxne : x ≠ y := by
1982 simpa [x] using hxy
1983 have hmap := congrArg (FreeGroup.lift χ) hword
1984 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
1985 mul_one, ofAdd_eq_one, one_ne_zero, χ] at hmap
1986private theorem secondReductionCanonical_zeroImage_schreierGenerator_eq
1987 {tailLen p q : ℕ}
1988 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
1989 (hp : 2 ≤ p) (hq : 2 ≤ q)
1990 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
1991 (htail : ∀ j, 2 ≤ tail j)
1992 (y :
1995 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
1996 (hy :
1998 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
1999 (FreeGroup.of y) = 1)
2000 (k : Fin q) :
2001 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2002 let σ :=
2004 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2005 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2006 let x :=
2008 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2009 let hT :=
2011 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2012 schreierGenerator hT ((FreeGroup.of x) ^ k.val) y =
2014 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k := by
2015 classical
2016 dsimp
2017 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2018 let σ :=
2020 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2021 let φ :=
2023 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2024 let x : FuchsianGenerator σ :=
2026 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2027 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
2028 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
2029 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
2031 secondReductionCanonicalZeroImageKernelElement, φ, x] using
2032 cyclicQuotient_trivialImage_schreierGenerator_eq_conj φ x y hx hy k
2034 {tailLen p q : ℕ}
2035 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2036 (hp : 2 ≤ p) (hq : 2 ≤ q)
2037 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2038 (htail : ∀ j, 2 ≤ tail j)
2039 (y :
2042 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
2043 (hy :
2045 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2046 (FreeGroup.of y) = 1)
2047 (k : Fin q)
2048 (hxy :
2050 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y) :
2051 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2052 let σ :=
2054 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2055 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2056 let φ :=
2058 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2059 let hT :=
2061 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2063 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k : φ.ker) ∈
2064 schreierGeneratorSet hT := by
2065 classical
2066 dsimp
2067 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2068 let σ :=
2070 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2071 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2072 let φ :=
2074 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2075 let x : FuchsianGenerator σ :=
2077 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2078 let T :=
2080 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2081 let hT :=
2083 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2084 refine ⟨(FreeGroup.of x) ^ k.val, ?_, y, ?_, ?_⟩
2085 · have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
2086 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
2087 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
2088 simpa [T, secondReductionCanonicalSchreierTransversal, φ, x] using
2090 φ x hx (m := k.val) k.isLt
2091 · simpa [hT, σ, φ, x] using
2093 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k).symm
2094 · intro h
2095 have hval := congrArg
2096 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) h
2097 have hzeroWord :
2098 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
2099 FreeGroup.of y *
2100 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ = 1 := by
2101 simp only [secondReductionCanonicalZeroImageKernelElement_coe m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy
2102 k,
2103 OneMemClass.coe_one, conj_eq_one_iff, FreeGroup.of_ne_one, φ] at hval
2104 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
2105 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
2106 have hxne : x ≠ y := by
2107 simpa [x] using hxy
2108 have hmap := congrArg (FreeGroup.lift χ) hzeroWord
2109 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
2112 {tailLen p q : ℕ}
2113 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2114 (hp : 2 ≤ p) (hq : 2 ≤ q)
2115 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2116 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
2117 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2118 let σ :=
2120 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2121 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2122 let φ :=
2124 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2125 let hT :=
2127 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2128 let y : FuchsianGenerator σ :=
2129 FuchsianGenerator.elliptic
2131 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
2132 let hy : φ (FreeGroup.of y) = 1 := by
2133 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2134 secondReductionCanonicalSourceZeroIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2135 secondReductionCanonicalSourceQuotientImage, OfNat.zero_ne_ofNat, ↓reduceIte, φ, y]
2137 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k : φ.ker) ∈
2138 schreierGeneratorSet hT := by
2139 classical
2140 dsimp
2141 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2142 let σ :=
2144 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2145 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2146 let φ :=
2148 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2149 let y : FuchsianGenerator σ :=
2150 FuchsianGenerator.elliptic
2152 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
2153 have hy : φ (FreeGroup.of y) = 1 := by
2154 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2155 secondReductionCanonicalSourceZeroIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2156 secondReductionCanonicalSourceQuotientImage, OfNat.zero_ne_ofNat, ↓reduceIte, φ, y]
2157 have hxy :
2159 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y := by
2160 intro hEq
2161 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
2162 add_zero, secondReductionCanonicalSourceZeroIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq,
2163 OfNat.ofNat_ne_zero, y] at hEq
2164 simpa [σ, φ, y, hy] using
2166 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k hxy
2168 {tailLen p q : ℕ}
2169 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2170 (hp : 2 ≤ p) (hq : 2 ≤ q)
2171 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2172 (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
2173 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2174 let σ :=
2176 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2177 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2178 let φ :=
2180 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2181 let hT :=
2183 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2184 let y : FuchsianGenerator σ :=
2185 FuchsianGenerator.elliptic
2187 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
2188 let hy : φ (FreeGroup.of y) = 1 := by
2189 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2190 secondReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2191 secondReductionCanonicalSourceQuotientImage, OfNat.one_ne_ofNat, ↓reduceIte, φ, y]
2193 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k : φ.ker) ∈
2194 schreierGeneratorSet hT := by
2195 classical
2196 dsimp
2197 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2198 let σ :=
2200 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2201 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2202 let φ :=
2204 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2205 let y : FuchsianGenerator σ :=
2206 FuchsianGenerator.elliptic
2208 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
2209 have hy : φ (FreeGroup.of y) = 1 := by
2210 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2211 secondReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2212 secondReductionCanonicalSourceQuotientImage, OfNat.one_ne_ofNat, ↓reduceIte, φ, y]
2213 have hxy :
2215 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y := by
2216 intro hEq
2217 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
2218 add_zero, secondReductionCanonicalSourceOneIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq,
2219 OfNat.ofNat_ne_one, y] at hEq
2220 simpa [σ, φ, y, hy] using
2222 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k hxy
2224 {tailLen p q : ℕ}
2225 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2226 (hp : 2 ≤ p) (hq : 2 ≤ q)
2227 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2228 (htail : ∀ j, 2 ≤ tail j) (r : Fin (p - 2)) (k : Fin q) :
2229 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2230 let σ :=
2232 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2233 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2234 let φ :=
2236 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2237 let hT :=
2239 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2240 let y : FuchsianGenerator σ :=
2241 FuchsianGenerator.elliptic
2243 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r.val, by omega⟩)
2244 let hy : φ (FreeGroup.of y) = 1 := by
2245 have hnot3 : ¬ 2 + (2 + r.val) = 3 := by omega
2246 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2247 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2248 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,
2249 ↓reduceIte, hnot3, φ, y]
2251 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k : φ.ker) ∈
2252 schreierGeneratorSet hT := by
2253 classical
2254 dsimp
2255 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2256 let σ :=
2258 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2259 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2260 let φ :=
2262 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2263 let y : FuchsianGenerator σ :=
2264 FuchsianGenerator.elliptic
2266 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r.val, by omega⟩)
2267 have hy : φ (FreeGroup.of y) = 1 := by
2268 have hnot3 : ¬ 2 + (2 + r.val) = 3 := by omega
2269 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2270 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2271 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,
2272 ↓reduceIte, hnot3, φ, y]
2273 have hxy :
2275 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y := by
2276 intro hEq
2277 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
2278 add_zero, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, Nat.left_eq_add, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero,
2279 false_and, y] at hEq
2280 simpa [σ, φ, y, hy] using
2282 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k hxy
2284 {tailLen p q : ℕ}
2285 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2286 (hp : 2 ≤ p) (hq : 2 ≤ q)
2287 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2288 (htail : ∀ j, 2 ≤ tail j) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
2289 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2290 let σ :=
2292 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2293 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2294 let φ :=
2296 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2297 let hT :=
2299 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2300 let y : FuchsianGenerator σ :=
2301 FuchsianGenerator.elliptic
2303 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j)
2304 let hy : φ (FreeGroup.of y) = 1 := by
2305 have hnot2 : ¬ 2 + p + b.val * tailLen + j.val = 2 := by omega
2306 have hnot3 : ¬ 2 + p + b.val * tailLen + j.val = 3 := by omega
2307 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2308 secondReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2309 secondReductionCanonicalSourceQuotientImage, hnot2, ↓reduceIte, hnot3, φ, y]
2311 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k : φ.ker) ∈
2312 schreierGeneratorSet hT := by
2313 classical
2314 dsimp
2315 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2316 let σ :=
2318 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2319 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2320 let φ :=
2322 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2323 let y : FuchsianGenerator σ :=
2324 FuchsianGenerator.elliptic
2326 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j)
2327 have hy : φ (FreeGroup.of y) = 1 := by
2328 have hnot2 : ¬ 2 + p + b.val * tailLen + j.val = 2 := by omega
2329 have hnot3 : ¬ 2 + p + b.val * tailLen + j.val = 3 := by omega
2330 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2331 secondReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2332 secondReductionCanonicalSourceQuotientImage, hnot2, ↓reduceIte, hnot3, φ, y]
2333 have hxy :
2335 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y := by
2336 intro hEq
2337 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
2338 add_zero, secondReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, y] at hEq
2339 omega
2340 simpa [σ, φ, y, hy] using
2342 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k hxy
2343noncomputable def secondReductionCanonicalSecondPowerKernel
2344 {tailLen p q : ℕ}
2345 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2346 (hp : 2 ≤ p) (hq : 2 ≤ q)
2347 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2348 (htail : ∀ j, 2 ≤ tail j) :
2349 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2350 let φ :=
2352 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2353 φ.ker := by
2354 classical
2355 dsimp
2356 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2357 let σ :=
2359 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2360 let φ :=
2362 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2363 let y : FuchsianGenerator σ :=
2364 FuchsianGenerator.elliptic
2366 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2367 refine ⟨(FreeGroup.of y) ^ q, ?_⟩
2368 rw [MonoidHom.mem_ker, map_pow]
2369 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod q) := by
2370 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2371 secondReductionCanonicalSourceMiddleIndex, Nat.reduceAdd, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2372 secondReductionCanonicalSourceQuotientImage, Nat.succ_ne_self, ↓reduceIte, ofAdd_neg, φ, y]
2373 rw [hy]
2374 apply (Multiplicative.toAdd : Multiplicative (ZMod q) ≃ ZMod q).injective
2375 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
2376 neg_zero, toAdd_one]
2378 {tailLen p q : ℕ}
2379 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2380 (hp : 2 ≤ p) (hq : 2 ≤ q)
2381 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2382 (htail : ∀ j, 2 ≤ tail j) :
2383 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2384 let σ :=
2386 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2387 let φ :=
2389 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2390 let y : FuchsianGenerator σ :=
2391 FuchsianGenerator.elliptic
2393 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2395 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail :
2396 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
2397 (FreeGroup.of y) ^ q := by
2398 classical
2399 dsimp
2400 simp only [secondReductionCanonicalSecondPowerKernel, Lean.Elab.WF.paramLet, id_eq]
2401noncomputable def secondReductionCanonicalSecondEdgeKernelElement
2402 {tailLen p q : ℕ}
2403 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2404 (hp : 2 ≤ p) (hq : 2 ≤ q)
2405 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2406 (htail : ∀ j, 2 ≤ tail j)
2407 (k : Fin q) :
2408 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2409 let φ :=
2411 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2412 φ.ker := by
2413 classical
2414 dsimp
2415 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2416 let σ :=
2418 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2419 let φ :=
2421 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2422 let x : FuchsianGenerator σ :=
2424 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2425 let y : FuchsianGenerator σ :=
2426 FuchsianGenerator.elliptic
2428 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2429 let r : ℕ := ((k.val : ZMod q) - 1).val
2430 refine ⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y * ((FreeGroup.of x) ^ r)⁻¹, ?_⟩
2431 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
2432 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
2433 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
2434 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod q) := by
2435 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2436 secondReductionCanonicalSourceMiddleIndex, Nat.reduceAdd, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2437 secondReductionCanonicalSourceQuotientImage, Nat.succ_ne_self, ↓reduceIte, ofAdd_neg, φ, y]
2438 rw [MonoidHom.mem_ker]
2440 apply (Multiplicative.toAdd : Multiplicative (ZMod q) ≃ ZMod q).injective
2441 simp only [ofAdd_neg, toAdd_mul, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one, toAdd_inv, ZMod.natCast_val,
2442 dvd_refl, ZMod.cast_sub, ZMod.cast_natCast, ZMod.cast_one, neg_sub, toAdd_one, r]
2443 ring
2445 {tailLen p q : ℕ}
2446 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2447 (hp : 2 ≤ p) (hq : 2 ≤ q)
2448 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2449 (htail : ∀ j, 2 ≤ tail j) :
2450 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2451 let σ :=
2453 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2454 let φ :=
2456 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2457 let x : FuchsianGenerator σ :=
2459 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2460 let y : FuchsianGenerator σ :=
2461 FuchsianGenerator.elliptic
2463 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2465 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2466 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩ :
2467 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
2468 FreeGroup.of y * ((FreeGroup.of x) ^ (q - 1))⁻¹ := by
2469 classical
2470 dsimp
2471 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2472 let σ :=
2474 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2475 let φ :=
2477 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2478 let x : FuchsianGenerator σ :=
2480 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2481 let y : FuchsianGenerator σ :=
2482 FuchsianGenerator.elliptic
2484 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2485 have hq_pos : 0 < q := lt_of_lt_of_le (by decide : 0 < 2) hq
2486 have hsucc : (q - 1).succ = q := by omega
2487 have hval : (-1 : ZMod q).val = q - 1 := by
2488 rw [← hsucc]
2489 exact ZMod.val_neg_one (q - 1)
2490 simp only [secondReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
2491 secondReductionCanonicalDistinguishedGenerator, pow_zero, one_mul, Nat.cast_zero, zero_sub, hval, id_eq]
2493 {tailLen p q : ℕ}
2494 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2495 (hp : 2 ≤ p) (hq : 2 ≤ q)
2496 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2497 (htail : ∀ j, 2 ≤ tail j)
2498 (i : Fin (q - 1)) :
2499 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2500 let σ :=
2502 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2503 let φ :=
2505 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2506 let x : FuchsianGenerator σ :=
2508 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2509 let y : FuchsianGenerator σ :=
2510 FuchsianGenerator.elliptic
2512 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2514 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2515 ⟨q - 1 - i.val, by omega⟩ :
2516 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
2517 (FreeGroup.of x) ^ (q - 1 - i.val) * FreeGroup.of y *
2518 ((FreeGroup.of x) ^ (q - 1 - 1 - i.val))⁻¹ := by
2519 classical
2520 dsimp
2521 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2522 let σ :=
2524 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2525 let φ :=
2527 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2528 let x : FuchsianGenerator σ :=
2530 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2531 let y : FuchsianGenerator σ :=
2532 FuchsianGenerator.elliptic
2534 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2535 let kNat := q - 1 - i.val
2536 have hq_gt_one : 1 < q := lt_of_lt_of_le (by decide : 1 < 2) hq
2537 haveI : Fact (1 < q) := ⟨hq_gt_one⟩
2538 have hkpos : 0 < kNat := by
2539 dsimp [kNat]
2540 omega
2541 have hklt : kNat < q := by
2542 dsimp [kNat]
2543 omega
2544 have hkval : ((kNat : ZMod q)).val = kNat :=
2545 ZMod.val_natCast_of_lt hklt
2546 have hsubval : ((kNat : ZMod q) - 1).val = kNat - 1 := by
2547 have hle : (1 : ZMod q).val ≤ (kNat : ZMod q).val := by
2548 rw [hkval, ZMod.val_one]
2549 exact Nat.succ_le_iff.mpr hkpos
2550 rw [ZMod.val_sub hle, hkval, ZMod.val_one]
2551 have hkSub : kNat - 1 = q - 1 - 1 - i.val := by
2552 dsimp [kNat]
2553 omega
2554 have hsubval' :
2555 (((q - 1 - i.val : ℕ) : ZMod q) - 1).val =
2556 q - 1 - 1 - i.val := by
2557 simpa [kNat, hkSub] using hsubval
2560 rw [hsubval']
2562 {tailLen p q : ℕ}
2563 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2564 (hp : 2 ≤ p) (hq : 2 ≤ q)
2565 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2566 (htail : ∀ j, 2 ≤ tail j)
2567 (i : Fin (q - 1)) :
2568 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2569 let σ :=
2571 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2572 let φ :=
2574 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2575 let x : FuchsianGenerator σ :=
2577 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2578 let y : FuchsianGenerator σ :=
2579 FuchsianGenerator.elliptic
2581 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2583 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2584 ⟨i.val + 1, by omega⟩ :
2585 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
2586 (FreeGroup.of x) ^ (i.val + 1) * FreeGroup.of y *
2587 ((FreeGroup.of x) ^ i.val)⁻¹ := by
2588 classical
2589 dsimp
2590 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2591 let σ :=
2593 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2594 let φ :=
2596 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2597 let x : FuchsianGenerator σ :=
2599 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2600 let y : FuchsianGenerator σ :=
2601 FuchsianGenerator.elliptic
2603 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2604 let kNat := i.val + 1
2605 have hq_gt_one : 1 < q := lt_of_lt_of_le (by decide : 1 < 2) hq
2606 haveI : Fact (1 < q) := ⟨hq_gt_one⟩
2607 have hkpos : 0 < kNat := by
2608 dsimp [kNat]
2609 omega
2610 have hklt : kNat < q := by
2611 dsimp [kNat]
2612 omega
2613 have hkval : ((kNat : ZMod q)).val = kNat :=
2614 ZMod.val_natCast_of_lt hklt
2615 have hsubval : ((kNat : ZMod q) - 1).val = kNat - 1 := by
2616 have hle : (1 : ZMod q).val ≤ (kNat : ZMod q).val := by
2617 rw [hkval, ZMod.val_one]
2618 exact Nat.succ_le_iff.mpr hkpos
2619 rw [ZMod.val_sub hle, hkval, ZMod.val_one]
2620 have hkSub : kNat - 1 = i.val := by
2621 omega
2622 have hsubval' :
2623 (((i.val + 1 : ℕ) : ZMod q) - 1).val = i.val := by
2624 simpa [kNat, hkSub] using hsubval
2627 rw [hsubval']
2628private theorem secondReductionCanonical_second_schreierGenerator_eq
2629 {tailLen p q : ℕ}
2630 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2631 (hp : 2 ≤ p) (hq : 2 ≤ q)
2632 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2633 (htail : ∀ j, 2 ≤ tail j)
2634 (k : Fin q) :
2635 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2636 let σ :=
2638 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2639 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2640 let x :=
2642 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2643 let y : FuchsianGenerator σ :=
2644 FuchsianGenerator.elliptic
2646 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2647 let hT :=
2649 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2650 schreierGenerator hT ((FreeGroup.of x) ^ k.val) y =
2652 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k := by
2653 classical
2654 dsimp
2655 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2656 let σ :=
2658 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2659 let φ :=
2661 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2662 let x : FuchsianGenerator σ :=
2664 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2665 let y : FuchsianGenerator σ :=
2666 FuchsianGenerator.elliptic
2668 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2669 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
2670 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
2671 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
2672 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod q) := by
2673 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2674 secondReductionCanonicalSourceMiddleIndex, Nat.reduceAdd, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2675 secondReductionCanonicalSourceQuotientImage, Nat.succ_ne_self, ↓reduceIte, ofAdd_neg, φ, y]
2677 secondReductionCanonicalSecondEdgeKernelElement, φ, x, y] using
2678 cyclicQuotient_negOneImage_schreierGenerator_eq φ x y hx hy k
2680 {tailLen p q : ℕ}
2681 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2682 (hp : 2 ≤ p) (hq : 2 ≤ q)
2683 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2684 (htail : ∀ j, 2 ≤ tail j)
2685 (k : Fin q) :
2686 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2687 let σ :=
2689 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2690 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2691 let φ :=
2693 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2694 let hT :=
2696 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2698 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k : φ.ker) ∈
2699 schreierGeneratorSet hT := by
2700 classical
2701 dsimp
2702 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2703 let σ :=
2705 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2706 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
2707 let φ :=
2709 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2710 let x : FuchsianGenerator σ :=
2712 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2713 let y : FuchsianGenerator σ :=
2714 FuchsianGenerator.elliptic
2716 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2717 let T :=
2719 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2720 let hT :=
2722 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2723 refine ⟨(FreeGroup.of x) ^ k.val, ?_, y, ?_, ?_⟩
2724 · have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
2725 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
2726 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
2727 simpa [T, secondReductionCanonicalSchreierTransversal, φ, x] using
2729 φ x hx (m := k.val) k.isLt
2730 · simpa [hT, σ, φ, x, y, secondReductionCanonicalDistinguishedGenerator] using
2732 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k).symm
2733 · intro h
2734 have hval := congrArg
2735 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) h
2736 let r : ℕ := ((k.val : ZMod q) - 1).val
2737 have hsecondWord :
2738 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
2739 FreeGroup.of y *
2740 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r)⁻¹ = 1 := by
2741 simpa [φ, x, y, r, secondReductionCanonicalSecondEdgeKernelElement,
2742 secondReductionCanonicalDistinguishedGenerator] using hval
2743 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
2744 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
2745 have hxne : x ≠ y := by
2746 intro hEq
2747 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
2748 add_zero, Nat.reduceAdd, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, Nat.reduceEqDiff, x, y] at hEq
2749 have hmap := congrArg (FreeGroup.lift χ) hsecondWord
2750 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
2753 {tailLen p q : ℕ}
2754 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2755 (hp : 2 ≤ p) (hq : 2 ≤ q)
2756 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2757 (htail : ∀ j, 2 ≤ tail j)
2758 {k₁ k₂ : Fin q}
2759 (hEq :
2761 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k₁ =
2763 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k₂) :
2764 k₁ = k₂ := by
2765 classical
2766 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2767 let σ :=
2769 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2770 let φ :=
2772 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2773 let x : FuchsianGenerator σ :=
2775 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2776 let y : FuchsianGenerator σ :=
2777 FuchsianGenerator.elliptic
2779 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2780 have hval := congrArg
2781 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
2782 let r₁ : ℕ := ((k₁.val : ZMod q) - 1).val
2783 let r₂ : ℕ := ((k₂.val : ZMod q) - 1).val
2784 have hleft :
2786 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k₁ : φ.ker) :
2787 FreeGroup (FuchsianGenerator σ)) =
2788 (FreeGroup.of x) ^ k₁.val * FreeGroup.of y *
2789 ((FreeGroup.of x) ^ r₁)⁻¹ := by
2790 simp only [secondReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
2791 secondReductionCanonicalDistinguishedGenerator, id_eq, σ, x, y, r₁]
2792 have hright :
2794 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k₂ : φ.ker) :
2795 FreeGroup (FuchsianGenerator σ)) =
2796 (FreeGroup.of x) ^ k₂.val * FreeGroup.of y *
2797 ((FreeGroup.of x) ^ r₂)⁻¹ := by
2798 simp only [secondReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
2799 secondReductionCanonicalDistinguishedGenerator, id_eq, σ, x, y, r₂]
2800 have hword :
2801 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val * FreeGroup.of y *
2802 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r₁)⁻¹ =
2803 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val * FreeGroup.of y *
2804 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r₂)⁻¹ := by
2805 simpa [hleft, hright] using hval
2806 have hxne : x ≠ y := by
2807 intro hEq'
2808 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
2809 add_zero, Nat.reduceAdd, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, Nat.reduceEqDiff, x, y] at hEq'
2810 exact Fin.ext
2813 {tailLen p q : ℕ}
2814 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2815 (hp : 2 ≤ p) (hq : 2 ≤ q)
2816 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2817 (htail : ∀ j, 2 ≤ tail j)
2818 (y :
2821 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
2822 (hy :
2824 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2825 (FreeGroup.of y) = 1)
2826 (k k' : Fin q)
2827 (hxy :
2829 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y)
2830 (hyne :
2831 y ≠ FuchsianGenerator.elliptic
2833 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)) :
2835 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k ≠
2837 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k' := by
2838 classical
2839 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2840 let σ :=
2842 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2843 let φ :=
2845 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2846 let x : FuchsianGenerator σ :=
2848 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2849 let yNeg : FuchsianGenerator σ :=
2850 FuchsianGenerator.elliptic
2852 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
2853 intro hEq
2854 have hval := congrArg
2855 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
2856 have hleft :
2858 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k :
2859 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
2860 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
2861 ((FreeGroup.of x) ^ k.val)⁻¹ := by
2862 simpa [σ, φ, x] using
2864 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
2865 let r : ℕ := ((k'.val : ZMod q) - 1).val
2866 have hright :
2868 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k' : φ.ker) :
2869 FreeGroup (FuchsianGenerator σ)) =
2870 (FreeGroup.of x) ^ k'.val * FreeGroup.of yNeg *
2871 ((FreeGroup.of x) ^ r)⁻¹ := by
2872 simp only [secondReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
2873 secondReductionCanonicalDistinguishedGenerator, id_eq, σ, x, yNeg, r]
2874 have hword :
2875 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val * FreeGroup.of y *
2876 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
2877 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k'.val * FreeGroup.of yNeg *
2878 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r)⁻¹ := by
2879 simpa [hleft, hright] using hval
2880 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
2881 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
2882 have hxne : x ≠ y := by
2883 simpa [x] using hxy
2884 have hyne' : yNeg ≠ y := by
2885 simpa [yNeg] using hyne.symm
2886 have hmap := congrArg (FreeGroup.lift χ) hword
2887 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
2888 mul_one, hyne', ofAdd_eq_one, one_ne_zero, χ] at hmap
2890 {tailLen p q : ℕ}
2891 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2892 (hp : 2 ≤ p) (hq : 2 ≤ q)
2893 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2894 (htail : ∀ j, 2 ≤ tail j)
2895 (y y' :
2898 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
2899 (hy :
2901 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2902 (FreeGroup.of y) = 1)
2903 (hy' :
2905 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2906 (FreeGroup.of y') = 1)
2907 (k k' : Fin q)
2908 (hxy :
2910 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ≠ y)
2911 (hyne : y' ≠ y) :
2913 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k ≠
2915 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y' hy' k' := by
2916 classical
2917 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2918 let σ :=
2920 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2921 let φ :=
2923 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2924 let x : FuchsianGenerator σ :=
2926 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2927 intro hEq
2928 have hval := congrArg
2929 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
2930 have hleft :
2932 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k :
2933 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
2934 (FreeGroup.of x) ^ k.val * FreeGroup.of y *
2935 ((FreeGroup.of x) ^ k.val)⁻¹ := by
2936 simpa [σ, φ, x] using
2938 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
2939 have hright :
2941 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y' hy' k' :
2942 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
2943 (FreeGroup.of x) ^ k'.val * FreeGroup.of y' *
2944 ((FreeGroup.of x) ^ k'.val)⁻¹ := by
2945 simpa [σ, φ, x] using
2947 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y' hy' k'
2948 have hword :
2949 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val * FreeGroup.of y *
2950 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =
2951 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k'.val * FreeGroup.of y' *
2952 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k'.val)⁻¹ := by
2953 simpa [hleft, hright] using hval
2954 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
2955 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
2956 have hxne : x ≠ y := by
2957 simpa [x] using hxy
2958 have hmap := congrArg (FreeGroup.lift χ) hword
2959 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
2960 mul_one, hyne, ofAdd_eq_one, one_ne_zero, χ] at hmap
2962 {tailLen p q : ℕ}
2963 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
2964 (hp : 2 ≤ p) (hq : 2 ≤ q)
2965 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
2966 (htail : ∀ j, 2 ≤ tail j)
2967 {r₁ r₂ : Fin (p - 2)} {k₁ k₂ : Fin q}
2968 (hEq :
2970 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r₁ k₁ =
2972 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r₂ k₂) :
2973 r₁ = r₂ ∧ k₁ = k₂ := by
2974 classical
2975 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
2976 let σ :=
2978 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2979 let φ :=
2981 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2982 let x : FuchsianGenerator σ :=
2984 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
2985 let y₁ : FuchsianGenerator σ :=
2986 FuchsianGenerator.elliptic
2988 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r₁.val, by omega⟩)
2989 let y₂ : FuchsianGenerator σ :=
2990 FuchsianGenerator.elliptic
2992 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r₂.val, by omega⟩)
2993 have hy₁ : φ (FreeGroup.of y₁) = 1 := by
2994 have hnot3 : ¬ 2 + (2 + r₁.val) = 3 := by omega
2995 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
2996 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
2997 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,
2998 ↓reduceIte, hnot3, φ, y₁]
2999 have hy₂ : φ (FreeGroup.of y₂) = 1 := by
3000 have hnot3 : ¬ 2 + (2 + r₂.val) = 3 := by omega
3001 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
3002 secondReductionCanonicalSourceMiddleIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
3003 secondReductionCanonicalSourceQuotientImage, Nat.add_eq_left, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and,
3004 ↓reduceIte, hnot3, φ, y₂]
3005 have hxy₁ : x ≠ y₁ := by
3006 intro hEq'
3007 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
3008 add_zero, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, Nat.left_eq_add, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero,
3009 false_and, x, y₁] at hEq'
3010 by_cases hgen : y₂ = y₁
3011 · have hr : r₁ = r₂ := by
3012 have hval := congrArg
3013 (fun y : FuchsianGenerator σ =>
3014 match y with
3015 | .elliptic i => i.val
3016 | .surfaceA _ => 0
3017 | .surfaceB _ => 0) hgen.symm
3018 simp only [secondReductionCanonicalSourceMiddleIndex, Nat.add_left_cancel_iff, y₂, y₁] at hval
3019 exact Fin.ext (by omega)
3020 subst r₂
3021 have hk : k₁ = k₂ := by
3022 exact
3024 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y₁ hy₁ hxy₁
3025 (by
3026 simpa [σ, φ, y₁, hy₁,
3028 exact ⟨rfl, hk⟩
3029 · exact False.elim
3031 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y₁ y₂ hy₁ hy₂ k₁ k₂
3032 hxy₁ hgen hEq)
3034 {tailLen p q : ℕ}
3035 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
3036 (hp : 2 ≤ p) (hq : 2 ≤ q)
3037 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
3038 (htail : ∀ j, 2 ≤ tail j)
3039 {b₁ b₂ : Fin p} {j₁ j₂ : Fin tailLen} {k₁ k₂ : Fin q}
3040 (hEq :
3042 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b₁ j₁ k₁ =
3044 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b₂ j₂ k₂) :
3045 b₁ = b₂ ∧ j₁ = j₂ ∧ k₁ = k₂ := by
3046 classical
3047 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3048 let σ :=
3050 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3051 let φ :=
3053 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3054 let x : FuchsianGenerator σ :=
3056 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3057 let tailGen : Fin p → Fin tailLen → FuchsianGenerator σ := fun b j =>
3058 FuchsianGenerator.elliptic
3060 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j)
3061 have hval := congrArg
3062 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
3063 have hleft :
3065 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b₁ j₁ k₁ :
3066 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
3067 (FreeGroup.of x) ^ k₁.val * FreeGroup.of (tailGen b₁ j₁) *
3068 ((FreeGroup.of x) ^ k₁.val)⁻¹ := by
3069 simp only [secondReductionCanonicalTailZeroKernelElement, Lean.Elab.WF.paramLet,
3070 secondReductionCanonicalZeroImageKernelElement, secondReductionCanonicalDistinguishedGenerator, id_eq, σ, x,
3071 tailGen]
3072 have hright :
3074 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b₂ j₂ k₂ :
3075 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
3076 (FreeGroup.of x) ^ k₂.val * FreeGroup.of (tailGen b₂ j₂) *
3077 ((FreeGroup.of x) ^ k₂.val)⁻¹ := by
3078 simp only [secondReductionCanonicalTailZeroKernelElement, Lean.Elab.WF.paramLet,
3079 secondReductionCanonicalZeroImageKernelElement, secondReductionCanonicalDistinguishedGenerator, id_eq, σ, x,
3080 tailGen]
3081 have hword :
3082 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
3083 FreeGroup.of (tailGen b₁ j₁) *
3084 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹ =
3085 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val *
3086 FreeGroup.of (tailGen b₂ j₂) *
3087 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val)⁻¹ := by
3088 simpa [hleft, hright] using hval
3089 have hxne₁ : x ≠ tailGen b₁ j₁ := by
3090 intro hEq'
3091 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
3092 add_zero, secondReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, x,
3093 tailGen] at hEq'
3094 omega
3095 have hxne₂ : x ≠ tailGen b₂ j₂ := by
3096 intro hEq'
3097 simp only [secondReductionCanonicalDistinguishedGenerator, secondReductionCanonicalSourceMiddleIndex,
3098 add_zero, secondReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, x,
3099 tailGen] at hEq'
3100 omega
3101 have hlen := congrArg
3102 (fun w : FreeGroup (FuchsianGenerator σ) => (FreeGroup.toWord w).length) hword
3103 change
3104 (FreeGroup.toWord
3105 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
3106 FreeGroup.of (tailGen b₁ j₁) *
3107 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹)).length =
3108 (FreeGroup.toWord
3109 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val *
3110 FreeGroup.of (tailGen b₂ j₂) *
3111 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val)⁻¹)).length at hlen
3112 rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₁ k₁.val k₁.val,
3113 freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₂ k₂.val k₂.val] at hlen
3114 simp only [List.append_assoc, List.cons_append, List.nil_append, List.length_append, List.length_replicate,
3115 List.length_cons] at hlen
3116 have hk : k₁ = k₂ := by
3117 ext
3118 omega
3119 subst k₂
3120 have hwords := congrArg
3121 (fun w : FreeGroup (FuchsianGenerator σ) => FreeGroup.toWord w) hword
3122 change
3123 FreeGroup.toWord
3124 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
3125 FreeGroup.of (tailGen b₁ j₁) *
3126 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹) =
3127 FreeGroup.toWord
3128 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
3129 FreeGroup.of (tailGen b₂ j₂) *
3130 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹) at hwords
3131 rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₁ k₁.val k₁.val,
3132 freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₂ k₁.val k₁.val] at hwords
3133 have hdrop := congrArg
3134 (fun L : List (FuchsianGenerator σ × Bool) => L.drop k₁.val) hwords
3135 have hhead := congrArg List.head? hdrop
3136 have htailGenEq : tailGen b₁ j₁ = tailGen b₂ j₂ := by
3137 simpa using hhead
3138 have hidxVal :
3139 2 + p + b₁.val * tailLen + j₁.val =
3140 2 + p + b₂.val * tailLen + j₂.val := by
3141 have h := congrArg
3142 (fun y : FuchsianGenerator σ =>
3143 match y with
3144 | .elliptic i => i.val
3145 | .surfaceA _ => 0
3146 | .surfaceB _ => 0) htailGenEq
3147 simpa [tailGen, secondReductionCanonicalSourceTailIndex] using h
3148 have hsum :
3149 b₁.val * tailLen + j₁.val = b₂.val * tailLen + j₂.val := by
3150 omega
3151 have htailLen_pos : 0 < tailLen := lt_of_le_of_lt (Nat.zero_le _) j₁.isLt
3152 have hdiv₁ : (b₁.val * tailLen + j₁.val) / tailLen = b₁.val := by
3153 rw [Nat.mul_comm b₁.val tailLen, Nat.mul_add_div htailLen_pos,
3154 Nat.div_eq_of_lt j₁.isLt]
3155 simp only [add_zero]
3156 have hdiv₂ : (b₂.val * tailLen + j₂.val) / tailLen = b₂.val := by
3157 rw [Nat.mul_comm b₂.val tailLen, Nat.mul_add_div htailLen_pos,
3158 Nat.div_eq_of_lt j₂.isLt]
3159 simp only [add_zero]
3160 have hbVal : b₁.val = b₂.val := by
3161 have hdiv := congrArg (fun n : ℕ => n / tailLen) hsum
3162 simpa [hdiv₁, hdiv₂] using hdiv
3163 have hmod₁ : (b₁.val * tailLen + j₁.val) % tailLen = j₁.val := by
3164 rw [Nat.mul_comm b₁.val tailLen, Nat.mul_add_mod_self_left,
3165 Nat.mod_eq_of_lt j₁.isLt]
3166 have hmod₂ : (b₂.val * tailLen + j₂.val) % tailLen = j₂.val := by
3167 rw [Nat.mul_comm b₂.val tailLen, Nat.mul_add_mod_self_left,
3168 Nat.mod_eq_of_lt j₂.isLt]
3169 have hjVal : j₁.val = j₂.val := by
3170 have hmod := congrArg (fun n : ℕ => n % tailLen) hsum
3171 simpa [hmod₁, hmod₂] using hmod
3172 exact ⟨Fin.ext hbVal, Fin.ext hjVal, rfl⟩
3174 {tailLen p q : ℕ}
3175 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
3176 (hp : 2 ≤ p) (hq : 2 ≤ q)
3177 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
3178 (htail : ∀ j, 2 ≤ tail j) :
3179 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3180 let n := q - 1
3182 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3183 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩ *
3184 (List.ofFn (fun i : Fin n =>
3186 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3187 ⟨n - i.val, by omega⟩)).prod =
3189 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
3190 classical
3191 dsimp
3192 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3193 let n := q - 1
3194 let σ :=
3196 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3197 let φ :=
3199 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3200 let x : FuchsianGenerator σ :=
3202 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3203 let y : FuchsianGenerator σ :=
3204 FuchsianGenerator.elliptic
3206 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
3207 apply Subtype.ext
3208 change
3210 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3211 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩ : φ.ker) :
3212 FreeGroup (FuchsianGenerator σ)) *
3213 (((List.ofFn (fun i : Fin n =>
3215 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3216 ⟨n - i.val, by omega⟩)).prod : φ.ker) :
3217 FreeGroup (FuchsianGenerator σ)) =
3219 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail : φ.ker) :
3220 FreeGroup (FuchsianGenerator σ))
3221 have hprodCoe :
3222 (((List.ofFn (fun i : Fin n =>
3224 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3225 ⟨n - i.val, by omega⟩)).prod : φ.ker) :
3226 FreeGroup (FuchsianGenerator σ)) =
3227 (List.ofFn (fun i : Fin n =>
3229 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3230 ⟨n - i.val, by omega⟩ : φ.ker) :
3231 FreeGroup (FuchsianGenerator σ)))).prod := by
3232 change
3233 φ.ker.subtype
3234 ((List.ofFn (fun i : Fin n =>
3236 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3237 ⟨n - i.val, by omega⟩)).prod) =
3238 (List.ofFn (fun i : Fin n =>
3239 φ.ker.subtype
3241 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3242 ⟨n - i.val, by omega⟩))).prod
3243 rw [map_list_prod, List.map_ofFn]
3244 rfl
3245 rw [hprodCoe]
3247 have htailList :
3248 (List.ofFn (fun i : Fin n =>
3250 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3251 ⟨n - i.val, by omega⟩ : φ.ker) :
3252 FreeGroup (FuchsianGenerator σ)))) =
3253 List.ofFn (fun i : Fin n =>
3254 (FreeGroup.of x) ^ (n - i.val) * FreeGroup.of y *
3255 ((FreeGroup.of x) ^ (n - 1 - i.val))⁻¹) := by
3256 apply List.ofFn_inj.2
3257 funext i
3258 simpa [n, σ, φ, x, y] using
3260 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i
3261 rw [htailList]
3262 change
3263 FreeGroup.of y * ((FreeGroup.of x) ^ n)⁻¹ *
3264 negOneCycleTailProduct (FreeGroup.of x) (FreeGroup.of y) n =
3265 (FreeGroup.of y) ^ q
3266 have hn : n + 1 = q := by
3267 dsimp [n]
3268 omega
3269 rw [← hn]
3270 exact negOneCycleProduct_eq_pow (FreeGroup.of x) (FreeGroup.of y) n
3272 {tailLen p q : ℕ}
3273 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
3274 (hp : 2 ≤ p) (hq : 2 ≤ q)
3275 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
3276 (htail : ∀ j, 2 ≤ tail j) :
3277 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3278 let n := q - 1
3279 let σ :=
3281 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3282 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3283 let e :=
3285 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3286 e.symm
3288 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3289 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩) *
3290 (List.ofFn (fun i : Fin n =>
3291 e.symm
3293 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3294 ⟨n - i.val, by omega⟩))).prod =
3295 e.symm
3297 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail) := by
3298 classical
3299 dsimp
3300 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3301 let n := q - 1
3302 let σ :=
3304 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3305 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3306 let e :=
3308 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3309 have hcycle :
3311 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3312 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩ *
3313 (List.ofFn (fun i : Fin n =>
3315 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3316 ⟨n - i.val, by omega⟩)).prod =
3318 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
3319 simpa [n] using
3321 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3322 have hmap := congrArg e.symm hcycle
3323 have htailMap :
3324 e.symm
3325 ((List.ofFn (fun i : Fin n =>
3327 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3328 ⟨n - i.val, by omega⟩)).prod) =
3329 (List.ofFn (fun i : Fin n =>
3330 e.symm
3332 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3333 ⟨n - i.val, by omega⟩))).prod := by
3334 rw [map_list_prod, List.map_ofFn]
3335 rfl
3338 {tailLen p q : ℕ}
3339 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
3340 (hp : 2 ≤ p) (hq : 2 ≤ q)
3341 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
3342 (htail : ∀ j, 2 ≤ tail j)
3343 (k : Fin q) :
3344 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3345 let σ :=
3347 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3348 let φ :=
3350 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3351 let x : FuchsianGenerator σ :=
3353 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3354 let y : FuchsianGenerator σ :=
3355 FuchsianGenerator.elliptic
3357 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
3358 let edge : Fin q → φ.ker :=
3360 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3361 let lower :=
3362 (List.ofFn (fun i : Fin k.val => edge ⟨k.val - i.val, by omega⟩)).prod
3363 let wrap := edge ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩
3364 let upper :=
3365 (List.ofFn (fun i : Fin (q - 1 - k.val) => edge ⟨q - 1 - i.val, by omega⟩)).prod
3366 lower * wrap * upper =
3367 (⟨(FreeGroup.of x) ^ k.val * (FreeGroup.of y) ^ q *
3368 ((FreeGroup.of x) ^ k.val)⁻¹, by
3369 rw [MonoidHom.mem_ker]
3370 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
3371 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
3372 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
3373 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod q) := by
3374 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
3375 secondReductionCanonicalSourceMiddleIndex, Nat.reduceAdd, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
3376 secondReductionCanonicalSourceQuotientImage, Nat.succ_ne_self, ↓reduceIte, ofAdd_neg, φ, y]
3378 apply (Multiplicative.toAdd : Multiplicative (ZMod q) ≃ ZMod q).injective
3379 simp only [ofAdd_neg, inv_pow, mul_inv_cancel_comm, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul,
3380 CharP.cast_eq_zero, mul_one, neg_zero, toAdd_one]⟩ : φ.ker) := by
3381 classical
3382 dsimp
3383 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3384 let σ :=
3386 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3387 let φ :=
3389 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3390 let x : FuchsianGenerator σ :=
3392 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3393 let y : FuchsianGenerator σ :=
3394 FuchsianGenerator.elliptic
3396 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)
3397 let edge : Fin q → φ.ker :=
3399 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3400 let lower :=
3401 (List.ofFn (fun i : Fin k.val => edge ⟨k.val - i.val, by omega⟩)).prod
3402 let wrap := edge ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩
3403 let upper :=
3404 (List.ofFn (fun i : Fin (q - 1 - k.val) => edge ⟨q - 1 - i.val, by omega⟩)).prod
3405 apply Subtype.ext
3406 change
3407 ((lower * wrap * upper : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
3408 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
3409 (FreeGroup.of y) ^ q *
3410 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹
3411 have hlowerCoe :
3412 ((lower : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
3413 (List.ofFn (fun i : Fin k.val =>
3414 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (k.val - i.val) *
3415 FreeGroup.of y *
3416 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
3417 (k.val - 1 - i.val))⁻¹)).prod := by
3418 change
3419 φ.ker.subtype lower =
3420 (List.ofFn (fun i : Fin k.val =>
3421 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (k.val - i.val) *
3422 FreeGroup.of y *
3423 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
3424 (k.val - 1 - i.val))⁻¹)).prod
3425 simp only [Subgroup.subtype_apply, Subgroup.val_list_prod, List.map_ofFn, lower, edge]
3426 apply congrArg List.prod
3427 apply List.ofFn_inj.2
3428 funext i
3429 let i' : Fin (q - 1) := ⟨k.val - 1 - i.val, by omega⟩
3430 have hidx :
3431 (⟨i'.val + 1, by omega⟩ : Fin q) = ⟨k.val - i.val, by omega⟩ := by
3432 ext
3433 simp only [i']
3434 omega
3435 have hs : k.val - 1 - i.val + 1 = k.val - i.val := by omega
3436 simpa [σ, φ, x, y, edge, i', hidx, hs] using
3438 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i'
3439 have hwrapCoe :
3440 ((wrap : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
3441 FreeGroup.of y *
3442 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (q - 1))⁻¹ := by
3443 simpa [σ, φ, x, y, edge, wrap] using
3445 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3446 have hupperCoe :
3447 ((upper : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
3448 (List.ofFn (fun i : Fin (q - 1 - k.val) =>
3449 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (q - 1 - i.val) *
3450 FreeGroup.of y *
3451 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
3452 (q - 1 - 1 - i.val))⁻¹)).prod := by
3453 change
3454 φ.ker.subtype upper =
3455 (List.ofFn (fun i : Fin (q - 1 - k.val) =>
3456 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (q - 1 - i.val) *
3457 FreeGroup.of y *
3458 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^
3459 (q - 1 - 1 - i.val))⁻¹)).prod
3460 simp only [Subgroup.subtype_apply, Subgroup.val_list_prod, List.map_ofFn, upper, edge]
3461 apply congrArg List.prod
3462 apply List.ofFn_inj.2
3463 funext i
3464 let i' : Fin (q - 1) := ⟨i.val, by omega⟩
3465 simpa [σ, φ, x, y, edge, i'] using
3467 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail i'
3468 change
3469 ((lower : φ.ker) : FreeGroup (FuchsianGenerator σ)) *
3470 ((wrap : φ.ker) : FreeGroup (FuchsianGenerator σ)) *
3471 ((upper : φ.ker) : FreeGroup (FuchsianGenerator σ)) =
3472 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
3473 (FreeGroup.of y) ^ q *
3474 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹
3475 rw [hlowerCoe, hwrapCoe, hupperCoe]
3476 rw [secondReduction_negOneCycleSegmentProduct_eq (FreeGroup.of x) (FreeGroup.of y)
3477 k.val k.val (by omega)]
3478 rw [secondReduction_negOneCycleSegmentProduct_eq (FreeGroup.of x) (FreeGroup.of y)
3479 (q - 1) (q - 1 - k.val) (by omega)]
3480 have hkk : k.val - k.val = 0 := by omega
3481 have hlast : q - 1 - (q - 1 - k.val) = k.val := by omega
3482 rw [hkk, hlast]
3483 simp only [pow_zero, inv_one, mul_one]
3484 have hkadd : k.val + 1 + (q - 1 - k.val) = q := by omega
3485 calc
3486 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
3487 (FreeGroup.of y) ^ k.val *
3488 (FreeGroup.of y * ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (q - 1))⁻¹) *
3489 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (q - 1) *
3490 (FreeGroup.of y) ^ (q - 1 - k.val) *
3491 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹)
3492 =
3493 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
3494 ((FreeGroup.of y) ^ k.val * FreeGroup.of y *
3495 (FreeGroup.of y) ^ (q - 1 - k.val)) *
3496 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ := by
3497 group
3498 _ =
3499 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
3500 (FreeGroup.of y) ^ q *
3501 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ := by
3502 rw [← pow_succ (FreeGroup.of y) k.val]
3503 rw [← pow_add (FreeGroup.of y) (k.val + 1) (q - 1 - k.val)]
3504 rw [hkadd]
3506 {tailLen p q : ℕ}
3507 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
3508 (hp : 2 ≤ p) (hq : 2 ≤ q)
3509 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
3510 (htail : ∀ j, 2 ≤ tail j) :
3511 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3512 let σ :=
3514 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3515 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3516 let φ :=
3518 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3519 let hT :=
3521 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3522 ∀ z : ↥(schreierGeneratorSet hT),
3523 (z : φ.ker) =
3525 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ∨
3526 (∃ k : Fin q,
3527 (z : φ.ker) =
3529 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k) ∨
3530 (∃ y :
3533 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail),
3534 ∃ hy :
3536 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3537 (FreeGroup.of y) = 1,
3538 ∃ k : Fin q,
3539 (z : φ.ker) =
3541 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k) := by
3542 classical
3543 dsimp
3544 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
3545 let σ :=
3547 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3548 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
3549 let φ :=
3551 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3552 let x : FuchsianGenerator σ :=
3554 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3555 let hT :=
3557 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3558 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod q) := by
3559 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalDistinguishedGenerator,
3560 secondReductionCanonicalSourceFreeQuotientHom_firstDistinguished m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail, φ, x]
3561 intro z
3562 rcases z.property with ⟨t, ht, g, hz, hne⟩
3563 have htPower : ∃ k : Fin q, t = (FreeGroup.of x) ^ k.val := by
3564 simpa [hT, secondReductionCanonicalSchreierTransversal, φ, x] using
3565 (mem_range_cyclicQuotientRightRep_iff_generatorPower φ (x := x) hx).1 ht
3566 rcases htPower with ⟨k, rfl⟩
3567 cases g with
3568 | elliptic i =>
3569 by_cases h2 : i.val = 2
3570 · have hi :
3571 i =
3573 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3574 ⟨0, by omega⟩ := by
3575 ext
3576 simpa [secondReductionCanonicalSourceMiddleIndex] using h2
3577 by_cases hwrap : k.val + 1 < q
3578 · have hgen :
3579 schreierGenerator hT ((FreeGroup.of x) ^ k.val) x = 1 := by
3580 simpa [hT, σ, φ, x, secondReductionCanonicalDistinguishedGenerator] using
3582 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail hwrap
3583 exact False.elim
3584 (hne (by simpa [hz, x, hi, secondReductionCanonicalDistinguishedGenerator] using hgen))
3585 · have hk : k.val = q - 1 := by
3586 have hklt := k.isLt
3587 omega
3588 left
3589 calc
3590 (z : φ.ker) = schreierGenerator hT ((FreeGroup.of x) ^ k.val) x := by
3591 simpa [x, hi, secondReductionCanonicalDistinguishedGenerator] using hz
3592 _ = schreierGenerator hT ((FreeGroup.of x) ^ (q - 1)) x := by
3593 rw [hk]
3594 _ =
3596 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by
3597 simpa [hT, σ, φ, x, secondReductionCanonicalDistinguishedGenerator] using
3599 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3600 · by_cases h3 : i.val = 3
3601 · have hp1 : 1 < p := by omega
3602 have hi :
3603 i =
3605 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
3606 ⟨1, hp1⟩ := by
3607 ext
3608 simpa [secondReductionCanonicalSourceMiddleIndex] using h3
3609 right
3610 left
3611 refine ⟨k, ?_⟩
3612 calc
3613 (z : φ.ker) =
3614 schreierGenerator hT ((FreeGroup.of x) ^ k.val)
3615 (FuchsianGenerator.elliptic
3617 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, hp1⟩)) := by
3618 simpa [hi] using hz
3619 _ =
3621 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k := by
3622 simpa [hT, σ, φ, x, secondReductionCanonicalDistinguishedGenerator] using
3624 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k
3625 · right
3626 right
3627 let y : FuchsianGenerator σ := FuchsianGenerator.elliptic i
3628 have hy : φ (FreeGroup.of y) = 1 := by
3629 simp only [Lean.Elab.WF.paramLet, secondReductionCanonicalSourceFreeQuotientHom, id_eq,
3630 FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, secondReductionCanonicalSourceQuotientImage, h2,
3631 ↓reduceIte, h3, φ, y]
3632 refine ⟨y, hy, k, ?_⟩
3633 calc
3634 (z : φ.ker) =
3635 schreierGenerator hT ((FreeGroup.of x) ^ k.val) y := by
3636 simpa [y] using hz
3637 _ =
3639 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k := by
3640 simpa [hT, σ, φ, x, y] using
3642 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail y hy k
3643 | surfaceA i =>
3644 exact Fin.elim0 (by
3645 simpa [σ, secondReductionCanonicalSourceSignature] using i)
3646 | surfaceB i =>
3647 exact Fin.elim0 (by
3648 simpa [σ, secondReductionCanonicalSourceSignature] using i)
3649end FenchelNielsen