FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/LowCardDihedral.lean
1import FenchelNielsenZomorrodian.Discrete.FiniteIndex.KernelTransfer
2import FenchelNielsenZomorrodian.Discrete.FiniteIndex.SmoothQuotientData
3import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.KernelEquivalence
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/LowCardDihedral.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
16Handles the cleanup of period-one target entries using quotient maps, kernel equivalences, low-cardinality dihedral cases, source subgroups, and relator proofs.
17-/
19open scoped BigOperators
21namespace FenchelNielsen
24 {tailLen p : ℕ} (hp : 2 ≤ p) (hTailLen : 0 < tailLen)
25 (hcard : ¬ 3 ≤ p * tailLen) :
26 p = 2 ∧ tailLen = 1 := by
27 have hlt : p * tailLen < 3 := by omega
28 have htail_le : tailLen ≤ 1 := by
29 by_cases hle : tailLen ≤ 1
30 · exact hle
31 · have htail_ge : 2 ≤ tailLen := by omega
32 have hprod_ge : 4 ≤ p * tailLen := Nat.mul_le_mul hp htail_ge
33 omega
34 have htail_eq : tailLen = 1 := by omega
35 have hp_le : p ≤ 2 := by
36 rw [htail_eq, Nat.mul_one] at hlt
37 omega
38 have hp_eq : p = 2 := by omega
39 exact ⟨hp_eq, htail_eq⟩
41private theorem zmod_two_eq_zero_or_one_for_dihedral (z : ZMod 2) :
42 z = 0 ∨ z = 1 := by
43 have hzlt : z.val < 2 := ZMod.val_lt z
44 have hval : z.val = 0 ∨ z.val = 1 := by omega
45 rcases hval with h | h
46 · left
47 rw [← ZMod.natCast_zmod_val z, h]
48 norm_num
49 · right
50 rw [← ZMod.natCast_zmod_val z, h]
51 norm_num
53noncomputable def twoTwoTailDihedralInversion (n : ℕ) :
54 MulAut (Multiplicative (ZMod n)) where
55 toFun x := Multiplicative.ofAdd (-(Multiplicative.toAdd x))
56 invFun x := Multiplicative.ofAdd (-(Multiplicative.toAdd x))
57 left_inv := by
58 intro x
59 cases x
60 simp only [toAdd_ofAdd, ofAdd_neg, toAdd_inv, neg_neg]
61 right_inv := by
62 intro x
63 cases x
64 simp only [toAdd_ofAdd, ofAdd_neg, toAdd_inv, neg_neg]
65 map_mul' := by
66 intro x y
67 cases x
68 cases y
69 simp only [toAdd_mul, toAdd_ofAdd, neg_add_rev, ofAdd_add, ofAdd_neg, mul_comm]
71noncomputable def twoTwoTailDihedralAction (n : ℕ) :
72 Multiplicative (ZMod 2) →* MulAut (Multiplicative (ZMod n)) where
73 toFun t :=
74 if Multiplicative.toAdd t = (0 : ZMod 2) then
75 1
76 else
78 map_one' := by rfl
79 map_mul' := by
80 intro a b
81 have ha := zmod_two_eq_zero_or_one_for_dihedral (Multiplicative.toAdd a)
82 have hb := zmod_two_eq_zero_or_one_for_dihedral (Multiplicative.toAdd b)
83 rcases ha with ha | ha <;> rcases hb with hb | hb
84 · ext x : 1
85 cases x
86 simp only [toAdd_mul, ha, hb, add_zero, ↓reduceIte, MulAut.one_apply, mul_one]
87 · ext x : 1
88 cases x
89 simp only [toAdd_mul, ha, hb, zero_add, one_ne_zero, ↓reduceIte, twoTwoTailDihedralInversion, ofAdd_neg,
90 ofAdd_toAdd, MulEquiv.coe_mk, Equiv.coe_fn_mk, one_mul]
91 · ext x : 1
92 cases x
93 simp only [toAdd_mul, ha, hb, add_zero, one_ne_zero, ↓reduceIte, twoTwoTailDihedralInversion, ofAdd_neg,
94 ofAdd_toAdd, MulEquiv.coe_mk, Equiv.coe_fn_mk, mul_one]
95 · have hsum : (1 : ZMod 2) + 1 = 0 := by
96 simpa using (ZMod.natCast_self 2)
97 ext x : 1
98 cases x
99 simp only [toAdd_mul, ha, hb, hsum, ↓reduceIte, MulAut.one_apply, one_ne_zero, twoTwoTailDihedralInversion,
102abbrev TwoTwoTailDihedralQuotient (n : ℕ) :=
103 Multiplicative (ZMod n) ⋊[twoTwoTailDihedralAction n] Multiplicative (ZMod 2)
105noncomputable def twoTwoTailRotation (n : ℕ) : TwoTwoTailDihedralQuotient n :=
106 SemidirectProduct.inl (Multiplicative.ofAdd (1 : ZMod n))
108noncomputable def twoTwoTailReflectionZero (n : ℕ) : TwoTwoTailDihedralQuotient n :=
109 SemidirectProduct.inr (Multiplicative.ofAdd (1 : ZMod 2))
111noncomputable def twoTwoTailReflectionOne (n : ℕ) : TwoTwoTailDihedralQuotient n :=
112 SemidirectProduct.inl (Multiplicative.ofAdd (1 : ZMod n)) *
113 SemidirectProduct.inr (Multiplicative.ofAdd (1 : ZMod 2))
115/-- The rotation in the two-two-tail dihedral quotient has exponent `n`. -/
116theorem twoTwoTailRotation_pow_period
117 (n : ℕ) :
118 twoTwoTailRotation n ^ n = 1 := by
119 rw [twoTwoTailRotation, ← map_pow
120 (SemidirectProduct.inl :
121 Multiplicative (ZMod n) →* TwoTwoTailDihedralQuotient n)]
122 apply congrArg SemidirectProduct.inl
123 apply (Multiplicative.toAdd : Multiplicative (ZMod n) ≃ ZMod n).injective
124 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]
126/-- The rotation in the two-two-tail dihedral quotient has order `n`. -/
127theorem twoTwoTailRotation_order
128 (n : ℕ) :
129 orderOf (twoTwoTailRotation n) = n := by
130 have hbase : orderOf (Multiplicative.ofAdd (1 : ZMod n)) = n := by
131 simp only [orderOf_ofAdd_eq_addOrderOf, ZMod.addOrderOf_one]
132 simpa [twoTwoTailRotation, hbase] using
133 orderOf_injective
134 (SemidirectProduct.inl :
135 Multiplicative (ZMod n) →* TwoTwoTailDihedralQuotient n)
136 SemidirectProduct.inl_injective
137 (Multiplicative.ofAdd (1 : ZMod n))
139/-- The first reflection in the two-two-tail dihedral quotient squares to one. -/
140theorem twoTwoTailReflectionZero_sq (n : ℕ) :
141 twoTwoTailReflectionZero n ^ 2 = 1 := by
142 have hsum : (1 : ZMod 2) + 1 = 0 := by
143 simpa using (ZMod.natCast_self 2)
144 ext
145 · simp only [twoTwoTailReflectionZero, pow_two, SemidirectProduct.mul_left,
147 toAdd_one, SemidirectProduct.one_left]
148 · simp only [twoTwoTailReflectionZero, pow_two, SemidirectProduct.mul_right,
149 SemidirectProduct.right_inr, toAdd_mul, toAdd_ofAdd, hsum,
150 SemidirectProduct.one_right, toAdd_one]
152/-- The second reflection in the two-two-tail dihedral quotient squares to one. -/
153theorem twoTwoTailReflectionOne_sq (n : ℕ) :
154 twoTwoTailReflectionOne n ^ 2 = 1 := by
155 have href : ¬ Multiplicative.toAdd (Multiplicative.ofAdd (1 : ZMod 2)) = (0 : ZMod 2) := by
156 exact one_ne_zero
157 have hsum : (1 : ZMod 2) + 1 = 0 := by
158 simpa using (ZMod.natCast_self 2)
159 ext
160 · simp only [twoTwoTailDihedralAction, toAdd_eq_zero, twoTwoTailDihedralInversion,
161 ofAdd_neg, ofAdd_toAdd, twoTwoTailReflectionOne, pow_two,
162 SemidirectProduct.mul_left, SemidirectProduct.left_inl, SemidirectProduct.right_inl,
163 MonoidHom.coe_mk, OneHom.coe_mk, ↓reduceIte, SemidirectProduct.left_inr,
164 MulAut.one_apply, mul_one, SemidirectProduct.mul_right, SemidirectProduct.right_inr,
165 one_mul, ofAdd_eq_one, one_ne_zero, MulEquiv.coe_mk, Equiv.coe_fn_mk,
166 mul_inv_cancel, toAdd_one, SemidirectProduct.one_left]
167 · simp only [twoTwoTailDihedralAction, twoTwoTailDihedralInversion,
168 ofAdd_neg, ofAdd_toAdd, twoTwoTailReflectionOne, pow_two,
169 SemidirectProduct.mul_right, SemidirectProduct.right_inl,
170 SemidirectProduct.right_inr, one_mul, toAdd_mul, toAdd_ofAdd, hsum,
171 SemidirectProduct.one_right, toAdd_one]
173/-- The first reflection in the two-two-tail dihedral quotient has order two. -/
174theorem twoTwoTailReflectionZero_order (n : ℕ) :
175 orderOf (twoTwoTailReflectionZero n) = 2 := by
176 have hsq := twoTwoTailReflectionZero_sq n
177 have hdvd : orderOf (twoTwoTailReflectionZero n) ∣ 2 :=
178 orderOf_dvd_of_pow_eq_one hsq
179 have hne : twoTwoTailReflectionZero n ≠ 1 := by
180 intro h
181 have hright := congrArg (fun x : TwoTwoTailDihedralQuotient n => x.right) h
182 simp only [twoTwoTailReflectionZero, SemidirectProduct.right_inr, SemidirectProduct.one_right, ofAdd_eq_one,
183 one_ne_zero] at hright
184 have hnotOne : orderOf (twoTwoTailReflectionZero n) ≠ 1 := by
185 intro horder
186 exact hne (orderOf_eq_one_iff.mp horder)
187 have hnotZero : orderOf (twoTwoTailReflectionZero n) ≠ 0 := by
188 intro hzero
189 rw [hzero] at hdvd
190 norm_num at hdvd
191 have hle : orderOf (twoTwoTailReflectionZero n) ≤ 2 :=
192 Nat.le_of_dvd (by decide : 0 < 2) hdvd
193 omega
195/-- The second reflection in the two-two-tail dihedral quotient has order two. -/
196theorem twoTwoTailReflectionOne_order (n : ℕ) :
197 orderOf (twoTwoTailReflectionOne n) = 2 := by
198 have hsq := twoTwoTailReflectionOne_sq n
199 have hdvd : orderOf (twoTwoTailReflectionOne n) ∣ 2 :=
200 orderOf_dvd_of_pow_eq_one hsq
201 have hne : twoTwoTailReflectionOne n ≠ 1 := by
202 intro h
203 have hright := congrArg (fun x : TwoTwoTailDihedralQuotient n => x.right) h
204 simp only [twoTwoTailReflectionOne, SemidirectProduct.mul_right, SemidirectProduct.right_inl,
205 SemidirectProduct.right_inr, one_mul, SemidirectProduct.one_right, ofAdd_eq_one, one_ne_zero] at hright
206 have hnotOne : orderOf (twoTwoTailReflectionOne n) ≠ 1 := by
207 intro horder
208 exact hne (orderOf_eq_one_iff.mp horder)
209 have hnotZero : orderOf (twoTwoTailReflectionOne n) ≠ 0 := by
210 intro hzero
211 rw [hzero] at hdvd
212 norm_num at hdvd
213 have hle : orderOf (twoTwoTailReflectionOne n) ≤ 2 :=
214 Nat.le_of_dvd (by decide : 0 < 2) hdvd
215 omega
217/-- The two reflections and the rotation satisfy the total-relation product. -/
218theorem twoTwoTail_reflection_product_rotation_eq_one (n : ℕ) :
219 twoTwoTailReflectionZero n * twoTwoTailReflectionOne n * twoTwoTailRotation n = 1 := by
220 have href : ¬ Multiplicative.toAdd (Multiplicative.ofAdd (1 : ZMod 2)) = (0 : ZMod 2) := by
221 exact one_ne_zero
222 have hsum : (1 : ZMod 2) + 1 = 0 := by
223 simpa using (ZMod.natCast_self 2)
224 ext
225 · simp only [twoTwoTailDihedralAction, toAdd_eq_zero, twoTwoTailDihedralInversion,
226 ofAdd_neg, ofAdd_toAdd, twoTwoTailReflectionZero, twoTwoTailReflectionOne,
227 twoTwoTailRotation, mul_assoc, SemidirectProduct.mul_left,
228 SemidirectProduct.left_inr, SemidirectProduct.right_inr, MonoidHom.coe_mk,
229 OneHom.coe_mk, ofAdd_eq_one, one_ne_zero, ↓reduceIte,
230 SemidirectProduct.left_inl, SemidirectProduct.right_inl, MulEquiv.coe_mk,
231 Equiv.coe_fn_mk, one_mul, MulAut.one_apply, mul_inv_cancel, inv_one, mul_one,
232 toAdd_one, SemidirectProduct.one_left]
233 · simp only [twoTwoTailDihedralAction, twoTwoTailDihedralInversion,
234 ofAdd_neg, ofAdd_toAdd, twoTwoTailReflectionZero, twoTwoTailReflectionOne,
235 twoTwoTailRotation, mul_assoc, SemidirectProduct.mul_right,
236 SemidirectProduct.right_inr, SemidirectProduct.right_inl, mul_comm, one_mul,
237 toAdd_mul, toAdd_ofAdd, hsum, SemidirectProduct.one_right, toAdd_one]
239def twoTwoTailPeriods (n : ℕ) : Fin 3 → ℕ := fun i =>
240 if i.val = 0 then 2 else if i.val = 1 then 2 else n
242/-- The period family of `twoTwoTailSignature` is pointwise at least two. -/
243theorem twoTwoTailPeriods_ge_two {n : ℕ} (hn : 2 ≤ n) :
244 ∀ i : Fin 3, 2 ≤ twoTwoTailPeriods n i := by
245 intro i
246 fin_cases i
247 · simp only [twoTwoTailPeriods, ↓reduceIte, le_refl]
248 · simp only [twoTwoTailPeriods, one_ne_zero, ↓reduceIte, le_refl]
249 · simp only [twoTwoTailPeriods, OfNat.ofNat_ne_zero, ↓reduceIte, OfNat.ofNat_ne_one, hn]
251noncomputable def twoTwoTailSignature (n : ℕ) (hn : 2 ≤ n) :
252 FuchsianSignature where
253 orbitGenus := 0
254 numCusps := 0
255 numPeriods := 3
256 periods := twoTwoTailPeriods n
257 period_ge_two := twoTwoTailPeriods_ge_two hn
258 numCusps_eq_zero := rfl
259 numPeriods_ge_three := by norm_num
261noncomputable def twoTwoTailDihedralGeneratorImage {n : ℕ} (hn : 2 ≤ n) :
263 | .elliptic i =>
264 if i.val = 0 then
266 else if i.val = 1 then
268 else
270 | .surfaceA _ => 1
271 | .surfaceB _ => 1
273private theorem twoTwoTailDihedralGeneratorImage_respects_relators
274 {n : ℕ} (hn : 2 ≤ n) :
275 ∀ r ∈ relators (twoTwoTailSignature n hn),
276 FreeGroup.lift (twoTwoTailDihedralGeneratorImage hn) r = 1 := by
277 intro r hr
278 rcases hr with ⟨i, rfl⟩ | rfl
279 · fin_cases i
280 · simpa only [twoTwoTailSignature, xWord, Fin.reduceFinMk, Fin.isValue,
281 twoTwoTailPeriods, Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceIte, map_pow,
282 FreeGroup.lift_apply_of, twoTwoTailDihedralGeneratorImage] using
283 twoTwoTailReflectionZero_sq (n := n)
284 · simpa only [twoTwoTailSignature, xWord, Fin.reduceFinMk, Fin.isValue,
285 twoTwoTailPeriods, Fin.coe_ofNat_eq_mod, Nat.one_mod, one_ne_zero,
286 ↓reduceIte, map_pow, FreeGroup.lift_apply_of, twoTwoTailDihedralGeneratorImage] using
287 twoTwoTailReflectionOne_sq (n := n)
288 · simpa only [twoTwoTailSignature, xWord, Fin.reduceFinMk, Fin.isValue,
289 twoTwoTailPeriods, Fin.coe_ofNat_eq_mod, Nat.mod_succ, OfNat.ofNat_ne_zero,
290 ↓reduceIte, OfNat.ofNat_ne_one, map_pow, FreeGroup.lift_apply_of,
292 twoTwoTailRotation_pow_period (n := n)
293 · dsimp [totalRelation]
295 have hEll :
296 (List.map (⇑(FreeGroup.lift (twoTwoTailDihedralGeneratorImage hn)))
297 (List.map (fun i => xWord (twoTwoTailSignature n hn) i)
298 (List.finRange (twoTwoTailSignature n hn).numPeriods))).prod =
299 twoTwoTailReflectionZero n * twoTwoTailReflectionOne n * twoTwoTailRotation n := by
300 simpa [twoTwoTailSignature] using
301 (show
302 (List.map (⇑(FreeGroup.lift (twoTwoTailDihedralGeneratorImage hn)))
303 (List.map (fun i => xWord (twoTwoTailSignature n hn) i)
304 (List.finRange 3))).prod =
306 have hRange : List.finRange 3 = [0, 1, 2] := by
307 decide
308 rw [hRange]
309 have hNum : (twoTwoTailSignature n hn).numPeriods = 3 := by
310 rfl
312 twoTwoTailDihedralGeneratorImage, Fin.coe_ofNat_eq_mod, hNum, Nat.zero_mod, ↓reduceIte, twoTwoTailReflectionZero,
313 Nat.one_mod, one_ne_zero, twoTwoTailReflectionOne, Nat.mod_succ, OfNat.ofNat_ne_zero, OfNat.ofNat_ne_one,
314 twoTwoTailRotation, List.prod_cons, List.prod_nil, mul_one, mul_assoc])
315 have hComm :
316 (List.map (⇑(FreeGroup.lift (twoTwoTailDihedralGeneratorImage hn)))
317 (List.map (fun j => ⁅aWord (twoTwoTailSignature n hn) j,
318 bWord (twoTwoTailSignature n hn) j⁆)
319 (List.finRange (twoTwoTailSignature n hn).orbitGenus))).prod = 1 := by
320 rfl
321 rw [hEll, hComm, mul_one]
324noncomputable def twoTwoTailDihedralHom
325 {n : ℕ} (hn : 2 ≤ n) :
326 FuchsianPresentedGroup (twoTwoTailSignature n hn) →*
328 PresentedGroup.toGroup (rels := relators (twoTwoTailSignature n hn))
329 (f := twoTwoTailDihedralGeneratorImage hn)
332/-- The two-two-tail dihedral quotient is finite. -/
334 {n : ℕ} (hn : 2 ≤ n) :
335 Finite (TwoTwoTailDihedralQuotient n) := by
336 letI : NeZero n := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hn)⟩
337 letI : Fintype (ZMod n) := ZMod.fintype n
338 haveI : Fintype (Multiplicative (ZMod n)) := inferInstance
339 haveI : Fintype (Multiplicative (ZMod 2)) := inferInstance
340 exact Finite.of_injective
341 (fun q : TwoTwoTailDihedralQuotient n => (q.left, q.right))
342 (by
343 intro q r h
344 exact SemidirectProduct.ext (congrArg Prod.fst h) (congrArg Prod.snd h))
346/-- The two-two-tail dihedral quotient has derived length at most two. -/
348 (n : ℕ) :
349 derivedSeries (TwoTwoTailDihedralQuotient n) 2 = ⊥ := by
350 let ρ : TwoTwoTailDihedralQuotient n →* Multiplicative (ZMod 2) :=
351 SemidirectProduct.rightHom
352 have hfirst : derivedSeries (TwoTwoTailDihedralQuotient n) 1 ≤ ρ.ker := by
353 rw [derivedSeries_one]
354 exact Abelianization.commutator_subset_ker ρ
355 have hkerComm :
356 ⁅ρ.ker, ρ.ker⁆ = (⊥ : Subgroup (TwoTwoTailDihedralQuotient n)) := by
357 rw [Subgroup.commutator_eq_bot_iff_le_centralizer]
358 intro x hx
359 rw [Subgroup.mem_centralizer_iff]
360 intro y hy
361 have hxright : x.right = 1 := by
362 simpa [ρ] using MonoidHom.mem_ker.mp hx
363 have hyright : y.right = 1 := by
364 simpa [ρ] using MonoidHom.mem_ker.mp hy
365 ext
367 mul_comm, toAdd_mul, hxright]
368 · simp only [SemidirectProduct.mul_right, hyright, hxright, mul_one, toAdd_one]
369 apply le_antisymm
370 · calc
371 derivedSeries (TwoTwoTailDihedralQuotient n) 2 =
372 ⁅derivedSeries (TwoTwoTailDihedralQuotient n) 1,
373 derivedSeries (TwoTwoTailDihedralQuotient n) 1⁆ := by
374 change derivedSeries (TwoTwoTailDihedralQuotient n) (1 + 1) =
375 ⁅derivedSeries (TwoTwoTailDihedralQuotient n) 1,
376 derivedSeries (TwoTwoTailDihedralQuotient n) 1⁆
377 rw [derivedSeries_succ]
378 _ ≤ ⁅ρ.ker, ρ.ker⁆ := Subgroup.commutator_mono hfirst hfirst
379 _ = ⊥ := hkerComm
380 · exact bot_le
382noncomputable def finiteSolvableSmoothQuotientData_two_of_twoTwoTail
383 {n : ℕ} (hn : 2 ≤ n) :
384 FiniteSolvableSmoothQuotientData (twoTwoTailSignature n hn) 2 where
385 Q := TwoTwoTailDihedralQuotient n
387 φ := twoTwoTailDihedralHom hn
388 derived_length := twoTwoTailDihedralQuotient_derivedSeries_two_eq_bot n
389 elliptic_exact := by
390 intro i
391 fin_cases i
393 twoTwoTailSignature, twoTwoTailPeriods] using
396 twoTwoTailSignature, twoTwoTailPeriods] using
399 twoTwoTailSignature, twoTwoTailPeriods] using
402/-- Source-subgroup version of the low `[2,2,n]` first-reduction branch.
404 later paper-facing endpoint can still normalize the final subgroup if it is
405 needed. -/
406theorem FirstReductionPeriodData.sourceSubgroup_exists_of_two_two_tail_two
407 {σ : FuchsianSignature} (D : FirstReductionPeriodData σ)
408 (hm₁' : D.m₁' = 1) (hm₂' : D.m₂' = 1)
409 (hp_eq_two : D.p = 2) (hTailLen_eq_one : D.tailLen = 1) :
410 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
411 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
412 SubgroupQuotientHasDerivedLengthAtMost L 2 := by
413 classical
414 let k : Fin D.tailLen := ⟨0, by omega⟩
415 let n := D.tail k
416 have hn : 2 ≤ n := D.htail k
417 let τ := twoTwoTailSignature n hn
418 let eTarget : OriginalFirstReductionIndex D.tailLen ≃ Fin τ.numPeriods :=
419 (originalFirstReductionIndexEquivCanonicalSourceFin D.tailLen).trans
420 (finCongr (by simp only [twoTwoTailSignature, τ]; omega))
421 have hSourceEquiv :
422 Nonempty (FuchsianPresentedGroup D.sourceSignature ≃* FuchsianPresentedGroup τ) := by
423 refine
425 D.sourceSignature τ
426 (by rfl)
427 (by rfl)
428 (originalFirstReductionOrderedIndexEquiv D.tailLen)
429 eTarget ?_
430 intro x
431 cases x using Sum.casesOn with
432 | inl i =>
433 fin_cases i
434 · have hSource :
435 D.sourceSignature.periods
436 ((originalFirstReductionOrderedIndexEquiv D.tailLen) (.inl 0)) = 2 := by
437 simp only [sourceSignature, originalFirstReductionSignature, Fin.isValue,
438 originalFirstReductionOrderedIndexEquiv_left_zero, hp_eq_two, hm₁', originalFirstReductionSignaturePeriod_zero_fin,
439 mul_one]
440 have hTarget :
441 τ.periods (eTarget (.inl 0)) = 2 := by
442 rfl
443 exact hSource.trans hTarget.symm
444 · have hSource :
445 D.sourceSignature.periods
446 ((originalFirstReductionOrderedIndexEquiv D.tailLen) (.inl 1)) = 2 := by
447 simp only [sourceSignature, originalFirstReductionSignature, Fin.isValue,
448 originalFirstReductionOrderedIndexEquiv_left_one, hp_eq_two, hm₂', originalFirstReductionSignaturePeriod_one_fin,
449 mul_one]
450 have hTarget :
451 τ.periods (eTarget (.inl 1)) = 2 := by
452 rfl
453 exact hSource.trans hTarget.symm
454 | inr j =>
455 have hj : j = k := by
456 ext
457 omega
458 rw [hj]
459 have hSource :
460 D.sourceSignature.periods
461 ((originalFirstReductionOrderedIndexEquiv D.tailLen) (.inr k)) = n := by
463 simpa [FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature, k, n]
464 using
466 (p := D.p) D.m₁' D.m₂' D.tail k
467 have hTarget :
468 τ.periods (eTarget (.inr k)) = n := by
469 rfl
470 exact hSource.trans hTarget.symm
471 have hτ :
472 ∃ L : Subgroup (FuchsianPresentedGroup τ),
473 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
476 exact sourceSubgroup_exists_of_mulEquiv (Classical.choice hSourceEquiv) hτ
478end FenchelNielsen