FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/KernelEquivalence.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.RelatorProofs
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/KernelEquivalence.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14Handles the cleanup of period-one target entries using quotient maps, kernel equivalences, low-cardinality dihedral cases, source subgroups, and relator proofs.
15-/
17open 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 (e :
27 OriginalFirstReductionIndex tailLen ≃
28 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
29 hTailLen).numPeriods)
30 {Y : Type} (targetRelators : Set (FreeGroup Y)) : Type :=
31 (letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
32 let source :=
33 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
34 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
35 let ξ :=
37 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
38 let f := ellipticQuotientGeneratorImage source ξ
39 let x :=
41 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
42 let hx : FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
43 simpa [f, x, ξ, originalFirstReductionPeriodOneFreeQuotientHom] using
45 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
50 {tailLen p : ℕ}
51 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
52 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
53 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
54 (e :
55 OriginalFirstReductionIndex tailLen ≃
56 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
57 hTailLen).numPeriods)
58 (τ : FuchsianSignature)
59 (θ :
60 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
61 let source :=
62 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
63 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
64 let hT :=
66 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
67 FreeGroup (FuchsianGenerator τ) →* FreeGroup ↥(schreierGeneratorSet hT)) :
68 Type :=
69 (letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
70 let source :=
71 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
72 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
73 let ξ :=
75 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
76 let f := ellipticQuotientGeneratorImage source ξ
77 let T :=
79 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
80 let basis :=
82 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
85 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := relators source) T))
87 θ)
89noncomputable def doublePeriodOneForwardMapData
90 {tailLen p : ℕ}
91 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
92 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
93 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
94 (hHigh : 3 ≤ p * tailLen)
95 (e :
96 OriginalFirstReductionIndex tailLen ≃
97 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
98 hTailLen).numPeriods)
99 (hperiods :
100 let source :=
101 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
102 ∀ x : OriginalFirstReductionIndex tailLen,
103 source.periods (e x) =
104 originalFirstReductionPeriods (p := p) m₁' m₂' tail x)
105 (he : e = originalFirstReductionOrderedIndexEquiv tailLen)
106 (hm₁'one : m₁' = 1) (hm₂'one : m₂' = 1) :
107 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
109 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e target
111 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e) := by
112 classical
113 dsimp
114 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
115 let source :=
116 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
117 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
118 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
119 let ξ :=
121 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
122 let f := ellipticQuotientGeneratorImage source ξ
123 let T :=
125 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
126 let hT :=
128 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
129 let basis :=
131 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
132 let θ :=
134 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e
135 let η :=
137 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e
138 refine
139 { toHom := η
140 mapsRelators := ?_
141 inv_toHom := ?_
142 to_invHom := ?_ }
143 · intro r hr
144 simpa [source, target, ξ, f, T, basis, η] using
146 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e hperiods he
147 hm₁'one hm₂'one r hr
148 · intro w
149 simpa [source, target, ξ, f, T, hT, basis, θ, η] using
151 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e hperiods he
152 hm₁'one w
153 · intro y
154 simpa [source, target, θ, η] using
156 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e
158 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e) y
160noncomputable def oneHeadPeriodOneForwardMapData
161 {tailLen p : ℕ}
162 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
163 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
164 (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
165 (e :
166 OriginalFirstReductionIndex tailLen ≃
167 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
168 hTailLen).numPeriods)
169 (hperiods :
170 let source :=
171 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
172 ∀ x : OriginalFirstReductionIndex tailLen,
173 source.periods (e x) =
174 originalFirstReductionPeriods (p := p) m₁' m₂' tail x)
175 (he : e = originalFirstReductionOrderedIndexEquiv tailLen)
176 (hm₁'one : m₁' = 1) :
177 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
179 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e target
181 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e) := by
182 classical
183 dsimp
184 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
185 let source :=
186 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
187 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
188 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
189 let ξ :=
191 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
192 let f := ellipticQuotientGeneratorImage source ξ
193 let T :=
195 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
196 let hT :=
198 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
199 let basis :=
201 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
202 let θ :=
204 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e
205 let η :=
207 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e
208 refine
209 { toHom := η
210 mapsRelators := ?_
211 inv_toHom := ?_
212 to_invHom := ?_ }
213 · intro r hr
214 simpa [source, target, ξ, f, T, basis, η] using
216 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e hperiods he
217 hm₁'one r hr
218 · intro w
219 simpa [source, target, ξ, f, T, hT, basis, θ, η] using
221 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e hperiods he
222 hm₁'one w
223 · intro y
224 simpa [source, target, θ, η] using
226 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e
228 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e) y
230noncomputable def oneHeadPeriodOneSchreierRelatorData_of_forwardMapData
231 {tailLen p : ℕ}
232 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
233 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
234 (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
235 (e :
236 OriginalFirstReductionIndex tailLen ≃
237 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
238 hTailLen).numPeriods)
239 (hperiods :
240 let source :=
241 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
242 ∀ x : OriginalFirstReductionIndex tailLen,
243 source.periods (e x) =
244 originalFirstReductionPeriods (p := p) m₁' m₂' tail x)
245 (he : e = originalFirstReductionOrderedIndexEquiv tailLen)
246 (hm₁'one : m₁' = 1)
247 (D :
248 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
250 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e target
252 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e)) :
253 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
256 classical
257 dsimp
258 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
259 let source :=
260 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
261 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
262 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
263 let ξ :=
265 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
266 let f := ellipticQuotientGeneratorImage source ξ
267 let T :=
269 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
270 let basis :=
272 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
273 let θ :=
275 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e
276 have hTarget :
278 Subgroup.normalClosure
280 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := relators source) T)) := by
281 simpa [source, target, ξ, f, T, basis, θ] using
283 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e hperiods he hm₁'one
285 OriginalFirstReductionPeriodOneForwardMapData, source, target, ξ, f, T, basis, θ] using
288 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := relators source) T))
290 (invHom := θ)
291 hTarget
292 D)
294noncomputable def doublePeriodOneSchreierRelatorData_of_forwardMapData
295 {tailLen p : ℕ}
296 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
297 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
298 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
299 (hHigh : 3 ≤ p * tailLen)
300 (e :
301 OriginalFirstReductionIndex tailLen ≃
302 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
303 hTailLen).numPeriods)
304 (hperiods :
305 let source :=
306 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
307 ∀ x : OriginalFirstReductionIndex tailLen,
308 source.periods (e x) =
309 originalFirstReductionPeriods (p := p) m₁' m₂' tail x)
310 (he : e = originalFirstReductionOrderedIndexEquiv tailLen)
311 (hm₁'one : m₁' = 1) (hm₂'one : m₂' = 1)
312 (D :
313 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
315 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e target
317 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e)) :
318 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
321 classical
322 dsimp
323 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
324 let source :=
325 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
326 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
327 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
328 let ξ :=
330 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
331 let f := ellipticQuotientGeneratorImage source ξ
332 let T :=
334 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
335 let basis :=
337 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
338 let θ :=
340 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e
341 have hTarget :
343 Subgroup.normalClosure
345 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := relators source) T)) := by
346 simpa [source, target, ξ, f, T, basis, θ] using
348 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e hperiods he
349 hm₁'one hm₂'one
351 OriginalFirstReductionPeriodOneForwardMapData, source, target, ξ, f, T, basis, θ] using
354 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := relators source) T))
356 (invHom := θ)
357 hTarget
358 D)
360noncomputable def originalFirstReductionPeriodOneKernelEquivOfRelatorData
361 {tailLen p : ℕ}
362 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
363 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
364 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
365 (e :
366 OriginalFirstReductionIndex tailLen ≃
367 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
368 hTailLen).numPeriods)
369 (hperiods :
370 let source :=
371 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
372 ∀ x : OriginalFirstReductionIndex tailLen,
373 source.periods (e x) =
374 originalFirstReductionPeriods (p := p) m₁' m₂' tail x)
375 (τ : FuchsianSignature)
378 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
379 let source :=
380 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
381 let ξ :=
383 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
385 FreeGroup.lift (ellipticQuotientGeneratorImage source ξ) r = 1 := by
386 simpa [ξ, originalFirstReductionPeriodOneFreeQuotientHom] using
388 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods
390 (f := ellipticQuotientGeneratorImage source ξ) hrels).ker ≃*
391 FuchsianPresentedGroup τ := by
392 classical
393 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
394 let source :=
395 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
396 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
397 let ξ :=
399 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
400 let hpow : ∀ i, ξ i ^ source.periods i = 1 :=
402 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods
403 let hprod : ∏ i : Fin source.numPeriods, ξ i = 1 :=
405 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
407 FreeGroup.lift (ellipticQuotientGeneratorImage source ξ) r = 1 := by
408 simpa [ξ, originalFirstReductionPeriodOneFreeQuotientHom] using
410 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods
411 let i₀ : Fin source.numPeriods := e (.inl (0 : Fin 2))
412 have hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p) := by
413 simp only [Fin.isValue, originalFirstReductionPeriodOneQuotientImage, Equiv.symm_apply_apply, ofAdd_neg,
414 twoPeriods_zero, ξ, i₀]
415 have hData :
416 FuchsianEllipticCyclicSchreierRelatorData source τ ξ i₀ hi₀ := by
419 source, ξ, i₀, hi₀, originalFirstReductionPeriodOneFreeQuotientHom,
421 simpa [ellipticQuotientHom, source, ξ, hpow, hprod, hrels] using
423 source τ ξ hpow hprod i₀ hi₀ hData
425noncomputable def oneHeadPeriodOneKernelEquivOfForwardMapData
426 {tailLen p : ℕ}
427 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
428 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
429 (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
430 (e :
431 OriginalFirstReductionIndex tailLen ≃
432 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
433 hTailLen).numPeriods)
434 (hperiods :
435 let source :=
436 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
437 ∀ x : OriginalFirstReductionIndex tailLen,
438 source.periods (e x) =
439 originalFirstReductionPeriods (p := p) m₁' m₂' tail x)
440 (he : e = originalFirstReductionOrderedIndexEquiv tailLen)
441 (hm₁'one : m₁' = 1)
442 (D :
443 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
445 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e target
447 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e)) :
448 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
449 let source :=
450 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
451 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
452 let ξ :=
454 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
456 FreeGroup.lift (ellipticQuotientGeneratorImage source ξ) r = 1 := by
457 simpa [ξ, originalFirstReductionPeriodOneFreeQuotientHom] using
459 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods
461 (f := ellipticQuotientGeneratorImage source ξ) hrels).ker ≃*
462 FuchsianPresentedGroup target := by
463 classical
464 dsimp
465 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
466 exact
468 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods target
470 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e hperiods he hm₁'one D)
472noncomputable def doublePeriodOneKernelEquivOfForwardMapData
473 {tailLen p : ℕ}
474 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
475 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
476 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
477 (hHigh : 3 ≤ p * tailLen)
478 (e :
479 OriginalFirstReductionIndex tailLen ≃
480 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
481 hTailLen).numPeriods)
482 (hperiods :
483 let source :=
484 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
485 ∀ x : OriginalFirstReductionIndex tailLen,
486 source.periods (e x) =
487 originalFirstReductionPeriods (p := p) m₁' m₂' tail x)
488 (he : e = originalFirstReductionOrderedIndexEquiv tailLen)
489 (hm₁'one : m₁' = 1) (hm₂'one : m₂' = 1)
490 (D :
491 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
493 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e target
495 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e)) :
496 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
497 let source :=
498 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
499 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
500 let ξ :=
502 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
504 FreeGroup.lift (ellipticQuotientGeneratorImage source ξ) r = 1 := by
505 simpa [ξ, originalFirstReductionPeriodOneFreeQuotientHom] using
507 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods
509 (f := ellipticQuotientGeneratorImage source ξ) hrels).ker ≃*
510 FuchsianPresentedGroup target := by
511 classical
512 dsimp
513 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
514 exact
516 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e hperiods target
518 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e hperiods he
519 hm₁'one hm₂'one D)
522end FenchelNielsen