FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/QuotientAndBasis.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.Signatures
2import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicProductIdentities
3import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicSchreierKernel
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/QuotientAndBasis.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
16The first explicit finite quotient reduction for compact zero-genus Fuchsian presentations, including quotient maps, basis transport, signatures, and relator verification.
17-/
19namespace FenchelNielsen
20noncomputable def firstReductionCanonicalSourceQuotientImage
21 {tailLen p : ℕ}
22 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
23 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
24 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
25 (let σ :=
26 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
27 Fin σ.numPeriods → Multiplicative (ZMod p)) :=
28 fun i =>
29 if i.val = 0 then Multiplicative.ofAdd (1 : ZMod p)
30 else if i.val = 1 then Multiplicative.ofAdd (-1 : ZMod p)
31 else 1
33 {tailLen p : ℕ}
34 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
35 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
36 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
37 let σ :=
38 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
39 ∀ i : Fin σ.numPeriods,
41 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i ^
42 σ.periods i = 1 := by
43 classical
44 dsimp
45 intro i
46 by_cases h0 : i.val = 0
47 · have hi :
48 i =
50 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
51 ext
52 simpa [firstReductionCanonicalSourceZeroIndex] using h0
53 subst i
54 have hzval :
56 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).val = 0 := by
57 simp only [firstReductionCanonicalSourceZeroIndex]
58 rw [firstReductionCanonicalSourceQuotientImage, if_pos hzval]
59 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
60 simp only [firstReductionCanonicalSourceSignature_period_zero, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul,
61 Nat.cast_mul, CharP.cast_eq_zero, zero_mul, mul_one, toAdd_one]
62 · by_cases h1 : i.val = 1
63 · have hi :
64 i =
66 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
67 ext
68 simpa [firstReductionCanonicalSourceOneIndex] using h1
69 subst i
70 have hoval :
72 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).val = 1 := by
73 simp only [firstReductionCanonicalSourceOneIndex]
74 have hnot0 :
76 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).val ≠ 0 := by
77 simp only [firstReductionCanonicalSourceOneIndex, ne_eq, one_ne_zero, not_false_eq_true]
78 rw [firstReductionCanonicalSourceQuotientImage, if_neg hnot0, if_pos hoval]
79 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
80 simp only [ofAdd_neg, firstReductionCanonicalSourceSignature_period_one, inv_pow, toAdd_inv, toAdd_pow,
81 toAdd_ofAdd, nsmul_eq_mul, Nat.cast_mul, CharP.cast_eq_zero, zero_mul, mul_one, neg_zero, toAdd_one]
82 · simp only [firstReductionCanonicalSourceQuotientImage, h0, ↓reduceIte, h1, one_pow]
84 {tailLen p : ℕ}
85 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
86 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
87 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
88 let σ :=
89 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
90 ∏ i : Fin σ.numPeriods,
92 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i = 1 := by
93 classical
94 dsimp
95 let σ :=
96 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
97 change ∏ i : Fin σ.numPeriods,
99 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i = 1
100 rw [Fin.prod_univ_def]
101 rw [← List.ofFn_eq_map]
102 have hNum : σ.numPeriods = 2 + tailLen := by
103 simp only [firstReductionCanonicalSourceSignature, σ]
104 rw [List.ofFn_congr hNum]
105 rw [list_ofFn_two_add]
106 simp only [List.prod_cons]
107 have htailOne :
108 (List.ofFn fun j : Fin tailLen =>
110 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
111 (Fin.cast hNum.symm ⟨2 + j.val, by omega⟩)) =
112 List.ofFn (fun _ : Fin tailLen => (1 : Multiplicative (ZMod p))) := by
113 apply List.ofFn_inj.2
114 funext j
115 simp only [firstReductionCanonicalSourceQuotientImage, Fin.cast_eq_self, Nat.add_eq_zero_iff,
116 OfNat.ofNat_ne_zero, false_and, ↓reduceIte, ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one]
117 omega
118 rw [htailOne]
119 simp only [firstReductionCanonicalSourceQuotientImage, Fin.mk_zero', Fin.cast_eq_self, Fin.coe_ofNat_eq_mod,
120 Nat.zero_mod, ↓reduceIte, one_ne_zero, ofAdd_neg, List.ofFn_const, List.prod_replicate, one_pow, mul_one,
121 mul_inv_cancel]
122noncomputable def firstReductionCanonicalSourceFreeQuotientHom
123 {tailLen p : ℕ}
124 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
125 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
126 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
127 let σ :=
128 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
129 FreeGroup (FuchsianGenerator σ) →* Multiplicative (ZMod p) := by
130 classical
131 dsimp
132 let σ :=
133 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
134 exact
135 FreeGroup.lift
138 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))
139@[simp 900] theorem firstReductionCanonicalSourceFreeQuotientHom_firstGenerator
140 {tailLen p : ℕ}
141 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
142 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
143 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
145 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
146 (FreeGroup.of
147 (FuchsianGenerator.elliptic
149 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen))) =
150 Multiplicative.ofAdd (1 : ZMod p) := by
151 classical
152 dsimp
153 simp only [firstReductionCanonicalSourceFreeQuotientHom, Lean.Elab.WF.paramLet, id_eq,
154 firstReductionCanonicalSourceZeroIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
155 firstReductionCanonicalSourceQuotientImage, ↓reduceIte]
157 {tailLen p : ℕ}
158 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
159 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
160 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
161 let σ :=
162 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
165 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r = 1 := by
166 classical
167 dsimp
168 let σ :=
169 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
170 simpa [firstReductionCanonicalSourceFreeQuotientHom, σ] using
173 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
175 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
177 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
178noncomputable abbrev firstReductionCanonicalDistinguishedGenerator
179 {tailLen p : ℕ}
180 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
181 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
182 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
185 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) :=
186 FuchsianGenerator.elliptic
188 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
189noncomputable def firstReductionCanonicalSchreierTransversal
190 {tailLen p : ℕ}
191 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
192 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
193 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
194 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
195 let σ :=
196 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
197 Set (FreeGroup (FuchsianGenerator σ)) := by
198 classical
199 dsimp
200 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
201 let σ :=
202 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
203 let φ :=
205 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
206 let x : FuchsianGenerator σ :=
208 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
209 exact Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
211 {tailLen p : ℕ}
212 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
213 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
214 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
215 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
216 let σ :=
217 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
218 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
219 let φ :=
221 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
224 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
225 classical
226 dsimp
227 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
228 let σ :=
229 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
230 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
231 let φ :=
233 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
234 let x : FuchsianGenerator σ :=
236 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
237 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
238 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
239 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
240 simpa [firstReductionCanonicalSchreierTransversal, σ, φ, x] using
242noncomputable def firstReductionCanonicalSchreierBasisEquiv
243 {tailLen p : ℕ}
244 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
245 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
246 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
247 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
248 let σ :=
249 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
250 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
251 let φ :=
253 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
254 let hT :=
256 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
257 FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker := by
258 classical
259 dsimp
260 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
261 let σ :=
262 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
263 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
264 let φ :=
266 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
267 let x : FuchsianGenerator σ :=
269 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
270 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
271 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
272 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
273 simpa [firstReductionCanonicalSchreierTransversal, σ, φ, x] using
275@[simp 900] theorem firstReductionCanonicalSchreierBasisEquiv_symm_apply
276 {tailLen p : ℕ}
277 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
278 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
279 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
280 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
281 let σ :=
282 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
283 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
284 let φ :=
286 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
287 let hT :=
289 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
290 ∀ z : ↥(schreierGeneratorSet hT),
292 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).symm (z : φ.ker) =
293 (FreeGroup.of z)⁻¹ := by
294 classical
295 dsimp
296 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
297 let σ :=
298 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
299 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
300 let φ :=
302 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
303 let x : FuchsianGenerator σ :=
305 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
306 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
307 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
308 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
309 intro z
310 let e :=
312 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
313 apply e.injective
314 simp only [firstReductionCanonicalSchreierTransversal, Lean.Elab.WF.paramLet, id_eq,
315 firstReductionCanonicalSchreierBasisEquiv, MulEquiv.apply_symm_apply, map_inv,
316 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator_of φ x hx z, inv_inv, e, φ, x]
317noncomputable def firstReductionCanonicalFirstPowerKernel
318 {tailLen p : ℕ}
319 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
320 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
321 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
322 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
323 let φ :=
325 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
326 φ.ker := by
327 classical
328 dsimp
329 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
330 let σ :=
331 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
332 let φ :=
334 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
335 let x : FuchsianGenerator σ :=
337 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
338 refine ⟨(FreeGroup.of x) ^ p, ?_⟩
339 rw [MonoidHom.mem_ker, map_pow]
340 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
341 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
342 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
343 rw [hx]
344 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
345 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]
347 {tailLen p : ℕ}
348 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
349 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
350 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
351 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
352 let σ :=
353 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
354 let φ :=
356 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
357 let x : FuchsianGenerator σ :=
359 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
361 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen :
362 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
363 (FreeGroup.of x) ^ p := by
364 classical
365 dsimp
366 simp only [firstReductionCanonicalFirstPowerKernel, Lean.Elab.WF.paramLet,
368noncomputable def firstReductionCanonicalSecondPowerKernel
369 {tailLen p : ℕ}
370 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
371 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
372 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
373 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
374 let φ :=
376 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
377 φ.ker := by
378 classical
379 dsimp
380 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
381 let σ :=
382 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
383 let φ :=
385 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
386 let y : FuchsianGenerator σ :=
387 FuchsianGenerator.elliptic
389 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
390 refine ⟨(FreeGroup.of y) ^ p, ?_⟩
391 rw [MonoidHom.mem_ker, map_pow]
392 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
393 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
394 firstReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
395 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
396 rw [hy]
397 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
398 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
399 neg_zero, toAdd_one]
400noncomputable def firstReductionCanonicalSecondEdgeKernelElement
401 {tailLen p : ℕ}
402 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
403 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
404 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
405 (k : Fin p) :
406 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
407 let φ :=
409 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
410 φ.ker := by
411 classical
412 dsimp
413 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
414 let σ :=
415 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
416 let φ :=
418 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
419 let x : FuchsianGenerator σ :=
421 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
422 let y : FuchsianGenerator σ :=
423 FuchsianGenerator.elliptic
425 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
426 let r : ℕ := ((k.val : ZMod p) - 1).val
427 refine ⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y * ((FreeGroup.of x) ^ r)⁻¹, ?_⟩
428 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
429 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
430 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
431 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
432 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
433 firstReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
434 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
435 rw [MonoidHom.mem_ker]
437 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
438 simp only [ofAdd_neg, toAdd_mul, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one, toAdd_inv, ZMod.natCast_val,
439 dvd_refl, ZMod.cast_sub, ZMod.cast_natCast, ZMod.cast_one, neg_sub, toAdd_one, r]
440 ring
442 {tailLen p : ℕ}
443 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
444 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
445 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
446 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
447 let σ :=
448 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
449 let φ :=
451 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
452 let x : FuchsianGenerator σ :=
454 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
455 let y : FuchsianGenerator σ :=
456 FuchsianGenerator.elliptic
458 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
460 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
461 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩ :
462 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
463 FreeGroup.of y * ((FreeGroup.of x) ^ (p - 1))⁻¹ := by
464 classical
465 dsimp
466 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
467 let σ :=
468 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
469 let φ :=
471 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
472 let x : FuchsianGenerator σ :=
474 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
475 let y : FuchsianGenerator σ :=
476 FuchsianGenerator.elliptic
478 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
479 have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
480 have hsucc : (p - 1).succ = p := by omega
481 have hval : (-1 : ZMod p).val = p - 1 := by
482 rw [← hsucc]
483 exact ZMod.val_neg_one (p - 1)
484 simp only [firstReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
485 firstReductionCanonicalDistinguishedGenerator, pow_zero, one_mul, Nat.cast_zero, zero_sub, hval, id_eq]
487 {tailLen p : ℕ}
488 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
489 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
490 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
491 (i : Fin (p - 1)) :
492 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
493 let σ :=
494 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
495 let φ :=
497 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
498 let x : FuchsianGenerator σ :=
500 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
501 let y : FuchsianGenerator σ :=
502 FuchsianGenerator.elliptic
504 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
506 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
507 ⟨p - 1 - i.val, by omega⟩ :
508 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
509 (FreeGroup.of x) ^ (p - 1 - i.val) * FreeGroup.of y *
510 ((FreeGroup.of x) ^ (p - 1 - 1 - i.val))⁻¹ := by
511 classical
512 dsimp
513 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
514 let σ :=
515 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
516 let φ :=
518 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
519 let x : FuchsianGenerator σ :=
521 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
522 let y : FuchsianGenerator σ :=
523 FuchsianGenerator.elliptic
525 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
526 let kNat := p - 1 - i.val
527 have hp_gt_one : 1 < p := lt_of_lt_of_le (by decide : 1 < 2) hp
528 haveI : Fact (1 < p) := ⟨hp_gt_one⟩
529 have hkpos : 0 < kNat := by
530 dsimp [kNat]
531 omega
532 have hklt : kNat < p := by
533 dsimp [kNat]
534 omega
535 have hkval : ((kNat : ZMod p)).val = kNat :=
536 ZMod.val_natCast_of_lt hklt
537 have hsubval : ((kNat : ZMod p) - 1).val = kNat - 1 := by
538 have hle : (1 : ZMod p).val ≤ (kNat : ZMod p).val := by
539 rw [hkval, ZMod.val_one]
540 exact Nat.succ_le_iff.mpr hkpos
541 rw [ZMod.val_sub hle, hkval, ZMod.val_one]
542 have hkSub : kNat - 1 = p - 1 - 1 - i.val := by
543 dsimp [kNat]
544 omega
545 have hsubval' :
546 (((p - 1 - i.val : ℕ) : ZMod p) - 1).val =
547 p - 1 - 1 - i.val := by
548 simpa [kNat, hkSub] using hsubval
551 rw [hsubval']
553 {tailLen p : ℕ}
554 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
555 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
556 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
557 (k : Fin (p - 1)) :
558 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
559 let σ :=
560 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
561 let φ :=
563 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
564 let x : FuchsianGenerator σ :=
566 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
567 let y : FuchsianGenerator σ :=
568 FuchsianGenerator.elliptic
570 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
572 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
573 ⟨k.val + 1, by omega⟩ :
574 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
575 (FreeGroup.of x) ^ (k.val + 1) * FreeGroup.of y *
576 ((FreeGroup.of x) ^ k.val)⁻¹ := by
577 classical
578 dsimp
579 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
580 let σ :=
581 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
582 let φ :=
584 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
585 let x : FuchsianGenerator σ :=
587 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
588 let y : FuchsianGenerator σ :=
589 FuchsianGenerator.elliptic
591 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
592 let kNat := k.val + 1
593 have hp_gt_one : 1 < p := lt_of_lt_of_le (by decide : 1 < 2) hp
594 haveI : Fact (1 < p) := ⟨hp_gt_one⟩
595 have hkpos : 0 < kNat := by
596 dsimp [kNat]
597 omega
598 have hklt : kNat < p := by
599 dsimp [kNat]
600 omega
601 have hkval : ((kNat : ZMod p)).val = kNat :=
602 ZMod.val_natCast_of_lt hklt
603 have hsubval : ((kNat : ZMod p) - 1).val = kNat - 1 := by
604 have hle : (1 : ZMod p).val ≤ (kNat : ZMod p).val := by
605 rw [hkval, ZMod.val_one]
606 exact Nat.succ_le_iff.mpr hkpos
607 rw [ZMod.val_sub hle, hkval, ZMod.val_one]
608 have hkSub : kNat - 1 = k.val := by
609 omega
610 have hsubval' :
611 (((k.val + 1 : ℕ) : ZMod p) - 1).val = k.val := by
612 simpa [kNat, hkSub] using hsubval
615 rw [hsubval']
617 {tailLen p : ℕ}
618 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
619 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
620 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
621 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
622 let n := p - 1
624 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
625 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩ *
626 (List.ofFn (fun i : Fin n =>
628 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
629 ⟨n - i.val, by omega⟩)).prod =
631 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
632 classical
633 dsimp
634 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
635 let n := p - 1
636 let σ :=
637 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
638 let φ :=
640 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
641 let x : FuchsianGenerator σ :=
643 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
644 let y : FuchsianGenerator σ :=
645 FuchsianGenerator.elliptic
647 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
648 apply Subtype.ext
649 change
651 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
652 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩ : φ.ker) :
653 FreeGroup (FuchsianGenerator σ)) *
654 (((List.ofFn (fun i : Fin n =>
656 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
657 ⟨n - i.val, by omega⟩)).prod : φ.ker) :
658 FreeGroup (FuchsianGenerator σ)) =
660 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen : φ.ker) :
661 FreeGroup (FuchsianGenerator σ))
662 have hprodCoe :
663 (((List.ofFn (fun i : Fin n =>
665 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
666 ⟨n - i.val, by omega⟩)).prod : φ.ker) :
667 FreeGroup (FuchsianGenerator σ)) =
668 (List.ofFn (fun i : Fin n =>
670 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
671 ⟨n - i.val, by omega⟩ : φ.ker) :
672 FreeGroup (FuchsianGenerator σ)))).prod := by
673 change
674 φ.ker.subtype
675 ((List.ofFn (fun i : Fin n =>
677 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
678 ⟨n - i.val, by omega⟩)).prod) =
679 (List.ofFn (fun i : Fin n =>
680 φ.ker.subtype
682 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
683 ⟨n - i.val, by omega⟩))).prod
684 rw [map_list_prod, List.map_ofFn]
685 rfl
686 rw [hprodCoe]
688 have htailList :
689 (List.ofFn (fun i : Fin n =>
691 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
692 ⟨n - i.val, by omega⟩ : φ.ker) :
693 FreeGroup (FuchsianGenerator σ)))) =
694 List.ofFn (fun i : Fin n =>
695 (FreeGroup.of x) ^ (n - i.val) * FreeGroup.of y *
696 ((FreeGroup.of x) ^ (n - 1 - i.val))⁻¹) := by
697 apply List.ofFn_inj.2
698 funext i
699 simpa [n, σ, φ, x, y] using
701 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen i
702 rw [htailList]
703 change
704 FreeGroup.of y * ((FreeGroup.of x) ^ n)⁻¹ *
705 negOneCycleTailProduct (FreeGroup.of x) (FreeGroup.of y) n =
706 (FreeGroup.of y) ^ p
707 have hn : n + 1 = p := by
708 dsimp [n]
709 omega
710 rw [← hn]
711 exact negOneCycleProduct_eq_pow (FreeGroup.of x) (FreeGroup.of y) n
713 {tailLen p : ℕ}
714 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
715 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
716 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
717 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
718 let n := p - 1
719 let σ :=
720 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
721 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
722 let e :=
724 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
725 e.symm
727 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
728 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩) *
729 (List.ofFn (fun i : Fin n =>
730 e.symm
732 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
733 ⟨n - i.val, by omega⟩))).prod =
734 e.symm
736 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
737 classical
738 dsimp
739 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
740 let n := p - 1
741 let σ :=
742 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
743 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
744 let e :=
746 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
747 have hcycle :
749 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
750 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hp⟩ *
751 (List.ofFn (fun i : Fin n =>
753 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
754 ⟨n - i.val, by omega⟩)).prod =
756 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
757 simpa [n] using
759 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
760 have hmap := congrArg e.symm hcycle
761 have htailMap :
762 e.symm
763 ((List.ofFn (fun i : Fin n =>
765 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
766 ⟨n - i.val, by omega⟩)).prod) =
767 (List.ofFn (fun i : Fin n =>
768 e.symm
770 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
771 ⟨n - i.val, by omega⟩))).prod := by
772 rw [map_list_prod, List.map_ofFn]
773 rfl
775noncomputable def firstReductionCanonicalTailKernelElement
776 {tailLen p : ℕ}
777 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
778 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
779 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
780 (j : Fin tailLen) (k : Fin p) :
781 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
782 let φ :=
784 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
785 φ.ker := by
786 classical
787 dsimp
788 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
789 let σ :=
790 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
791 let φ :=
793 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
794 let x : FuchsianGenerator σ :=
796 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
797 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
798 FuchsianGenerator.elliptic
800 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
801 refine
802 ⟨(FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
803 ((FreeGroup.of x) ^ k.val)⁻¹, ?_⟩
804 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
805 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
806 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
807 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
808 change
810 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
811 (FreeGroup.of
812 (FuchsianGenerator.elliptic
814 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j))) = 1
815 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
816 firstReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
817 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
818 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one]
819 omega
820 rw [MonoidHom.mem_ker]
821 change
822 φ ((FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
823 ((FreeGroup.of x) ^ k.val)⁻¹) = 1
824 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hx, htailMap, mul_one, map_inv, mul_inv_cancel]
826 {tailLen p : ℕ}
827 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
828 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
829 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
830 {k : ℕ} (hk : k + 1 < p) :
831 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
832 let σ :=
833 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
834 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
835 let x :=
837 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
838 let hT :=
840 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
841 schreierGenerator hT ((FreeGroup.of x) ^ k) x = 1 := by
842 classical
843 dsimp
844 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
845 let σ :=
846 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
847 let φ :=
849 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
850 let x : FuchsianGenerator σ :=
852 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
853 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
854 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
855 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
856 simpa [firstReductionCanonicalSchreierTransversal, φ, x] using
859 {tailLen p : ℕ}
860 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
861 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
862 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
863 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
864 let σ :=
865 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
866 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
867 let x :=
869 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
870 let hT :=
872 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
873 schreierGenerator hT ((FreeGroup.of x) ^ (p - 1)) x =
875 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
876 classical
877 dsimp
878 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
879 let σ :=
880 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
881 let φ :=
883 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
884 let x : FuchsianGenerator σ :=
886 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
887 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
888 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
889 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
891 firstReductionCanonicalFirstPowerKernel, φ, x] using
894 {tailLen p : ℕ}
895 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
896 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
897 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
898 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
899 let σ :=
900 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
901 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
902 let φ :=
904 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
905 let hT :=
907 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
909 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen : φ.ker) ∈
910 schreierGeneratorSet hT := by
911 classical
912 dsimp
913 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
914 let σ :=
915 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
916 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
917 let φ :=
919 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
920 let x : FuchsianGenerator σ :=
922 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
923 let T :=
925 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
926 let hT :=
928 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
929 refine ⟨(FreeGroup.of x) ^ (p - 1), ?_, x, ?_, ?_⟩
930 · have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
931 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
932 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
933 simpa [T, firstReductionCanonicalSchreierTransversal, φ, x] using
935 φ x hx (m := p - 1) (by omega)
936 · simpa [hT, σ, φ, x, firstReductionCanonicalDistinguishedGenerator] using
938 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).symm
939 · intro h
940 have hval := congrArg
941 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) h
942 have hpow : (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ p = 1 := by
943 simpa [σ, φ, x, firstReductionCanonicalDistinguishedGenerator,
945 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen] using hval
946 exact freeGroup_of_pow_ne_one x (by omega) hpow
947private theorem firstReductionCanonical_second_schreierGenerator_eq
948 {tailLen p : ℕ}
949 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
950 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
951 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
952 (k : Fin p) :
953 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
954 let σ :=
955 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
956 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
957 let x :=
959 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
960 let y : FuchsianGenerator σ :=
961 FuchsianGenerator.elliptic
963 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
964 let hT :=
966 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
967 schreierGenerator hT ((FreeGroup.of x) ^ k.val) y =
969 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k := by
970 classical
971 dsimp
972 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
973 let σ :=
974 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
975 let φ :=
977 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
978 let x : FuchsianGenerator σ :=
980 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
981 let y : FuchsianGenerator σ :=
982 FuchsianGenerator.elliptic
984 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
985 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
986 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
987 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
988 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
989 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
990 firstReductionCanonicalSourceOneIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
991 firstReductionCanonicalSourceQuotientImage, one_ne_zero, ↓reduceIte, ofAdd_neg, φ, y]
993 firstReductionCanonicalSecondEdgeKernelElement, φ, x, y] using
994 cyclicQuotient_negOneImage_schreierGenerator_eq φ x y hx hy k
996 {tailLen p : ℕ}
997 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
998 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
999 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1000 (k : Fin p) :
1001 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1002 let σ :=
1003 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1004 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1005 let φ :=
1007 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1008 let hT :=
1010 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1012 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k : φ.ker) ∈
1013 schreierGeneratorSet hT := by
1014 classical
1015 dsimp
1016 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1017 let σ :=
1018 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1019 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1020 let φ :=
1022 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1023 let x : FuchsianGenerator σ :=
1025 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1026 let y : FuchsianGenerator σ :=
1027 FuchsianGenerator.elliptic
1029 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1030 let T :=
1032 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1033 let hT :=
1035 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1036 refine ⟨(FreeGroup.of x) ^ k.val, ?_, y, ?_, ?_⟩
1037 · have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1038 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
1039 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
1040 simpa [T, firstReductionCanonicalSchreierTransversal, φ, x] using
1042 φ x hx (m := k.val) k.isLt
1043 · simpa [hT, σ, φ, x, y, firstReductionCanonicalDistinguishedGenerator] using
1045 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k).symm
1046 · intro h
1047 have hval := congrArg
1048 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) h
1049 let r : ℕ := ((k.val : ZMod p) - 1).val
1050 have hsecondWord :
1051 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
1052 FreeGroup.of y *
1053 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r)⁻¹ = 1 := by
1054 simpa [φ, x, y, r, firstReductionCanonicalSecondEdgeKernelElement,
1055 firstReductionCanonicalDistinguishedGenerator] using hval
1056 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
1057 fun u => if u = y then Multiplicative.ofAdd (1 : ℤ) else 1
1058 have hxne : x ≠ y := by
1059 intro hEq
1060 simp only [firstReductionCanonicalDistinguishedGenerator, firstReductionCanonicalSourceZeroIndex,
1061 firstReductionCanonicalSourceOneIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, zero_ne_one, x, y] at hEq
1062 have hmap := congrArg (FreeGroup.lift χ) hsecondWord
1063 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
1066 {tailLen p : ℕ}
1067 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1068 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1069 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1070 {k₁ k₂ : Fin p}
1071 (hEq :
1073 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k₁ =
1075 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k₂) :
1076 k₁ = k₂ := by
1077 classical
1078 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1079 let σ :=
1080 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1081 let φ :=
1083 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1084 let x : FuchsianGenerator σ :=
1086 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1087 let y : FuchsianGenerator σ :=
1088 FuchsianGenerator.elliptic
1090 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
1091 have hval := congrArg
1092 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
1093 let r₁ : ℕ := ((k₁.val : ZMod p) - 1).val
1094 let r₂ : ℕ := ((k₂.val : ZMod p) - 1).val
1095 have hleft :
1097 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k₁ : φ.ker) :
1098 FreeGroup (FuchsianGenerator σ)) =
1099 (FreeGroup.of x) ^ k₁.val * FreeGroup.of y *
1100 ((FreeGroup.of x) ^ r₁)⁻¹ := by
1101 simp only [firstReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
1102 firstReductionCanonicalDistinguishedGenerator, id_eq, σ, x, y, r₁]
1103 have hright :
1105 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k₂ : φ.ker) :
1106 FreeGroup (FuchsianGenerator σ)) =
1107 (FreeGroup.of x) ^ k₂.val * FreeGroup.of y *
1108 ((FreeGroup.of x) ^ r₂)⁻¹ := by
1109 simp only [firstReductionCanonicalSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
1110 firstReductionCanonicalDistinguishedGenerator, id_eq, σ, x, y, r₂]
1111 have hword :
1112 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val * FreeGroup.of y *
1113 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r₁)⁻¹ =
1114 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val * FreeGroup.of y *
1115 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ r₂)⁻¹ := by
1116 simpa [hleft, hright] using hval
1117 have hxne : x ≠ y := by
1118 intro hEq'
1119 simp only [firstReductionCanonicalDistinguishedGenerator, firstReductionCanonicalSourceZeroIndex,
1120 firstReductionCanonicalSourceOneIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, zero_ne_one, x, y] at hEq'
1121 exact Fin.ext
1123private theorem firstReductionCanonical_tail_schreierGenerator_eq
1124 {tailLen p : ℕ}
1125 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1126 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1127 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1128 (j : Fin tailLen) (k : Fin p) :
1129 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1130 let σ :=
1131 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1132 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1133 let x :=
1135 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1136 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1137 FuchsianGenerator.elliptic
1139 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1140 let hT :=
1142 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1143 schreierGenerator hT ((FreeGroup.of x) ^ k.val) (tailGen j) =
1145 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k := by
1146 classical
1147 dsimp
1148 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1149 let σ :=
1150 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1151 let φ :=
1153 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1154 let x : FuchsianGenerator σ :=
1156 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1157 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1158 FuchsianGenerator.elliptic
1160 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1161 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1162 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
1163 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
1164 have htailMap : φ (FreeGroup.of (tailGen j)) = 1 := by
1165 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalSourceFreeQuotientHom, id_eq,
1166 firstReductionCanonicalSourceTailIndex, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage,
1167 firstReductionCanonicalSourceQuotientImage, Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceIte,
1168 ofAdd_neg, ite_eq_right_iff, inv_eq_one, ofAdd_eq_one, φ, tailGen]
1169 omega
1171 firstReductionCanonicalTailKernelElement, φ, x, tailGen] using
1172 cyclicQuotient_trivialImage_schreierGenerator_eq_conj φ x (tailGen j) hx htailMap k
1174 {tailLen p : ℕ}
1175 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1176 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1177 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1178 (j : Fin tailLen) (k : Fin p) :
1179 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1180 let σ :=
1181 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1182 let φ :=
1184 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1185 let x : FuchsianGenerator σ :=
1187 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1188 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1189 FuchsianGenerator.elliptic
1191 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1193 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k :
1194 φ.ker) : FreeGroup (FuchsianGenerator σ)) =
1195 (FreeGroup.of x) ^ k.val * FreeGroup.of (tailGen j) *
1196 ((FreeGroup.of x) ^ k.val)⁻¹ := by
1197 classical
1198 dsimp
1199 simp only [firstReductionCanonicalTailKernelElement, Lean.Elab.WF.paramLet,
1202 {tailLen p : ℕ}
1203 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1204 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1205 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1206 {j₁ j₂ : Fin tailLen} {k₁ k₂ : Fin p}
1207 (hEq :
1209 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j₁ k₁ =
1211 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j₂ k₂) :
1212 j₁ = j₂ ∧ k₁ = k₂ := by
1213 classical
1214 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1215 let σ :=
1216 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1217 let φ :=
1219 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1220 let x : FuchsianGenerator σ :=
1222 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1223 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1224 FuchsianGenerator.elliptic
1226 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1227 have hval := congrArg
1228 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) hEq
1229 have hleft :
1231 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j₁ k₁ : φ.ker) :
1232 FreeGroup (FuchsianGenerator σ)) =
1233 (FreeGroup.of x) ^ k₁.val * FreeGroup.of (tailGen j₁) *
1234 ((FreeGroup.of x) ^ k₁.val)⁻¹ := by
1235 simpa [σ, φ, x, tailGen] using
1237 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j₁ k₁
1238 have hright :
1240 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j₂ k₂ : φ.ker) :
1241 FreeGroup (FuchsianGenerator σ)) =
1242 (FreeGroup.of x) ^ k₂.val * FreeGroup.of (tailGen j₂) *
1243 ((FreeGroup.of x) ^ k₂.val)⁻¹ := by
1244 simpa [σ, φ, x, tailGen] using
1246 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j₂ k₂
1247 have hword :
1248 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
1249 FreeGroup.of (tailGen j₁) *
1250 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹ =
1251 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val *
1252 FreeGroup.of (tailGen j₂) *
1253 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val)⁻¹ := by
1254 simpa [hleft, hright] using hval
1255 have hxne₁ : x ≠ tailGen j₁ := by
1256 intro hEq'
1257 simp only [firstReductionCanonicalDistinguishedGenerator, firstReductionCanonicalSourceZeroIndex,
1258 firstReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, x, tailGen] at hEq'
1259 omega
1260 have hxne₂ : x ≠ tailGen j₂ := by
1261 intro hEq'
1262 simp only [firstReductionCanonicalDistinguishedGenerator, firstReductionCanonicalSourceZeroIndex,
1263 firstReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, x, tailGen] at hEq'
1264 omega
1265 have hlen := congrArg
1266 (fun w : FreeGroup (FuchsianGenerator σ) => (FreeGroup.toWord w).length) hword
1267 change
1268 (FreeGroup.toWord
1269 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
1270 FreeGroup.of (tailGen j₁) *
1271 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹)).length =
1272 (FreeGroup.toWord
1273 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val *
1274 FreeGroup.of (tailGen j₂) *
1275 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₂.val)⁻¹)).length at hlen
1276 rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₁ k₁.val k₁.val,
1277 freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₂ k₂.val k₂.val] at hlen
1278 simp only [List.append_assoc, List.cons_append, List.nil_append, List.length_append, List.length_replicate,
1279 List.length_cons] at hlen
1280 have hk : k₁ = k₂ := by
1281 ext
1282 omega
1283 subst k₂
1284 have hwords := congrArg
1285 (fun w : FreeGroup (FuchsianGenerator σ) => FreeGroup.toWord w) hword
1286 change
1287 FreeGroup.toWord
1288 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
1289 FreeGroup.of (tailGen j₁) *
1290 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹) =
1291 FreeGroup.toWord
1292 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val *
1293 FreeGroup.of (tailGen j₂) *
1294 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k₁.val)⁻¹) at hwords
1295 rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₁ k₁.val k₁.val,
1296 freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₂ k₁.val k₁.val] at hwords
1297 have hdrop := congrArg
1298 (fun L : List (FuchsianGenerator σ × Bool) => L.drop k₁.val) hwords
1299 have hhead := congrArg List.head? hdrop
1300 have htailGenEq : tailGen j₁ = tailGen j₂ := by
1301 simpa using hhead
1302 have hjVal : j₁.val = j₂.val := by
1303 simp only [firstReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq,
1304 Nat.add_left_cancel_iff, tailGen] at htailGenEq
1305 omega
1306 exact ⟨Fin.ext hjVal, rfl⟩
1308 {tailLen p : ℕ}
1309 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1310 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1311 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
1312 (j : Fin tailLen) (k : Fin p) :
1313 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1314 let σ :=
1315 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1316 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1317 let φ :=
1319 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1320 let hT :=
1322 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1324 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k : φ.ker) ∈
1325 schreierGeneratorSet hT := by
1326 classical
1327 dsimp
1328 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1329 let σ :=
1330 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1331 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1332 let φ :=
1334 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1335 let x : FuchsianGenerator σ :=
1337 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1338 let tailGen : Fin tailLen → FuchsianGenerator σ := fun j =>
1339 FuchsianGenerator.elliptic
1341 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)
1342 let T :=
1344 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1345 let hT :=
1347 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1348 refine ⟨(FreeGroup.of x) ^ k.val, ?_, tailGen j, ?_, ?_⟩
1349 · have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1350 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
1351 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
1352 simpa [T, firstReductionCanonicalSchreierTransversal, φ, x] using
1354 φ x hx (m := k.val) k.isLt
1355 · simpa [hT, σ, φ, x, tailGen] using
1357 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k).symm
1358 · intro h
1359 have hval := congrArg
1360 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator σ))) h
1361 have htailWord :
1362 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val *
1363 FreeGroup.of (tailGen j) *
1364 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ = 1 := by
1365 simp only [firstReductionCanonicalTailKernelElement_coe m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k,
1366 OneMemClass.coe_one, conj_eq_one_iff, FreeGroup.of_ne_one, φ] at hval
1367 let χ : FuchsianGenerator σ → Multiplicative ℤ :=
1368 fun y => if y = tailGen j then Multiplicative.ofAdd (1 : ℤ) else 1
1369 have hxne : x ≠ tailGen j := by
1370 intro hEq
1371 simp only [firstReductionCanonicalDistinguishedGenerator, firstReductionCanonicalSourceZeroIndex,
1372 firstReductionCanonicalSourceTailIndex, FuchsianGenerator.elliptic.injEq, Fin.mk.injEq, x, tailGen] at hEq
1373 omega
1374 have hmap := congrArg (FreeGroup.lift χ) htailWord
1375 simp only [map_mul, map_pow, FreeGroup.lift_apply_of, hxne, ↓reduceIte, one_pow, one_mul, map_inv, inv_one,
1378 {tailLen p : ℕ}
1379 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
1380 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
1381 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
1382 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1383 let σ :=
1384 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1385 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1386 let φ :=
1388 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1389 let hT :=
1391 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1392 ∀ z : ↥(schreierGeneratorSet hT),
1393 (z : φ.ker) =
1395 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen ∨
1396 (∃ k : Fin p,
1397 (z : φ.ker) =
1399 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k) ∨
1400 (∃ j : Fin tailLen, ∃ k : Fin p,
1401 (z : φ.ker) =
1403 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k) := by
1404 classical
1405 dsimp
1406 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
1407 let σ :=
1408 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1409 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
1410 let φ :=
1412 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1413 let x : FuchsianGenerator σ :=
1415 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1416 let hT :=
1418 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1419 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
1420 simp only [Lean.Elab.WF.paramLet, firstReductionCanonicalDistinguishedGenerator,
1421 firstReductionCanonicalSourceFreeQuotientHom_firstGenerator m₁' m₂' tail hp hm₁' hm₂' htail hTailLen, φ, x]
1422 intro z
1423 rcases z.property with ⟨t, ht, g, hz, hne⟩
1424 have htPower : ∃ k : Fin p, t = (FreeGroup.of x) ^ k.val := by
1425 simpa [hT, firstReductionCanonicalSchreierTransversal, φ, x] using
1426 (mem_range_cyclicQuotientRightRep_iff_generatorPower φ (x := x) hx).1 ht
1427 rcases htPower with ⟨k, rfl⟩
1428 cases g with
1429 | elliptic i =>
1430 by_cases h0 : i.val = 0
1431 · have hi :
1432 i =
1434 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
1435 ext
1436 simpa [firstReductionCanonicalSourceZeroIndex] using h0
1437 subst i
1438 by_cases hwrap : k.val + 1 < p
1439 · have hgen :
1440 schreierGenerator hT ((FreeGroup.of x) ^ k.val) x = 1 := by
1441 simpa [hT, σ, φ, x, firstReductionCanonicalDistinguishedGenerator] using
1443 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hwrap
1444 exact False.elim (hne (by simpa [hz, x] using hgen))
1445 · have hk : k.val = p - 1 := by
1446 have hklt := k.isLt
1447 omega
1448 left
1449 calc
1450 (z : φ.ker) = schreierGenerator hT ((FreeGroup.of x) ^ k.val) x := by
1451 simpa [x, firstReductionCanonicalDistinguishedGenerator] using hz
1452 _ = schreierGenerator hT ((FreeGroup.of x) ^ (p - 1)) x := by
1453 rw [hk]
1454 _ =
1456 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
1457 simpa [hT, σ, φ, x, firstReductionCanonicalDistinguishedGenerator] using
1459 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
1460 · by_cases h1 : i.val = 1
1461 · have hi :
1462 i =
1464 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen := by
1465 ext
1466 simpa [firstReductionCanonicalSourceOneIndex] using h1
1467 subst i
1468 right
1469 left
1470 refine ⟨k, ?_⟩
1471 calc
1472 (z : φ.ker) =
1473 schreierGenerator hT ((FreeGroup.of x) ^ k.val)
1474 (FuchsianGenerator.elliptic
1476 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) := hz
1477 _ =
1479 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k := by
1480 simpa [hT, σ, φ, x, firstReductionCanonicalDistinguishedGenerator] using
1482 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k
1483 · right
1484 right
1485 let j : Fin tailLen := ⟨i.val - 2, by
1486 have hiLt : i.val < 2 + tailLen := by
1487 simp only [firstReductionCanonicalSourceSignature] at i
1488 exact i.isLt
1489 omega⟩
1490 have hiTail :
1491 i =
1493 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j := by
1494 ext
1495 simp only [firstReductionCanonicalSourceTailIndex, j]
1496 omega
1497 refine ⟨j, k, ?_⟩
1498 have hzTail :
1499 (z : φ.ker) =
1500 schreierGenerator hT ((FreeGroup.of x) ^ k.val)
1501 (FuchsianGenerator.elliptic
1503 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)) := by
1504 simpa [hiTail] using hz
1505 calc
1506 (z : φ.ker) =
1507 schreierGenerator hT ((FreeGroup.of x) ^ k.val)
1508 (FuchsianGenerator.elliptic
1510 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j)) := hzTail
1511 _ =
1513 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k := by
1514 simpa [hT, σ, φ, x, firstReductionCanonicalDistinguishedGenerator] using
1516 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j k
1517 | surfaceA i =>
1518 exact Fin.elim0 (by
1519 simpa [σ, firstReductionCanonicalSourceSignature] using i)
1520 | surfaceB i =>
1521 exact Fin.elim0 (by
1522 simpa [σ, firstReductionCanonicalSourceSignature] using i)
1523end FenchelNielsen