FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/QuotientAndBasis.lean
1import FenchelNielsenZomorrodian.Discrete.Core.EllipticCompact
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.QuotientAndBasis
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/QuotientAndBasis.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15Handles the cleanup of period-one target entries using quotient maps, kernel equivalences, low-cardinality dihedral cases, source subgroups, and relator proofs.
16-/
18open scoped BigOperators
19namespace FenchelNielsen
22 {tailLen p : ℕ}
23 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
24 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
25 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
26 (x : OriginalFirstReductionIndex tailLen) :
27 let source :=
28 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
29 source.periods ((originalFirstReductionOrderedIndexEquiv tailLen) x) =
30 originalFirstReductionPeriods (p := p) m₁' m₂' tail x := by
31 classical
32 dsimp
33 let source :=
34 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
35 cases x using Sum.casesOn with
36 | inl i =>
37 fin_cases i <;>
38 simp only [originalFirstReductionSignature, Fin.mk_zero, Fin.mk_one, Fin.isValue,
39 originalFirstReductionOrderedIndexEquiv, Fin.val_eq_zero_iff, Equiv.coe_fn_mk, Fin.coe_ofNat_eq_mod, Nat.mod_succ,
40 originalFirstReductionSignaturePeriod, one_ne_zero, ↓reduceDIte, originalFirstReductionPeriods, twoPeriods,
41 Nat.reduceAdd, fin_cases_const_one, Fin.cases_zero]
42 | inr j =>
47 {tailLen p : ℕ}
48 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
49 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
50 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
51 let source :=
52 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
53 let e := originalFirstReductionOrderedIndexEquiv tailLen
54 totalRelation source =
57 (List.ofFn (fun j : Fin tailLen =>
59 classical
60 dsimp
61 let source :=
62 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
63 let e := originalFirstReductionOrderedIndexEquiv tailLen
64 change totalRelation source =
68 have hOneFin : (1 : Fin (2 + tailLen)) = ⟨1, by omega⟩ := by
69 apply Fin.ext
70 simp only [Fin.coe_ofNat_eq_mod]
71 rw [Nat.mod_eq_of_lt (by omega : 1 < 2 + tailLen)]
72 rw [totalRelation]
73 simpa [source, e, originalFirstReductionSignature, List.ofFn_eq_map,
74 List.prod_cons, mul_assoc, hOneFin] using
75 congrArg List.prod
76 (list_ofFn_two_add (fun i : Fin (2 + tailLen) => xWord source i))
78noncomputable def originalFirstReductionPeriodOneQuotientImage
79 {tailLen p : ℕ}
80 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
81 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
82 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
83 (e :
84 OriginalFirstReductionIndex tailLen ≃
85 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
86 hTailLen).numPeriods) :
87 (let source :=
88 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
89 Fin source.numPeriods → Multiplicative (ZMod p)) :=
90 fun i =>
91 match e.symm i with
92 | .inl h => twoPeriods (Multiplicative.ofAdd (1 : ZMod p))
93 (Multiplicative.ofAdd (-1 : ZMod p)) h
94 | .inr _ => 1
97 {tailLen p : ℕ}
98 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
99 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
100 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
101 (e :
102 OriginalFirstReductionIndex tailLen ≃
103 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
104 hTailLen).numPeriods)
105 (hperiods :
106 let source :=
107 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
108 ∀ x : OriginalFirstReductionIndex tailLen,
109 source.periods (e x) =
110 originalFirstReductionPeriods (p := p) m₁' m₂' tail x) :
111 let source :=
112 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
113 ∀ i : Fin source.numPeriods,
115 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e i ^
116 source.periods i = 1 := by
117 classical
118 dsimp
119 let source :=
120 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
121 intro i
122 let x : OriginalFirstReductionIndex tailLen := e.symm i
123 have hi : i = e x := by
124 simp only [Equiv.apply_symm_apply, x]
125 rw [hi]
126 cases x using Sum.casesOn with
127 | inl h =>
128 rw [hperiods (.inl h)]
129 fin_cases h
130 · apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
131 simp only [originalFirstReductionPeriodOneQuotientImage, Fin.zero_eta, Fin.isValue, Equiv.symm_apply_apply,
132 twoPeriods, Nat.reduceAdd, ofAdd_neg, Fin.cases_zero, originalFirstReductionPeriods, toAdd_pow, toAdd_ofAdd,
133 nsmul_eq_mul, Nat.cast_mul, CharP.cast_eq_zero, zero_mul, mul_one, toAdd_one]
134 · apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
135 simp only [originalFirstReductionPeriodOneQuotientImage, Fin.mk_one, Fin.isValue, Equiv.symm_apply_apply,
136 twoPeriods, Nat.reduceAdd, ofAdd_neg, fin_cases_const_one, originalFirstReductionPeriods, inv_pow, toAdd_inv,
137 toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, Nat.cast_mul, CharP.cast_eq_zero, zero_mul, mul_one, neg_zero, toAdd_one]
138 | inr j =>
139 rw [hperiods (.inr j)]
140 simp only [originalFirstReductionPeriodOneQuotientImage, Equiv.symm_apply_apply, one_pow]
143 {tailLen p : ℕ}
144 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
145 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
146 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
147 (e :
148 OriginalFirstReductionIndex tailLen ≃
149 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
150 hTailLen).numPeriods) :
151 let source :=
152 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
153 ∏ i : Fin source.numPeriods,
155 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e i = 1 := by
156 classical
157 dsimp
158 let source :=
159 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
160 rw [← Equiv.prod_comp e]
161 simp only [OriginalFirstReductionIndex, originalFirstReductionPeriodOneQuotientImage, Equiv.symm_apply_apply,
162 ofAdd_neg, Fintype.prod_sum_type, Fin.prod_univ_two, Fin.isValue, twoPeriods_zero, twoPeriods_one, mul_inv_cancel,
163 Finset.prod_const_one, mul_one]
165noncomputable def originalFirstReductionPeriodOneFreeQuotientHom
166 {tailLen p : ℕ}
167 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
168 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
169 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
170 (e :
171 OriginalFirstReductionIndex tailLen ≃
172 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
173 hTailLen).numPeriods) :
174 let source :=
175 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
176 FreeGroup (FuchsianGenerator source) →* Multiplicative (ZMod p) := by
177 classical
178 dsimp
179 let source :=
180 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
181 exact
182 FreeGroup.lift
183 (ellipticQuotientGeneratorImage source
185 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e))
188 {tailLen p : ℕ}
189 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
190 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
191 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
192 (e :
193 OriginalFirstReductionIndex tailLen ≃
194 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
195 hTailLen).numPeriods)
196 (hperiods :
197 let source :=
198 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
199 ∀ x : OriginalFirstReductionIndex tailLen,
200 source.periods (e x) =
201 originalFirstReductionPeriods (p := p) m₁' m₂' tail x) :
202 let source :=
203 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
206 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e r = 1 := by
207 classical
208 dsimp
209 let source :=
210 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
211 simpa [originalFirstReductionPeriodOneFreeQuotientHom, source] using
214 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e)
216 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods)
218 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e)
221 {tailLen p : ℕ}
222 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
223 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
224 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
225 (e :
226 OriginalFirstReductionIndex tailLen ≃
227 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
228 hTailLen).numPeriods) :
230 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
231 (FreeGroup.of (FuchsianGenerator.elliptic (e (.inl (0 : Fin 2))))) =
232 Multiplicative.ofAdd (1 : ZMod p) := by
233 classical
234 dsimp
235 simp only [originalFirstReductionPeriodOneFreeQuotientHom, Lean.Elab.WF.paramLet, id_eq, Fin.isValue,
236 FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, originalFirstReductionPeriodOneQuotientImage,
237 Equiv.symm_apply_apply, ofAdd_neg, twoPeriods_zero]
240 {tailLen p : ℕ}
241 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
242 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
243 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
244 (e :
245 OriginalFirstReductionIndex tailLen ≃
246 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
247 hTailLen).numPeriods) :
249 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
250 (FreeGroup.of (FuchsianGenerator.elliptic (e (.inl (1 : Fin 2))))) =
251 Multiplicative.ofAdd (-1 : ZMod p) := by
252 classical
253 dsimp
254 simp only [originalFirstReductionPeriodOneFreeQuotientHom, Lean.Elab.WF.paramLet, id_eq, Fin.isValue,
255 FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, originalFirstReductionPeriodOneQuotientImage,
256 Equiv.symm_apply_apply, twoPeriods, Nat.reduceAdd, ofAdd_neg, fin_cases_const_one]
259 {tailLen p : ℕ}
260 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
261 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
262 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
263 (e :
264 OriginalFirstReductionIndex tailLen ≃
265 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
266 hTailLen).numPeriods)
267 (j : Fin tailLen) :
269 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
270 (FreeGroup.of (FuchsianGenerator.elliptic (e (.inr j)))) = 1 := by
271 classical
272 dsimp
273 simp only [originalFirstReductionPeriodOneFreeQuotientHom, Lean.Elab.WF.paramLet, id_eq,
274 FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, originalFirstReductionPeriodOneQuotientImage,
275 Equiv.symm_apply_apply]
277noncomputable def originalFirstReductionPeriodOneDistinguishedGenerator
278 {tailLen p : ℕ}
279 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
280 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
281 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
282 (e :
283 OriginalFirstReductionIndex tailLen ≃
284 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
285 hTailLen).numPeriods) :
286 let source :=
287 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
288 FuchsianGenerator source := by
289 classical
290 dsimp
291 exact FuchsianGenerator.elliptic (e (.inl (0 : Fin 2)))
293noncomputable def originalFirstReductionPeriodOneSchreierTransversal
294 {tailLen p : ℕ}
295 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
296 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
297 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
298 (e :
299 OriginalFirstReductionIndex tailLen ≃
300 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
301 hTailLen).numPeriods) :
302 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
303 let source :=
304 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
305 Set (FreeGroup (FuchsianGenerator source)) := by
306 classical
307 dsimp
308 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
309 let source :=
310 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
311 let φ :=
313 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
314 let x : FuchsianGenerator source :=
316 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
317 exact Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
320 {tailLen p : ℕ}
321 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
322 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
323 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
324 (e :
325 OriginalFirstReductionIndex tailLen ≃
326 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
327 hTailLen).numPeriods) :
328 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
329 let source :=
330 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
331 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
332 let φ :=
334 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
337 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e) := by
338 classical
339 dsimp
340 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
341 let source :=
342 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
343 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
344 let φ :=
346 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
347 let x : FuchsianGenerator source :=
349 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
350 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
351 simpa [φ, x, originalFirstReductionPeriodOneDistinguishedGenerator] using
353 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
354 simpa [originalFirstReductionPeriodOneSchreierTransversal, source, φ, x] using
357noncomputable def originalFirstReductionPeriodOneSchreierBasisEquiv
358 {tailLen p : ℕ}
359 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
360 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
361 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
362 (e :
363 OriginalFirstReductionIndex tailLen ≃
364 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
365 hTailLen).numPeriods) :
366 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
367 let source :=
368 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
369 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
370 let φ :=
372 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
373 let hT :=
375 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
376 FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker := by
377 classical
378 dsimp
379 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
380 let source :=
381 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
382 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
383 let φ :=
385 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
386 let x : FuchsianGenerator source :=
388 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
389 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
390 simpa [φ, x, originalFirstReductionPeriodOneDistinguishedGenerator] using
392 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
395@[simp 900] theorem originalFirstReductionPeriodOneSchreierBasisEquiv_symm_apply
396 {tailLen p : ℕ}
397 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
398 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
399 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
400 (e :
401 OriginalFirstReductionIndex tailLen ≃
402 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
403 hTailLen).numPeriods) :
404 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
405 let source :=
406 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
407 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
408 let φ :=
410 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
411 let hT :=
413 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
414 ∀ z : ↥(schreierGeneratorSet hT),
416 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e).symm (z : φ.ker) =
417 (FreeGroup.of z)⁻¹ := by
418 classical
419 dsimp
420 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
421 let source :=
422 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
423 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
424 let φ :=
426 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
427 let x : FuchsianGenerator source :=
429 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
430 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
431 simpa [φ, x, originalFirstReductionPeriodOneDistinguishedGenerator] using
433 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
434 intro z
435 let basis :=
437 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
438 apply basis.injective
439 simp only [originalFirstReductionPeriodOneSchreierTransversal, Lean.Elab.WF.paramLet, id_eq,
440 originalFirstReductionPeriodOneSchreierBasisEquiv, MulEquiv.apply_symm_apply, map_inv,
441 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator_of φ x hx z, inv_inv, basis, φ, x]
443noncomputable def originalFirstReductionPeriodOneFirstPowerKernel
444 {tailLen p : ℕ}
445 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
446 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
447 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
448 (e :
449 OriginalFirstReductionIndex tailLen ≃
450 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
451 hTailLen).numPeriods) :
452 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
453 let φ :=
455 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
456 φ.ker := by
457 classical
458 dsimp
459 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
460 let source :=
461 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
462 let φ :=
464 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
465 let x : FuchsianGenerator source :=
467 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
468 refine ⟨(FreeGroup.of x) ^ p, ?_⟩
469 rw [MonoidHom.mem_ker]
470 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
471 simpa [φ, x, originalFirstReductionPeriodOneDistinguishedGenerator] using
473 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
474 rw [map_pow, hx]
475 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
476 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]
478noncomputable def originalFirstReductionPeriodOneSecondEdgeKernelElement
479 {tailLen p : ℕ}
480 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
481 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
482 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
483 (e :
484 OriginalFirstReductionIndex tailLen ≃
485 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
486 hTailLen).numPeriods)
487 (k : Fin p) :
488 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
489 let φ :=
491 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
492 φ.ker := by
493 classical
494 dsimp
495 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
496 let source :=
497 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
498 let φ :=
500 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
501 let x : FuchsianGenerator source :=
503 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
504 let y : FuchsianGenerator source := FuchsianGenerator.elliptic (e (.inl (1 : Fin 2)))
505 let r : ℕ := ((k.val : ZMod p) - 1).val
506 refine ⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y * ((FreeGroup.of x) ^ r)⁻¹, ?_⟩
507 rw [MonoidHom.mem_ker]
508 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
509 simpa [φ, x, originalFirstReductionPeriodOneDistinguishedGenerator] using
511 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
512 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
513 simpa [φ, y] using
515 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
517 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
518 simp only [ofAdd_neg, toAdd_mul, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one, toAdd_inv, ZMod.natCast_val,
519 dvd_refl, ZMod.cast_sub, ZMod.cast_natCast, ZMod.cast_one, neg_sub, toAdd_one, r]
520 ring
522noncomputable def originalFirstReductionPeriodOneTailKernelElement
523 {tailLen p : ℕ}
524 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
525 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
526 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
527 (e :
528 OriginalFirstReductionIndex tailLen ≃
529 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
530 hTailLen).numPeriods)
531 (j : Fin tailLen) (k : Fin p) :
532 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
533 let φ :=
535 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
536 φ.ker := by
537 classical
538 dsimp
539 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
540 let source :=
541 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
542 let φ :=
544 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
545 let x : FuchsianGenerator source :=
547 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
548 let y : FuchsianGenerator source := FuchsianGenerator.elliptic (e (.inr j))
549 refine ⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y * ((FreeGroup.of x) ^ k.val)⁻¹, ?_⟩
550 rw [MonoidHom.mem_ker]
551 have hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
552 simpa [φ, x, originalFirstReductionPeriodOneDistinguishedGenerator] using
554 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
555 have hy : φ (FreeGroup.of y) = 1 := by
556 simpa [φ, y] using
558 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j
559 change φ ((FreeGroup.of x) ^ k.val * FreeGroup.of y * ((FreeGroup.of x) ^ k.val)⁻¹) = 1
562noncomputable def originalFirstReductionPeriodOneSecondPowerKernel
563 {tailLen p : ℕ}
564 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
565 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
566 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
567 (e :
568 OriginalFirstReductionIndex tailLen ≃
569 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
570 hTailLen).numPeriods) :
571 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
572 let φ :=
574 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
575 φ.ker := by
576 classical
577 dsimp
578 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
579 let source :=
580 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
581 let φ :=
583 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
584 let y : FuchsianGenerator source := FuchsianGenerator.elliptic (e (.inl (1 : Fin 2)))
585 refine ⟨(FreeGroup.of y) ^ p, ?_⟩
586 rw [MonoidHom.mem_ker]
587 have hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod p) := by
588 simpa [φ, y] using
590 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
591 rw [map_pow, hy]
592 apply (Multiplicative.toAdd : Multiplicative (ZMod p) ≃ ZMod p).injective
593 simp only [ofAdd_neg, inv_pow, toAdd_inv, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
594 neg_zero, toAdd_one]
597 {tailLen p : ℕ}
598 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
599 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
600 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
601 (e :
602 OriginalFirstReductionIndex tailLen ≃
603 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
604 hTailLen).numPeriods) :
605 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
606 let source :=
607 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
608 let φ :=
610 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
611 let x : FuchsianGenerator source :=
613 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
615 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e : φ.ker) :
616 FreeGroup (FuchsianGenerator source)) =
617 (FreeGroup.of x) ^ p := by
618 classical
619 dsimp
620 simp only [originalFirstReductionPeriodOneFirstPowerKernel, Lean.Elab.WF.paramLet,
621 originalFirstReductionPeriodOneDistinguishedGenerator, Fin.isValue, id_eq]
624 {tailLen p : ℕ}
625 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
626 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
627 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
628 (e :
629 OriginalFirstReductionIndex tailLen ≃
630 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
631 hTailLen).numPeriods) :
632 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
633 let source :=
634 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
635 let φ :=
637 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
638 let y : FuchsianGenerator source := FuchsianGenerator.elliptic (e (.inl (1 : Fin 2)))
640 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e : φ.ker) :
641 FreeGroup (FuchsianGenerator source)) =
642 (FreeGroup.of y) ^ p := by
643 classical
644 dsimp
645 simp only [originalFirstReductionPeriodOneSecondPowerKernel, Lean.Elab.WF.paramLet, Fin.isValue, id_eq]
648 {tailLen p : ℕ}
649 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
650 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
651 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
652 (e :
653 OriginalFirstReductionIndex tailLen ≃
654 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
655 hTailLen).numPeriods)
656 (k : Fin p) :
657 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
658 let source :=
659 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
660 let φ :=
662 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
663 let x : FuchsianGenerator source :=
665 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
666 let y : FuchsianGenerator source := FuchsianGenerator.elliptic (e (.inl (1 : Fin 2)))
667 let r : ℕ := ((k.val : ZMod p) - 1).val
669 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k : φ.ker) :
670 FreeGroup (FuchsianGenerator source)) =
671 (FreeGroup.of x) ^ k.val * FreeGroup.of y * ((FreeGroup.of x) ^ r)⁻¹ := by
672 classical
673 dsimp
674 simp only [originalFirstReductionPeriodOneSecondEdgeKernelElement, Lean.Elab.WF.paramLet,
675 originalFirstReductionPeriodOneDistinguishedGenerator, Fin.isValue, id_eq]
678 {tailLen p : ℕ}
679 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
680 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
681 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
682 (e :
683 OriginalFirstReductionIndex tailLen ≃
684 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
685 hTailLen).numPeriods)
686 (j : Fin tailLen) (k : Fin p) :
687 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
688 let source :=
689 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
690 let φ :=
692 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
693 let x : FuchsianGenerator source :=
695 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
696 let y : FuchsianGenerator source := FuchsianGenerator.elliptic (e (.inr j))
698 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k : φ.ker) :
699 FreeGroup (FuchsianGenerator source)) =
700 (FreeGroup.of x) ^ k.val * FreeGroup.of y * ((FreeGroup.of x) ^ k.val)⁻¹ := by
701 classical
702 dsimp
703 simp only [originalFirstReductionPeriodOneTailKernelElement, Lean.Elab.WF.paramLet,
704 originalFirstReductionPeriodOneDistinguishedGenerator, Fin.isValue, id_eq]
707 {tailLen p : ℕ}
708 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
709 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
710 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
711 (e :
712 OriginalFirstReductionIndex tailLen ≃
713 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
714 hTailLen).numPeriods)
715 {k₁ k₂ : Fin p}
716 (hEq :
718 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k₁ =
720 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k₂) :
721 k₁ = k₂ := by
722 classical
723 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
724 let source :=
725 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
726 let φ :=
728 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
729 let x : FuchsianGenerator source :=
731 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
732 let y : FuchsianGenerator source := FuchsianGenerator.elliptic (e (.inl (1 : Fin 2)))
733 have hval := congrArg
734 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator source))) hEq
735 let r₁ : ℕ := ((k₁.val : ZMod p) - 1).val
736 let r₂ : ℕ := ((k₂.val : ZMod p) - 1).val
737 have hleft :
739 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k₁ : φ.ker) :
740 FreeGroup (FuchsianGenerator source)) =
741 (FreeGroup.of x) ^ k₁.val * FreeGroup.of y *
742 ((FreeGroup.of x) ^ r₁)⁻¹ := by
743 simpa [source, φ, x, y, r₁] using
745 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k₁
746 have hright :
748 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k₂ : φ.ker) :
749 FreeGroup (FuchsianGenerator source)) =
750 (FreeGroup.of x) ^ k₂.val * FreeGroup.of y *
751 ((FreeGroup.of x) ^ r₂)⁻¹ := by
752 simpa [source, φ, x, y, r₂] using
754 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k₂
755 have hword :
756 (FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val * FreeGroup.of y *
757 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ r₁)⁻¹ =
758 (FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₂.val * FreeGroup.of y *
759 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ r₂)⁻¹ := by
760 simpa [hleft, hright] using hval
761 have hxne : x ≠ y := by
762 intro hEq'
763 simp only [originalFirstReductionPeriodOneDistinguishedGenerator, Lean.Elab.WF.paramLet, Fin.isValue, id_eq,
764 FuchsianGenerator.elliptic.injEq, EmbeddingLike.apply_eq_iff_eq, Sum.inl.injEq, zero_ne_one, x, y] at hEq'
765 exact Fin.ext
769 {tailLen p : ℕ}
770 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
771 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
772 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
773 (e :
774 OriginalFirstReductionIndex tailLen ≃
775 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
776 hTailLen).numPeriods)
777 {j₁ j₂ : Fin tailLen} {k₁ k₂ : Fin p}
778 (hEq :
780 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j₁ k₁ =
782 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j₂ k₂) :
783 j₁ = j₂ ∧ k₁ = k₂ := by
784 classical
785 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
786 let source :=
787 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
788 let φ :=
790 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
791 let x : FuchsianGenerator source :=
793 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
794 let tailGen : Fin tailLen → FuchsianGenerator source := fun j =>
795 FuchsianGenerator.elliptic (e (.inr j))
796 have hval := congrArg
797 (fun z : φ.ker => (z : FreeGroup (FuchsianGenerator source))) hEq
798 have hleft :
800 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j₁ k₁ : φ.ker) :
801 FreeGroup (FuchsianGenerator source)) =
802 (FreeGroup.of x) ^ k₁.val * FreeGroup.of (tailGen j₁) *
803 ((FreeGroup.of x) ^ k₁.val)⁻¹ := by
804 simpa [source, φ, x, tailGen] using
806 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j₁ k₁
807 have hright :
809 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j₂ k₂ : φ.ker) :
810 FreeGroup (FuchsianGenerator source)) =
811 (FreeGroup.of x) ^ k₂.val * FreeGroup.of (tailGen j₂) *
812 ((FreeGroup.of x) ^ k₂.val)⁻¹ := by
813 simpa [source, φ, x, tailGen] using
815 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j₂ k₂
816 have hword :
817 (FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val *
818 FreeGroup.of (tailGen j₁) *
819 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val)⁻¹ =
820 (FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₂.val *
821 FreeGroup.of (tailGen j₂) *
822 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₂.val)⁻¹ := by
823 simpa [hleft, hright] using hval
824 have hxne₁ : x ≠ tailGen j₁ := by
825 intro hEq'
826 simp only [originalFirstReductionPeriodOneDistinguishedGenerator, Lean.Elab.WF.paramLet, Fin.isValue, id_eq,
827 FuchsianGenerator.elliptic.injEq, EmbeddingLike.apply_eq_iff_eq, reduceCtorEq, x, tailGen] at hEq'
828 have hxne₂ : x ≠ tailGen j₂ := by
829 intro hEq'
830 simp only [originalFirstReductionPeriodOneDistinguishedGenerator, Lean.Elab.WF.paramLet, Fin.isValue, id_eq,
831 FuchsianGenerator.elliptic.injEq, EmbeddingLike.apply_eq_iff_eq, reduceCtorEq, x, tailGen] at hEq'
832 have hlen := congrArg
833 (fun w : FreeGroup (FuchsianGenerator source) => (FreeGroup.toWord w).length) hword
834 change
835 (FreeGroup.toWord
836 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val *
837 FreeGroup.of (tailGen j₁) *
838 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val)⁻¹)).length =
839 (FreeGroup.toWord
840 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₂.val *
841 FreeGroup.of (tailGen j₂) *
842 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₂.val)⁻¹)).length at hlen
843 rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₁ k₁.val k₁.val,
844 freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₂ k₂.val k₂.val] at hlen
845 simp only [List.append_assoc, List.cons_append, List.nil_append, List.length_append, List.length_replicate,
846 List.length_cons] at hlen
847 have hk : k₁ = k₂ := by
848 ext
849 omega
850 subst k₂
851 have hwords := congrArg
852 (fun w : FreeGroup (FuchsianGenerator source) => FreeGroup.toWord w) hword
853 change
854 FreeGroup.toWord
855 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val *
856 FreeGroup.of (tailGen j₁) *
857 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val)⁻¹) =
858 FreeGroup.toWord
859 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val *
860 FreeGroup.of (tailGen j₂) *
861 ((FreeGroup.of x : FreeGroup (FuchsianGenerator source)) ^ k₁.val)⁻¹) at hwords
862 rw [freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₁ k₁.val k₁.val,
863 freeGroup_toWord_pow_mul_of_mul_pow_inv hxne₂ k₁.val k₁.val] at hwords
864 have hdrop := congrArg
865 (fun L : List (FuchsianGenerator source × Bool) => L.drop k₁.val) hwords
866 have hhead := congrArg List.head? hdrop
867 have htailGenEq : tailGen j₁ = tailGen j₂ := by
868 simpa using hhead
869 have hj : j₁ = j₂ := by
870 have hidx : (e (.inr j₁) : Fin source.numPeriods) = e (.inr j₂) := by
871 have hidx' :=
872 congrArg
873 (fun g : FuchsianGenerator source =>
874 match g with
875 | .elliptic i => i
876 | .surfaceA _ => e (.inr j₁)
877 | .surfaceB _ => e (.inr j₁))
878 htailGenEq
879 change (e (.inr j₁) : Fin source.numPeriods) = e (.inr j₂) at hidx'
880 exact hidx'
881 exact Sum.inr.inj (e.injective hidx)
882 exact ⟨hj, rfl⟩
884noncomputable def originalFirstReductionPeriodOneQuotientHom
885 {tailLen p : ℕ}
886 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
887 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
888 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
890 (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) →*
891 Multiplicative (ZMod p) := by
892 classical
893 let source :=
894 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
895 let e : OriginalFirstReductionIndex tailLen ≃ Fin source.numPeriods := by
896 simpa [source, originalFirstReductionSignature] using
898 have hperiods :
899 ∀ x : OriginalFirstReductionIndex tailLen,
900 source.periods (e x) =
901 originalFirstReductionPeriods (p := p) m₁' m₂' tail x := by
902 intro x
903 simpa [source, e] using
905 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen x
906 exact
908 (f := ellipticQuotientGeneratorImage source
910 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e))
911 (by
912 simpa [originalFirstReductionPeriodOneFreeQuotientHom, source] using
914 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods)
917 {tailLen p : ℕ}
918 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
919 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
920 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
921 let source :=
922 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
924 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
925 (ellipticElement source
926 ((originalFirstReductionOrderedIndexEquiv tailLen) (.inl (0 : Fin 2)))) =
927 Multiplicative.ofAdd (1 : ZMod p) := by
928 classical
929 dsimp
930 simp only [originalFirstReductionSignature, originalFirstReductionPeriodOneQuotientHom, id_eq,
931 ellipticElement, PresentedGroup.toGroup.of, ellipticQuotientGeneratorImage,
932 originalFirstReductionPeriodOneQuotientImage, originalFirstReductionOrderedIndexEquiv_symm_zero, Fin.isValue,
933 ofAdd_neg, twoPeriods_zero]
936 {tailLen p : ℕ}
937 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
938 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
939 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
940 let source :=
941 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
943 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
944 (ellipticElement source
945 ((originalFirstReductionOrderedIndexEquiv tailLen) (.inl (1 : Fin 2)))) =
946 Multiplicative.ofAdd (-1 : ZMod p) := by
947 classical
948 dsimp
949 simp only [originalFirstReductionSignature, originalFirstReductionPeriodOneQuotientHom, id_eq,
950 ellipticElement, Fin.isValue, originalFirstReductionOrderedIndexEquiv_left_one, PresentedGroup.toGroup.of,
952 originalFirstReductionOrderedIndexEquiv_symm_one, twoPeriods, Nat.reduceAdd, ofAdd_neg, fin_cases_const_one]
955 {tailLen p : ℕ}
956 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
957 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
958 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
959 (j : Fin tailLen) :
960 let source :=
961 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
963 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
964 (ellipticElement source
965 ((originalFirstReductionOrderedIndexEquiv tailLen) (.inr j))) =
966 1 := by
967 classical
968 dsimp
969 simp only [originalFirstReductionSignature, originalFirstReductionPeriodOneQuotientHom, id_eq,
970 ellipticElement, PresentedGroup.toGroup.of, ellipticQuotientGeneratorImage,
971 originalFirstReductionPeriodOneQuotientImage, originalFirstReductionOrderedIndexEquiv_symm_right]
973end FenchelNielsen