FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/SourceSubgroup.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.Quotients
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.KernelEquivalence
3import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.LowCardDihedral
4import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.KernelEquivalence
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/SourceSubgroup.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
17Handles the cleanup of period-one target entries using quotient maps, kernel equivalences, low-cardinality dihedral cases, source subgroups, and relator proofs.
18-/
20namespace FenchelNielsen
22theorem SecondStageCleanupPeriodData.periodOne_of_not_strict
23 {σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
24 {secondPrime : FirstKernelTailPrimeDivisorData D}
25 (E : SecondStageCleanupPeriodData D secondPrime)
26 (hNonStrict : ¬ (2 ≤ D.m₁' ∧ 2 ≤ D.m₂' ∧ 2 ≤ E.m₃')) :
27 D.m₁' = 1 ∨ D.m₂' = 1 ∨ E.m₃' = 1 := by
28 by_cases hm₁ : 2 ≤ D.m₁'
29 · by_cases hm₂ : 2 ≤ D.m₂'
30 · by_cases hm₃ : 2 ≤ E.m₃'
31 · exact False.elim (hNonStrict ⟨hm₁, hm₂, hm₃⟩)
32 · right
33 right
34 have hpos : 0 < E.m₃' := E.hm₃'
35 omega
36 · right
37 left
38 have hpos : 0 < D.m₂' := D.hm₂'
39 omega
40 · left
41 have hpos : 0 < D.m₁' := D.hm₁'
42 omega
44private theorem originalFirstReduction_doublePeriodOne_sourceSubgroup_exists
45 {tailLen p : ℕ} (tail : Fin tailLen → ℕ)
46 (hp : 2 ≤ p) (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
47 ∃ L : Subgroup
49 (originalFirstReductionSignature 1 1 tail hp (by norm_num) (by norm_num)
50 htail hTailLen)),
51 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
52 SubgroupQuotientHasDerivedLengthAtMost L 2 := by
53 classical
54 let source :=
55 originalFirstReductionSignature 1 1 tail hp (by norm_num) (by norm_num)
56 htail hTailLen
57 by_cases hHigh : 3 ≤ p * tailLen
58 · let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
59 have hTargetSubgroup :
60 ∃ L : Subgroup (FuchsianPresentedGroup target),
61 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
64 target (m := 1) (by norm_num)
65 (doublePeriodOneTailReplicatedSignature_lcmCondition tail htail hHigh hp)
66 let eIdx := originalFirstReductionOrderedIndexEquiv tailLen
67 have hperiods :
68 ∀ x : OriginalFirstReductionIndex tailLen,
69 source.periods (eIdx x) =
70 originalFirstReductionPeriods (p := p) 1 1 tail x := by
71 intro x
72 simpa [source, eIdx] using
74 1 1 tail hp (by norm_num) (by norm_num) htail hTailLen x
75 let φ :=
77 1 1 tail hp (by norm_num) (by norm_num) htail hTailLen
78 let eKernel :
79 φ.ker ≃* FuchsianPresentedGroup target := by
80 simpa [φ, source, target, eIdx, originalFirstReductionPeriodOneQuotientHom] using
82 1 1 tail hp (by norm_num) (by norm_num) htail hTailLen
83 hHigh eIdx hperiods rfl rfl rfl
85 1 1 tail hp (by norm_num) (by norm_num) htail hTailLen
86 hHigh eIdx hperiods rfl rfl rfl)
87 letI : NeZero p :=
88 ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
89 letI : Fintype (ZMod p) := ZMod.fintype p
90 letI : Fintype (Multiplicative (ZMod p)) := inferInstance
91 haveI : Finite (Multiplicative (ZMod p)) :=
92 Finite.of_fintype (Multiplicative (ZMod p))
93 simpa [source, φ] using
95 φ eKernel hTargetSubgroup
96 · have hMin : p = 2 ∧ tailLen = 1 :=
97 firstReductionTransportPeriodsFin_tail_low_card_eq_two hp hTailLen hHigh
98 let k : Fin tailLen := ⟨0, by omega⟩
99 let n := tail k
100 have hn : 2 ≤ n := htail k
101 let τ := twoTwoTailSignature n hn
102 let eTarget : OriginalFirstReductionIndex tailLen ≃ Fin τ.numPeriods :=
103 (originalFirstReductionIndexEquivCanonicalSourceFin tailLen).trans
104 (finCongr (by simp only [twoTwoTailSignature, τ]; omega))
105 have hSourceEquiv :
106 Nonempty (FuchsianPresentedGroup source ≃* FuchsianPresentedGroup τ) := by
107 refine
109 source τ
110 (by simp only [originalFirstReductionSignature, source])
111 (by simp only [twoTwoTailSignature, τ])
112 (originalFirstReductionOrderedIndexEquiv tailLen)
113 eTarget ?_
114 intro x
115 cases x using Sum.casesOn with
116 | inl i =>
117 fin_cases i
118 · have hSource :
119 source.periods
120 ((originalFirstReductionOrderedIndexEquiv tailLen) (.inl 0)) = 2 := by
121 simp only [originalFirstReductionSignature, Fin.isValue, originalFirstReductionOrderedIndexEquiv_left_zero,
122 hMin.1, originalFirstReductionSignaturePeriod_zero_fin, mul_one, source]
123 have hTarget :
124 τ.periods (eTarget (.inl 0)) = 2 := by
125 simp only [twoTwoTailSignature, originalFirstReductionIndexEquivCanonicalSourceFin, Equiv.sumCongr_refl,
126 Equiv.refl_trans, Fin.isValue, Equiv.trans_apply, finSumFinEquiv_apply_left, finCongr_apply, twoTwoTailPeriods,
127 Fin.val_cast, Fin.val_castAdd, Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceIte, eTarget, τ]
128 exact hSource.trans hTarget.symm
129 · have hSource :
130 source.periods
131 ((originalFirstReductionOrderedIndexEquiv tailLen) (.inl 1)) = 2 := by
132 simp only [originalFirstReductionSignature, Fin.isValue, originalFirstReductionOrderedIndexEquiv_left_one,
133 hMin.1, originalFirstReductionSignaturePeriod_one_fin, mul_one, source]
134 have hTarget :
135 τ.periods (eTarget (.inl 1)) = 2 := by
136 simp only [twoTwoTailSignature, originalFirstReductionIndexEquivCanonicalSourceFin, Equiv.sumCongr_refl,
137 Equiv.refl_trans, Fin.isValue, Equiv.trans_apply, finSumFinEquiv_apply_left, finCongr_apply, twoTwoTailPeriods,
138 Fin.val_cast, Fin.val_castAdd, Fin.coe_ofNat_eq_mod, Nat.mod_succ, one_ne_zero, ↓reduceIte, eTarget, τ]
139 exact hSource.trans hTarget.symm
140 | inr j =>
141 have hj : j = k := by
142 ext
143 omega
144 rw [hj]
145 have hSource :
146 source.periods
147 ((originalFirstReductionOrderedIndexEquiv tailLen) (.inr k)) = n := by
149 simpa [source, originalFirstReductionSignature, k, n] using
151 (p := p) 1 1 tail k
152 have hTarget :
153 τ.periods (eTarget (.inr k)) = n := by
154 simp only [twoTwoTailSignature, originalFirstReductionIndexEquivCanonicalSourceFin, Equiv.sumCongr_refl,
155 Equiv.refl_trans, Equiv.trans_apply, finSumFinEquiv_apply_right, Fin.natAdd_mk, add_zero, finCongr_apply,
156 Fin.cast_mk, Fin.reduceFinMk, twoTwoTailPeriods, Fin.isValue, Fin.coe_ofNat_eq_mod, Nat.mod_succ,
157 OfNat.ofNat_ne_zero, ↓reduceIte, OfNat.ofNat_ne_one, n, k, eTarget, τ]
158 exact hSource.trans hTarget.symm
159 have hτ :
160 ∃ L : Subgroup (FuchsianPresentedGroup τ),
161 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
164 exact sourceSubgroup_exists_of_mulEquiv (Classical.choice hSourceEquiv) hτ
166private theorem oneHeadPeriodOneTarget_sourceSubgroup_exists_by_tailPair
167 {tailLen p : ℕ} (m₂' : ℕ) (tail : Fin tailLen → ℕ)
168 (hp : 2 ≤ p) (hm₂' : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
169 (hTailLen : 0 < tailLen) :
170 ∃ L : Subgroup
172 (oneHeadPeriodOneTargetSignature m₂' tail hp hm₂' htail hTailLen)),
173 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
174 SubgroupQuotientHasDerivedLengthAtMost L 2 := by
175 classical
176 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂' htail hTailLen
177 let idx := OneHeadPeriodOneTargetIndex tailLen p
178 let j₀ : Fin tailLen := ⟨0, hTailLen⟩
179 let k₀ : Fin p := finZeroOfTwoLe hp
180 let k₁ : Fin p := finPartner hp k₀
181 let pos : idx := .inr (k₀, j₀)
184 intro h
185 have hk : k₁ = k₀ := by
186 exact (congrArg Prod.fst (Sum.inr.inj h)).symm
187 exact finPartner_ne hp k₀ hk
189 let restLen := Fintype.card restSubtype
190 let reidx : OriginalFirstReductionIndex restLen ≃ idx :=
191 originalFirstReductionReindex pos neg hposneg
192 let restPeriods : Fin restLen → ℕ := fun r =>
193 oneHeadPeriodOneTargetPeriods (p := p) m₂' tail (reidx (.inr r))
194 have hRestLen : 0 < restLen := by
195 have hnePos : (Sum.inl (0 : Fin 1) : idx) ≠ pos := by
196 change (Sum.inl (0 : Fin 1) : idx) ≠ Sum.inr (k₀, j₀)
197 intro h
198 cases h
200 change (Sum.inl (0 : Fin 1) : idx) ≠ Sum.inr (k₁, j₀)
201 intro h
202 cases h
203 have hnonempty : Nonempty restSubtype :=
204 ⟨⟨(Sum.inl (0 : Fin 1) : idx), hnePos, hneNeg⟩⟩
205 simpa [restLen] using (Fintype.card_pos_iff.mpr hnonempty)
206 have hrest : ∀ r : Fin restLen, 2 ≤ restPeriods r := by
207 intro r
208 dsimp [restPeriods]
209 cases h : reidx (.inr r) with
210 | inl head =>
211 fin_cases head
212 simpa [oneHeadPeriodOneTargetPeriods] using hm₂'
213 | inr kj =>
214 simpa [oneHeadPeriodOneTargetPeriods] using htail kj.2
215 let q := tail j₀
216 have hq : 2 ≤ q := htail j₀
217 let source :=
218 originalFirstReductionSignature 1 1 restPeriods hq (by norm_num) (by norm_num)
219 hrest hRestLen
220 have hSourceSubgroup :
221 ∃ L : Subgroup (FuchsianPresentedGroup source),
222 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
225 restPeriods hq hrest hRestLen
226 have hTargetEquiv :
227 Nonempty (FuchsianPresentedGroup target ≃* FuchsianPresentedGroup source) := by
228 refine
230 target source
231 (by simp only [oneHeadPeriodOneTargetSignature, target])
232 (by simp only [originalFirstReductionSignature, source])
233 (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p)
234 (reidx.symm.trans (originalFirstReductionOrderedIndexEquiv restLen)) ?_
235 intro x
236 have hsourcePeriod :
237 source.periods
238 ((reidx.symm.trans (originalFirstReductionOrderedIndexEquiv restLen)) x) =
239 originalFirstReductionPeriods (p := q) 1 1 restPeriods (reidx.symm x) := by
240 simpa [source] using
242 1 1 restPeriods hq (by norm_num) (by norm_num) hrest hRestLen
243 (reidx.symm x)
244 calc
245 target.periods ((oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p) x) =
246 originalFirstReductionPeriods (p := q) 1 1 restPeriods (reidx.symm x) := by
247 generalize hy : reidx.symm x = y
248 have hx : x = reidx y := by
249 rw [← hy]
250 simp only [Equiv.apply_symm_apply]
251 cases y using Sum.casesOn with
252 | inl head =>
253 fin_cases head
254 · subst hx
255 have htarget :
256 target.periods (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p pos) = q := by
257 simp only [oneHeadPeriodOneTargetSignature, oneHeadPeriodOneTargetPeriods, Equiv.symm_apply_apply, pos, q,
258 target]
259 simpa [originalFirstReductionPeriods, twoPeriods] using htarget
260 · subst hx
261 have htarget :
262 target.periods (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p neg) = q := by
263 simp only [oneHeadPeriodOneTargetSignature, oneHeadPeriodOneTargetPeriods, Equiv.symm_apply_apply, neg, q,
264 target]
265 simpa [originalFirstReductionPeriods, twoPeriods] using htarget
266 | inr r =>
267 subst hx
268 have htarget :
269 target.periods (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p (reidx (.inr r))) =
270 restPeriods r := by
271 simp only [oneHeadPeriodOneTargetSignature, Equiv.symm_apply_apply, restPeriods, target]
272 simpa [originalFirstReductionPeriods] using htarget
273 _ = source.periods
274 ((reidx.symm.trans (originalFirstReductionOrderedIndexEquiv restLen)) x) :=
275 hsourcePeriod.symm
276 exact sourceSubgroup_exists_of_mulEquiv (Classical.choice hTargetEquiv) hSourceSubgroup
278private theorem firstReductionCanonicalTarget_periods_eq
279 {tailLen p : ℕ}
280 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
281 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
282 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
283 (x : FirstReductionIndex tailLen p) :
285 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
286 (firstReductionIndexEquivCanonicalTargetFin tailLen p x) =
287 firstReductionPeriods (p := p) m₁' m₂' tail x := by
288 classical
289 cases x using Sum.casesOn with
290 | inl head =>
291 fin_cases head
292 · simpa [firstReductionCanonicalTargetZeroIndex,
294 firstReductionPeriods, twoPeriods] using
296 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
297 · simpa [firstReductionCanonicalTargetOneIndex,
299 firstReductionPeriods, twoPeriods] using
301 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
302 | inr jk =>
303 rcases jk with ⟨j, k⟩
305 firstReductionIndexEquivCanonicalTargetFin, finProdFinEquiv,
306 Nat.add_assoc, Nat.add_comm, Nat.mul_comm,
307 firstReductionPeriods] using
309 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j
312 {tailLen p : ℕ}
313 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
314 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
315 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
316 ∃ L : Subgroup
319 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)),
320 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
321 SubgroupQuotientHasDerivedLengthAtMost L 2 := by
322 classical
323 let target :=
325 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
326 let idx := FirstReductionIndex tailLen p
327 let j₀ : Fin tailLen := ⟨0, hTailLen⟩
328 let k₀ : Fin p := finZeroOfTwoLe hp
329 let k₁ : Fin p := finPartner hp k₀
330 let pos : idx := .inr (j₀, k₀)
333 intro h
334 have hk : k₁ = k₀ := by
335 exact (congrArg Prod.snd (Sum.inr.inj h)).symm
336 exact finPartner_ne hp k₀ hk
338 let restLen := Fintype.card restSubtype
339 let reidx : OriginalFirstReductionIndex restLen ≃ idx :=
340 originalFirstReductionReindex pos neg hposneg
341 let restPeriods : Fin restLen → ℕ := fun r =>
342 firstReductionPeriods (p := p) m₁' m₂' tail (reidx (.inr r))
343 have hRestLen : 0 < restLen := by
344 have hnePos : (Sum.inl (0 : Fin 2) : idx) ≠ pos := by
345 change (Sum.inl (0 : Fin 2) : idx) ≠ Sum.inr (j₀, k₀)
346 intro h
347 cases h
349 change (Sum.inl (0 : Fin 2) : idx) ≠ Sum.inr (j₀, k₁)
350 intro h
351 cases h
352 have hnonempty : Nonempty restSubtype :=
353 ⟨⟨(Sum.inl (0 : Fin 2) : idx), hnePos, hneNeg⟩⟩
354 simpa [restLen] using (Fintype.card_pos_iff.mpr hnonempty)
355 have hrest : ∀ r : Fin restLen, 2 ≤ restPeriods r := by
356 intro r
357 dsimp [restPeriods]
358 cases h : reidx (.inr r) with
359 | inl head =>
360 fin_cases head
361 · simpa [firstReductionPeriods, twoPeriods] using hm₁'
362 · simpa [firstReductionPeriods, twoPeriods] using hm₂'
363 | inr jk =>
364 simpa [firstReductionPeriods] using htail jk.1
365 let q := tail j₀
366 have hq : 2 ≤ q := htail j₀
367 let source :=
368 originalFirstReductionSignature 1 1 restPeriods hq (by norm_num) (by norm_num)
369 hrest hRestLen
370 have hSourceSubgroup :
371 ∃ L : Subgroup (FuchsianPresentedGroup source),
372 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
375 restPeriods hq hrest hRestLen
376 have hTargetEquiv :
377 Nonempty (FuchsianPresentedGroup target ≃* FuchsianPresentedGroup source) := by
378 refine
380 target source
381 (by simp only [firstReductionCanonicalTargetSignature, target])
382 (by simp only [originalFirstReductionSignature, source])
383 (firstReductionIndexEquivCanonicalTargetFin tailLen p)
384 (reidx.symm.trans (originalFirstReductionOrderedIndexEquiv restLen)) ?_
385 intro x
386 have hsourcePeriod :
387 source.periods
388 ((reidx.symm.trans (originalFirstReductionOrderedIndexEquiv restLen)) x) =
389 originalFirstReductionPeriods (p := q) 1 1 restPeriods (reidx.symm x) := by
390 simpa [source] using
392 1 1 restPeriods hq (by norm_num) (by norm_num) hrest hRestLen
393 (reidx.symm x)
394 calc
395 target.periods (firstReductionIndexEquivCanonicalTargetFin tailLen p x) =
396 originalFirstReductionPeriods (p := q) 1 1 restPeriods (reidx.symm x) := by
397 generalize hy : reidx.symm x = y
398 have hx : x = reidx y := by
399 rw [← hy]
400 simp only [Equiv.apply_symm_apply]
401 cases y using Sum.casesOn with
402 | inl head =>
403 fin_cases head
404 · subst hx
405 have htarget :
406 target.periods (firstReductionIndexEquivCanonicalTargetFin tailLen p pos) = q := by
407 simpa [target, q, pos] using
409 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen pos
410 simpa [originalFirstReductionPeriods, twoPeriods] using htarget
411 · subst hx
412 have htarget :
413 target.periods (firstReductionIndexEquivCanonicalTargetFin tailLen p neg) = q := by
417 simpa [originalFirstReductionPeriods, twoPeriods] using htarget
418 | inr r =>
419 subst hx
420 have htarget :
421 target.periods
422 (firstReductionIndexEquivCanonicalTargetFin tailLen p (reidx (.inr r))) =
423 restPeriods r := by
424 simpa [target, restPeriods] using
426 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen (reidx (.inr r))
427 simpa [originalFirstReductionPeriods] using htarget
428 _ = source.periods
429 ((reidx.symm.trans (originalFirstReductionOrderedIndexEquiv restLen)) x) :=
430 hsourcePeriod.symm
431 exact sourceSubgroup_exists_of_mulEquiv (Classical.choice hTargetEquiv) hSourceSubgroup
434 {σ : FuchsianSignature}
435 (D : FirstReductionPeriodData σ)
436 (hm₁' : D.m₁' = 1) :
437 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
438 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
439 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
440 classical
441 by_cases hSourceBoundTwo :
442 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
443 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
445 · exact
447 (G := FuchsianPresentedGroup D.sourceSignature) (m := 2) (n := 3)
448 (by norm_num) hSourceBoundTwo
449 · have hSourceNotLCM : ¬ LCMCondition D.sourceSignature.toFenchelSignature := by
450 intro hLCM
451 exact hSourceBoundTwo
453 D.sourceSignature (m := 2) (by norm_num) hLCM)
454 have hPeriodOneQuotientData :
455 ∃ φ : FuchsianPresentedGroup D.sourceSignature →* Multiplicative (ZMod D.p),
456 φ.ker.FiniteIndex ∧
457 φ (ellipticElement D.sourceSignature
458 ((originalFirstReductionOrderedIndexEquiv D.tailLen)
459 (.inl (0 : Fin 2)))) =
460 Multiplicative.ofAdd (1 : ZMod D.p) ∧
461 φ (ellipticElement D.sourceSignature
462 ((originalFirstReductionOrderedIndexEquiv D.tailLen)
463 (.inl (1 : Fin 2)))) =
464 Multiplicative.ofAdd (-1 : ZMod D.p) ∧
465 (∀ j : Fin D.tailLen,
466 φ (ellipticElement D.sourceSignature
467 ((originalFirstReductionOrderedIndexEquiv D.tailLen)
468 (.inr j))) = 1) := by
469 let φ₀ :=
471 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
472 let φ : FuchsianPresentedGroup D.sourceSignature →* Multiplicative (ZMod D.p) := by
473 simpa [FirstReductionPeriodData.sourceSignature] using φ₀
474 refine ⟨φ, ?_, ?_, ?_, ?_⟩
475 letI : NeZero D.p :=
476 ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) D.hp)⟩
477 letI : Fintype (ZMod D.p) := ZMod.fintype D.p
478 letI : Fintype (Multiplicative (ZMod D.p)) := inferInstance
479 haveI : Finite (Multiplicative (ZMod D.p)) :=
480 Finite.of_fintype (Multiplicative (ZMod D.p))
481 · exact Subgroup.finiteIndex_ker φ
482 · simpa [φ, FirstReductionPeriodData.sourceSignature] using
484 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
485 · simpa [φ, FirstReductionPeriodData.sourceSignature] using
487 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
488 · intro j
489 simpa [φ, FirstReductionPeriodData.sourceSignature] using
491 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen j
492 have hSecondHeadShape : D.m₂' = 1 ∨ 2 ≤ D.m₂' := by
493 by_cases hm₂one : D.m₂' = 1
494 · exact Or.inl hm₂one
495 · have hpos : 0 < D.m₂' := D.hm₂'
496 exact Or.inr (by omega)
497 rcases hSecondHeadShape with hm₂one | hm₂ge
498 · by_cases hHighDouble : 3 ≤ D.p * D.tailLen
499 · have hSourceLCMObstruction :=
501 D.sourceSignature.toFenchelSignature hSourceNotLCM
502 have hDroppedDoubleTargetSubgroup :
503 ∃ L : Subgroup
506 D.tail D.htail hHighDouble)),
507 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
510 (doublePeriodOneTailReplicatedSignature D.tail D.htail hHighDouble)
511 (m := 1) (by norm_num)
513 D.tail D.htail hHighDouble D.hp)
514 -- FRONTIER(period-one-left-high-double-residual): both divided heads
515 -- are period one, the double-period-one tail has high cardinality,
516 -- the exact `≤ 2` source-subgroup route has failed, and the source-LCM
517 -- smooth quotient route is impossible by `hSourceNotLCM`. The repeated
518 -- tail target produced by dropping the period-one heads is now closed by
519 -- the LCM smooth quotient route, while the source itself carries the
520 -- displayed LCM obstruction `hSourceLCMObstruction`; what remains is the cyclic kernel
521 -- transport from this repeated-tail target back to `D.sourceSignature`.
522 -- The remaining task is the public `≤ 3` source-subgroup statement, not
523 -- a cleaned presentation theorem.
524 let source :=
526 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
527 let target :=
528 doublePeriodOneTailReplicatedSignature D.tail D.htail hHighDouble
529 let eIdx := originalFirstReductionOrderedIndexEquiv D.tailLen
530 have hperiods :
531 ∀ x : OriginalFirstReductionIndex D.tailLen,
532 source.periods (eIdx x) =
533 originalFirstReductionPeriods (p := D.p) D.m₁' D.m₂' D.tail x := by
534 intro x
535 simpa [source, eIdx] using
537 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen x
538 let φ :=
540 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
541 let eKernel :
542 φ.ker ≃* FuchsianPresentedGroup target := by
543 simpa [φ, source, target, eIdx, originalFirstReductionPeriodOneQuotientHom] using
545 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
546 hHighDouble eIdx hperiods rfl hm₁' hm₂one
548 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
549 hHighDouble eIdx hperiods rfl hm₁' hm₂one)
550 letI : NeZero D.p :=
551 ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) D.hp)⟩
552 letI : Fintype (ZMod D.p) := ZMod.fintype D.p
553 letI : Fintype (Multiplicative (ZMod D.p)) := inferInstance
554 haveI : Finite (Multiplicative (ZMod D.p)) :=
555 Finite.of_fintype (Multiplicative (ZMod D.p))
556 have hSourceBoundTwo' :
557 ∃ L : Subgroup (FuchsianPresentedGroup source),
558 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
559 SubgroupQuotientHasDerivedLengthAtMost L 2 := by
560 simpa [target, φ] using
562 φ eKernel hDroppedDoubleTargetSubgroup
563 have hSourceBoundThree' :
564 ∃ L : Subgroup (FuchsianPresentedGroup source),
565 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
568 (G := FuchsianPresentedGroup source) (m := 2) (n := 3)
569 (by norm_num) hSourceBoundTwo'
570 simpa [source, FirstReductionPeriodData.sourceSignature] using hSourceBoundThree'
571 · have hMin : D.p = 2 ∧ D.tailLen = 1 :=
573 D.hp D.hTailLen hHighDouble
574 have hLowSubgroupTwo :
575 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
576 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
578 D.sourceSubgroup_exists_of_two_two_tail_two hm₁' hm₂one hMin.1 hMin.2
579 exact
581 (G := FuchsianPresentedGroup D.sourceSignature) (m := 2) (n := 3)
582 (by norm_num) hLowSubgroupTwo
583 · have hSourceLCMObstruction :=
585 D.sourceSignature.toFenchelSignature hSourceNotLCM
586 let droppedHeadTarget :=
587 oneHeadPeriodOneTargetSignature D.m₂' D.tail D.hp hm₂ge D.htail D.hTailLen
588 have hDroppedHeadTargetSubgroup :
589 ∃ L : Subgroup (FuchsianPresentedGroup droppedHeadTarget),
590 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
591 SubgroupQuotientHasDerivedLengthAtMost L 2 := by
592 simpa [droppedHeadTarget] using
594 D.m₂' D.tail D.hp hm₂ge D.htail D.hTailLen
595 let source :=
597 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
598 let target :=
599 oneHeadPeriodOneTargetSignature D.m₂' D.tail D.hp hm₂ge D.htail D.hTailLen
600 let eIdx := originalFirstReductionOrderedIndexEquiv D.tailLen
601 have hperiods :
602 ∀ x : OriginalFirstReductionIndex D.tailLen,
603 source.periods (eIdx x) =
604 originalFirstReductionPeriods (p := D.p) D.m₁' D.m₂' D.tail x := by
605 intro x
606 simpa [source, eIdx] using
608 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen x
609 let φ :=
611 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' D.htail D.hTailLen
612 let eKernel :
613 φ.ker ≃* FuchsianPresentedGroup target := by
614 simpa [φ, source, target, eIdx, originalFirstReductionPeriodOneQuotientHom] using
616 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' hm₂ge D.htail D.hTailLen
617 eIdx hperiods rfl hm₁'
619 D.m₁' D.m₂' D.tail D.hp D.hm₁' D.hm₂' hm₂ge D.htail D.hTailLen
620 eIdx hperiods rfl hm₁')
621 letI : NeZero D.p :=
622 ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) D.hp)⟩
623 letI : Fintype (ZMod D.p) := ZMod.fintype D.p
624 letI : Fintype (Multiplicative (ZMod D.p)) := inferInstance
625 haveI : Finite (Multiplicative (ZMod D.p)) :=
626 Finite.of_fintype (Multiplicative (ZMod D.p))
627 have hSourceBoundThree' :
628 ∃ L : Subgroup (FuchsianPresentedGroup source),
629 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
630 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
631 simpa [target, φ, droppedHeadTarget] using
633 φ eKernel hDroppedHeadTargetSubgroup
634 simpa [source, FirstReductionPeriodData.sourceSignature] using hSourceBoundThree'
636 {σ : FuchsianSignature}
637 (D : FirstReductionPeriodData σ)
638 (hm₂' : D.m₂' = 1) :
639 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
640 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
641 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
642 classical
643 let headSwap : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
644 let sourceSwap : OriginalFirstReductionIndex D.tailLen ≃
645 OriginalFirstReductionIndex D.tailLen :=
646 Equiv.sumCongr headSwap (Equiv.refl (Fin D.tailLen))
647 let Dswap : FirstReductionPeriodData D.sourceSignature :=
648 { p := D.p
649 hpPrime := D.hpPrime
650 hp := D.hp
651 tailLen := D.tailLen
652 m₁' := D.m₂'
653 m₂' := D.m₁'
654 tail := D.tail
655 hm₁' := D.hm₂'
656 hm₂' := D.hm₁'
657 htail := D.htail
658 hTailLen := D.hTailLen
659 reindex := sourceSwap.trans (originalFirstReductionOrderedIndexEquiv D.tailLen)
660 periods_eq := by
661 intro x
662 cases x using Sum.casesOn with
663 | inl i =>
664 fin_cases i
665 · simp [originalFirstReductionPeriods, twoPeriods,
666 FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature,
667 Equiv.trans_apply, sourceSwap, headSwap]
668 · simp [originalFirstReductionPeriods, twoPeriods,
669 FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature,
670 Equiv.trans_apply, sourceSwap, headSwap]
671 | inr j =>
672 simp only [originalFirstReductionPeriods, FirstReductionPeriodData.sourceSignature,
673 originalFirstReductionSignature, Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, id_eq,
674 originalFirstReductionOrderedIndexEquiv_right, originalFirstReductionSignaturePeriod_tail, sourceSwap]}
675 let e :
676 FuchsianPresentedGroup D.sourceSignature ≃*
677 FuchsianPresentedGroup Dswap.sourceSignature :=
678 Classical.choice
679 (firstReductionSourceMulEquiv_exists Dswap (by
680 simp only [FirstReductionPeriodData.sourceSignature, originalFirstReductionSignature]))
681 exact
683 (firstReductionSourceSubgroup_leftPeriodOne_exists Dswap hm₂')
685private theorem SecondStageCleanupPeriodData.sourceSubgroup_exists_of_tailPair
686 {σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
687 {secondPrime : FirstKernelTailPrimeDivisorData D}
688 (E : SecondStageCleanupPeriodData D secondPrime)
689 (hm₁' : 2 ≤ D.m₁') (hm₂' : 2 ≤ D.m₂') :
690 ∃ L : Subgroup (FuchsianPresentedGroup E.sourceSignature),
691 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
692 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
693 let sourceTail :=
695 secondPrime.hqPrime.two_le E.m₃' E.tail E.hm₃' E.htail
696 let canonicalSource :=
697 firstReductionCanonicalSourceSignature D.m₁' D.m₂'
698 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
699 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)
700 have hCanonicalSubgroup :
701 ∃ L : Subgroup (FuchsianPresentedGroup canonicalSource),
702 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
703 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
704 by_cases hCanonicalBoundTwo :
705 ∃ L : Subgroup (FuchsianPresentedGroup canonicalSource),
706 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
708 · exact
710 (G := FuchsianPresentedGroup canonicalSource) (m := 2) (n := 3)
711 (by norm_num) hCanonicalBoundTwo
712 · by_cases hCanonicalLCM : LCMCondition canonicalSource.toFenchelSignature
713 · exact
715 canonicalSource (m := 3) (by norm_num) hCanonicalLCM
716 · let target :=
717 firstReductionCanonicalTargetSignature D.m₁' D.m₂'
718 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
719 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)
720 have hTargetSubgroup :
721 ∃ L : Subgroup (FuchsianPresentedGroup target),
722 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
725 D.m₁' D.m₂'
726 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
727 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)
728 let φ :=
729 firstReductionCanonicalSourceQuotientHom D.m₁' D.m₂'
730 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
731 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)
732 let eKernel :
733 φ.ker ≃* FuchsianPresentedGroup target := by
734 simpa [φ, target] using
736 D.m₁' D.m₂'
737 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
738 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)
739 letI : NeZero D.p :=
740 ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) D.hp)⟩
741 letI : Fintype (ZMod D.p) := ZMod.fintype D.p
742 letI : Fintype (Multiplicative (ZMod D.p)) := inferInstance
743 haveI : Finite (Multiplicative (ZMod D.p)) :=
744 Finite.of_fintype (Multiplicative (ZMod D.p))
745 simpa [canonicalSource, φ, target] using
747 φ eKernel hTargetSubgroup
748 let eSourceCanonical :
749 FuchsianPresentedGroup E.sourceSignature ≃*
750 FuchsianPresentedGroup canonicalSource := by
751 simpa [canonicalSource, sourceTail, SecondStageCleanupPeriodData.sourceSignature,
752 firstReductionSourceSignature] using
753 (Classical.choice
755 D.m₁' D.m₂'
756 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
757 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)))
758 exact sourceSubgroup_exists_of_mulEquiv eSourceCanonical hCanonicalSubgroup
761 {σ : FuchsianSignature}
762 (D : FirstReductionPeriodData σ)
763 (_hquot : D.tail D.tailPrimeDivisorData.k / D.tailPrimeDivisorData.q = 1) :
764 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
765 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
766 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
767 classical
768 let secondPrime : FirstKernelTailPrimeDivisorData D := D.tailPrimeDivisorData
769 by_cases hSourceBoundTwo :
770 ∃ L : Subgroup (FuchsianPresentedGroup D.sourceSignature),
771 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
773 · exact
775 (G := FuchsianPresentedGroup D.sourceSignature) (m := 2) (n := 3)
776 (by norm_num) hSourceBoundTwo
777 · have hSourceNotLCM : ¬ LCMCondition D.sourceSignature.toFenchelSignature := by
778 intro hLCM
779 exact hSourceBoundTwo
781 D.sourceSignature (m := 2) (by norm_num) hLCM)
782 by_cases hm₁' : D.m₁' = 1
783 · exact firstReductionSourceSubgroup_leftPeriodOne_exists D hm₁'
784 · by_cases hm₂' : D.m₂' = 1
785 · exact firstReductionSourceSubgroup_rightPeriodOne_exists D hm₂'
786 · have hm₁'ge : 2 ≤ D.m₁' := by
787 have hpos : 0 < D.m₁' := D.hm₁'
788 omega
789 have hm₂'ge : 2 ≤ D.m₂' := by
790 have hpos : 0 < D.m₂' := D.hm₂'
791 omega
792 let E : SecondStageCleanupPeriodData D secondPrime :=
793 secondStageCleanupPeriodDataOfTailPrime D secondPrime
794 have hESourceSubgroup :
795 ∃ L : Subgroup (FuchsianPresentedGroup E.sourceSignature),
796 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
798 SecondStageCleanupPeriodData.sourceSubgroup_exists_of_tailPair E hm₁'ge hm₂'ge
799 let eOuter :
800 FuchsianPresentedGroup D.sourceSignature ≃*
801 FuchsianPresentedGroup E.sourceSignature :=
802 Classical.choice (secondStageCleanupSourceMulEquiv_exists E)
803 exact sourceSubgroup_exists_of_mulEquiv eOuter hESourceSubgroup
806/-- Source-subgroup form of the strict two-stage branch. This is the form
807 actually needed before the final paper-facing normal core is taken: the
809 subgroups, not local normality. -/
810theorem SecondStageCleanupPeriodData.sourceSubgroup_exists_of_canonicalReductions
811 {σ : FuchsianSignature} {D : FirstReductionPeriodData σ}
812 {secondPrime : FirstKernelTailPrimeDivisorData D}
813 (E : SecondStageCleanupPeriodData D secondPrime)
814 (hm₁' : 2 ≤ D.m₁') (hm₂' : 2 ≤ D.m₂') (hm₃' : 2 ≤ E.m₃') :
815 ∃ L : Subgroup (FuchsianPresentedGroup E.sourceSignature),
816 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
817 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
818 let sourceTail :=
820 secondPrime.hqPrime.two_le E.m₃' E.tail E.hm₃' E.htail
821 let canonicalSource :=
822 firstReductionCanonicalSourceSignature D.m₁' D.m₂'
823 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
824 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)
825 have hCanonicalSubgroup :
826 ∃ L : Subgroup (FuchsianPresentedGroup canonicalSource),
827 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
828 SubgroupQuotientHasDerivedLengthAtMost L 3 := by
829 let target :=
830 secondReductionTransportSignature (p := D.p) secondPrime.hqPrime.two_le
831 D.m₁' D.m₂' E.m₃' E.tail hm₁' hm₂' hm₃' E.htail
832 rcases
834 D.m₁' D.m₂' E.m₃' E.tail D.hp secondPrime.hqPrime.two_le
835 hm₁' hm₂' hm₃' E.htail with
836 ⟨eΨ⟩
837 have hMiddleSubgroup :
838 ∃ L : Subgroup
841 D.m₁' D.m₂' E.m₃' E.tail D.hp secondPrime.hqPrime.two_le
842 hm₁' hm₂' hm₃' E.htail)),
843 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
844 SubgroupQuotientHasDerivedLengthAtMost L 2 := by
845 let ψ :=
847 D.m₁' D.m₂' E.m₃' E.tail D.hp secondPrime.hqPrime.two_le
848 hm₁' hm₂' hm₃' E.htail
850 target
852 (p := D.p) secondPrime.hqPrime.two_le
853 D.m₁' D.m₂' E.m₃' E.tail hm₁' hm₂' hm₃' E.htail)
854 letI : NeZero secondPrime.q :=
855 ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) secondPrime.hqPrime.two_le)⟩
856 letI : Fintype (ZMod secondPrime.q) := ZMod.fintype secondPrime.q
857 letI : Fintype (Multiplicative (ZMod secondPrime.q)) := inferInstance
858 haveI : Finite (Multiplicative (ZMod secondPrime.q)) :=
859 Finite.of_fintype (Multiplicative (ZMod secondPrime.q))
860 haveI : ψ.ker.FiniteIndex := Subgroup.finiteIndex_ker ψ
861 exact
863 ψ eΨ QD.sourceSubgroup_exists_classical
864 let φ :=
865 firstReductionCanonicalSourceQuotientHom D.m₁' D.m₂'
866 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
867 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)
868 let eSource :
870 (secondReductionSourceSignature (p := D.p) D.m₁' D.m₂' E.m₃' E.tail secondPrime.hqPrime.two_le hm₁' hm₂'
871 (lt_of_lt_of_le (by decide : 0 < 2) hm₃') E.htail)
872 ≃*
875 D.m₁' D.m₂' E.m₃' E.tail D.hp secondPrime.hqPrime.two_le
876 hm₁' hm₂' hm₃' E.htail) :=
877 Classical.choice
879 D.m₁' D.m₂' E.m₃' E.tail D.hp secondPrime.hqPrime.two_le
880 hm₁' hm₂' hm₃' E.htail)
881 let eΦ :
882 φ.ker ≃*
885 D.m₁' D.m₂' E.m₃' E.tail D.hp secondPrime.hqPrime.two_le
886 hm₁' hm₂' hm₃' E.htail) :=
888 D.m₁' D.m₂' E.m₃' E.tail D.hp secondPrime.hqPrime.two_le
889 hm₁' hm₂' (lt_of_lt_of_le (by decide : 0 < 2) hm₃') E.htail).trans
890 eSource
891 letI : NeZero D.p :=
892 ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) D.hp)⟩
893 letI : Fintype (ZMod D.p) := ZMod.fintype D.p
894 letI : Fintype (Multiplicative (ZMod D.p)) := inferInstance
895 haveI : Finite (Multiplicative (ZMod D.p)) :=
896 Finite.of_fintype (Multiplicative (ZMod D.p))
897 simpa [canonicalSource, φ] using
899 φ eΦ hMiddleSubgroup
900 let eSource :
901 FuchsianPresentedGroup E.sourceSignature ≃*
902 FuchsianPresentedGroup canonicalSource :=
903 by
904 simpa [canonicalSource, sourceTail, SecondStageCleanupPeriodData.sourceSignature,
905 firstReductionSourceSignature] using
906 (Classical.choice
908 D.m₁' D.m₂'
909 (firstReductionTailIncludingThird (q := secondPrime.q) E.m₃' E.tail)
910 D.hp hm₁' hm₂' sourceTail (Nat.succ_pos _)))
911 exact sourceSubgroup_exists_of_mulEquiv eSource hCanonicalSubgroup
913end FenchelNielsen