FenchelNielsenZomorrodian/Profinite/DiscreteBridge.lean
1import FenchelNielsenZomorrodian.Discrete.MainTheorem
2import FenchelNielsenZomorrodian.Profinite.CompactFuchsianSignature
3import FenchelNielsenZomorrodian.Profinite.Perfectness
4import FenchelNielsenZomorrodian.Profinite.SmoothQuotient
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FenchelNielsenZomorrodian/Profinite/DiscreteBridge.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Bridge from discrete compact Fuchsian quotients to profinite quotients
17Transfers compact zero-genus three-step finite-index constructions through the profinite presentation to obtain finite smooth profinite quotients.
18-/
20namespace FenchelNielsen
22universe u
24open scoped BigOperators
26namespace ProfiniteFGroup
28theorem mul_swap_eq_one_of_mul_eq_one
29 {G : Type*} [Group G] {a b : G} (h : a * b = 1) :
30 b * a = 1 := by
31 have ha : a = b⁻¹ := by
32 calc
33 a = a * 1 := by simp only [mul_one]
34 _ = a * (b * b⁻¹) := by simp only [mul_one, mul_inv_cancel]
35 _ = (a * b) * b⁻¹ := by group
36 _ = b⁻¹ := by simp only [h, one_mul]
37 simp only [ha, mul_inv_cancel]
39/-- The abstract compact Fuchsian presentation maps to a compact profinite `F`-group by sending
40the paper generators to the corresponding profinite presentation generators. -/
41noncomputable def compactPresentationHomToProfinite
42 (Δ : ProfiniteFGroup.{u})
43 (hCompact : Δ.signature.IsCompact)
44 (hPeriods : 3 ≤ Δ.signature.numPeriods) :
46 (compactFuchsianSignature Δ.signature hCompact hPeriods) →*
47 Δ.carrier := by
48 let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
49 let f : FuchsianGenerator σ → Δ.carrier
50 | .elliptic i => Δ.inertia i
51 | .surfaceA i => Δ.surfaceA i
52 | .surfaceB i => Δ.surfaceB i
54 intro r hr
55 rcases hr with ⟨i, rfl⟩ | rfl
56 · have hpow : Δ.inertia i ^ Δ.signature.periods i = 1 := by
57 rw [← Δ.inertia_order i]
58 exact pow_orderOf_eq_one (Δ.inertia i)
59 simpa [σ, f, xWord, compactFuchsianSignature] using hpow
60 · have hCusp :
61 ((List.finRange Δ.signature.numCusps).map fun j => Δ.cusp j).prod = 1 := by
62 apply List.prod_eq_one
63 intro x hx
64 rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
65 exfalso
66 rw [hCompact] at j
67 exact Nat.not_lt_zero _ j.2
68 have hRel :
69 ((List.finRange Δ.signature.orbitGenus).map fun i =>
70 ⁅Δ.surfaceA i, Δ.surfaceB i⁆).prod *
71 ((List.finRange Δ.signature.numPeriods).map fun k => Δ.inertia k).prod =
72 1 := by
73 simpa [profiniteFenchelTotalRelation, hCusp, mul_assoc] using
74 Δ.presentation_relation
75 have hRel' :
76 ((List.finRange Δ.signature.numPeriods).map fun k => Δ.inertia k).prod *
77 ((List.finRange Δ.signature.orbitGenus).map fun i =>
78 ⁅Δ.surfaceA i, Δ.surfaceB i⁆).prod =
79 1 :=
81 simpa [σ, f, totalRelation, xWord, aWord, bWord, compactFuchsianSignature,
82 map_list_prod, Function.comp_def, map_commutatorElement] using hRel'
84@[local simp]
86 (Δ : ProfiniteFGroup.{u})
87 (hCompact : Δ.signature.IsCompact)
88 (hPeriods : 3 ≤ Δ.signature.numPeriods)
89 (i : Fin Δ.signature.numPeriods) :
90 compactPresentationHomToProfinite Δ hCompact hPeriods
92 (compactFuchsianSignature Δ.signature hCompact hPeriods) i) =
93 Δ.inertia i := by
94 simp only [compactPresentationHomToProfinite, ellipticElement, PresentedGroup.toGroup.of]
96@[local simp]
98 (Δ : ProfiniteFGroup.{u})
99 (hCompact : Δ.signature.IsCompact)
100 (hPeriods : 3 ≤ Δ.signature.numPeriods)
101 (i : Fin Δ.signature.orbitGenus) :
102 compactPresentationHomToProfinite Δ hCompact hPeriods
103 (PresentedGroup.of
105 (compactFuchsianSignature Δ.signature hCompact hPeriods))
106 (FuchsianGenerator.surfaceA i)) =
107 Δ.surfaceA i := by
108 simp only [compactPresentationHomToProfinite, PresentedGroup.toGroup.of]
110@[local simp]
112 (Δ : ProfiniteFGroup.{u})
113 (hCompact : Δ.signature.IsCompact)
114 (hPeriods : 3 ≤ Δ.signature.numPeriods)
115 (i : Fin Δ.signature.orbitGenus) :
116 compactPresentationHomToProfinite Δ hCompact hPeriods
117 (PresentedGroup.of
119 (compactFuchsianSignature Δ.signature hCompact hPeriods))
120 (FuchsianGenerator.surfaceB i)) =
121 Δ.surfaceB i := by
122 simp only [compactPresentationHomToProfinite, PresentedGroup.toGroup.of]
124private theorem compactPresentationHomToProfinite_elliptic_order
125 (Δ : ProfiniteFGroup.{u})
126 (hCompact : Δ.signature.IsCompact)
127 (hPeriods : 3 ≤ Δ.signature.numPeriods)
128 (i : Fin Δ.signature.numPeriods) :
129 orderOf
131 (compactFuchsianSignature Δ.signature hCompact hPeriods) i) =
132 Δ.signature.periods i := by
133 apply Nat.dvd_antisymm
134 · simpa [compactFuchsianSignature] using
135 orderOf_dvd_of_pow_eq_one
137 (compactFuchsianSignature Δ.signature hCompact hPeriods) i)
138 · have hdiv :=
139 orderOf_map_dvd
140 (compactPresentationHomToProfinite Δ hCompact hPeriods)
142 (compactFuchsianSignature Δ.signature hCompact hPeriods) i)
144 Δ.inertia_order i] using hdiv
146private noncomputable def compactDiscreteNormalQuotientGeneratorImageCore
147 (Δ : ProfiniteFGroup.{u})
148 (hCompact : Δ.signature.IsCompact)
149 (hPeriods : 3 ≤ Δ.signature.numPeriods)
150 (H : Subgroup
152 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
153 [H.Normal] :
154 ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
156 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H
157 | ULift.up (.surfaceA i) =>
158 QuotientGroup.mk' H
159 (PresentedGroup.of
161 (compactFuchsianSignature Δ.signature hCompact hPeriods))
162 (FuchsianGenerator.surfaceA i))
163 | ULift.up (.surfaceB i) =>
164 QuotientGroup.mk' H
165 (PresentedGroup.of
167 (compactFuchsianSignature Δ.signature hCompact hPeriods))
168 (FuchsianGenerator.surfaceB i))
169 | ULift.up (.cusp _) => 1
170 | ULift.up (.inertia i) =>
171 QuotientGroup.mk' H
173 (compactFuchsianSignature Δ.signature hCompact hPeriods) i)
175private noncomputable def compactDiscreteNormalQuotientGeneratorImage
176 (Δ : ProfiniteFGroup.{u})
177 (hCompact : Δ.signature.IsCompact)
178 (hPeriods : 3 ≤ Δ.signature.numPeriods)
179 (H : Subgroup
181 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
182 [H.Normal] :
183 ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
184 ULift.{u, 0}
186 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) :=
187 fun x =>
188 ULift.up
189 (compactDiscreteNormalQuotientGeneratorImageCore Δ hCompact hPeriods H x)
191private theorem compactDiscreteNormalQuotientGeneratorImage_total_relation
192 (Δ : ProfiniteFGroup.{u})
193 (hCompact : Δ.signature.IsCompact)
194 (hPeriods : 3 ≤ Δ.signature.numPeriods)
195 (H : Subgroup
197 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
198 [H.Normal] :
201 Δ hCompact hPeriods H
202 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
204 Δ hCompact hPeriods H
205 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
207 Δ hCompact hPeriods H
208 (ULift.up (ProfiniteFenchelGenerator.cusp j)))
210 Δ hCompact hPeriods H
211 (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1 := by
212 let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
213 let q : FuchsianPresentedGroup σ →*
214 FuchsianPresentedGroup σ ⧸ H :=
215 QuotientGroup.mk' H
216 have hPresented :
217 q (PresentedGroup.mk (relators σ) (totalRelation σ)) = 1 := by
218 simpa using congrArg q
220 (x := totalRelation σ) (Or.inr rfl))
221 have hPresented' :
223 (((List.finRange Δ.signature.numPeriods).map fun i =>
226 (((List.finRange Δ.signature.orbitGenus).map fun j =>
228 1 := by
229 simpa [σ, q, totalRelation, xWord, aWord, bWord, ellipticElement,
230 Function.comp_def, map_commutatorElement, compactFuchsianSignature] using hPresented
231 have hDiscreteTotal :
232 ((List.finRange Δ.signature.numPeriods).map fun i =>
234 ((List.finRange Δ.signature.orbitGenus).map fun j =>
237 1 := by
238 simpa [map_list_prod, Function.comp_def, map_commutatorElement] using hPresented'
239 have hSwapped :
240 ((List.finRange Δ.signature.orbitGenus).map fun j =>
243 ((List.finRange Δ.signature.numPeriods).map fun i =>
245 1 :=
246 mul_swap_eq_one_of_mul_eq_one hDiscreteTotal
247 have hCusp :
248 ((List.finRange Δ.signature.numCusps).map fun _j =>
249 (1 :
250 FuchsianPresentedGroup σ ⧸ H)).prod = 1 := by
251 rw [hCompact]
252 simp only [List.finRange_zero, List.map_nil, List.prod_nil]
253 simpa [profiniteFenchelTotalRelation,
254 compactDiscreteNormalQuotientGeneratorImageCore, σ, q, hCusp,
255 compactFuchsianSignature, mul_assoc] using hSwapped
258 (Δ : ProfiniteFGroup.{u})
259 (hCompact : Δ.signature.IsCompact)
260 (hPeriods : 3 ≤ Δ.signature.numPeriods)
261 (H : Subgroup
263 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
264 [H.Normal] :
267 Δ hCompact hPeriods H
268 (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
270 Δ hCompact hPeriods H
271 (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
273 Δ hCompact hPeriods H
274 (ULift.up (ProfiniteFenchelGenerator.cusp j)))
276 Δ hCompact hPeriods H
277 (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1 := by
278 apply
279 (MulEquiv.ulift :
280 ULift.{u, 0}
282 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
284 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).injective
286 map_list_prod, Function.comp_def, map_commutatorElement] using
288 Δ hCompact hPeriods H
290private theorem compactDiscreteNormalQuotientGeneratorImage_period_relation
291 (Δ : ProfiniteFGroup.{u})
292 (hCompact : Δ.signature.IsCompact)
293 (hPeriods : 3 ≤ Δ.signature.numPeriods)
294 (H : Subgroup
296 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
297 [H.Normal]
298 (k : Fin Δ.signature.numPeriods) :
300 Δ hCompact hPeriods H
301 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
302 Δ.signature.periods k = 1 := by
303 change
304 (QuotientGroup.mk' H
306 (compactFuchsianSignature Δ.signature hCompact hPeriods) k)) ^
307 (compactFuchsianSignature Δ.signature hCompact hPeriods).periods k = 1
308 rw [← map_pow, ellipticElement_pow_period_eq_one, map_one]
311 (Δ : ProfiniteFGroup.{u})
312 (hCompact : Δ.signature.IsCompact)
313 (hPeriods : 3 ≤ Δ.signature.numPeriods)
314 (H : Subgroup
316 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
317 [H.Normal]
318 (k : Fin Δ.signature.numPeriods) :
320 Δ hCompact hPeriods H
321 (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
322 Δ.signature.periods k = 1 := by
323 apply
324 (MulEquiv.ulift :
325 ULift.{u, 0}
327 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
329 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).injective
330 simpa [compactDiscreteNormalQuotientGeneratorImage] using
332 Δ hCompact hPeriods H k
334private theorem compactDiscreteNormalQuotient_derivedLength
335 (Δ : ProfiniteFGroup.{u})
336 (hCompact : Δ.signature.IsCompact)
337 (hPeriods : 3 ≤ Δ.signature.numPeriods)
338 (H : Subgroup
340 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
341 [H.Normal]
342 (hHQuot :
344 derivedSeries
346 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) 3 =
347 ⊥ := by
348 let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
349 let q : FuchsianPresentedGroup σ →*
350 FuchsianPresentedGroup σ ⧸ H :=
351 QuotientGroup.mk' H
352 have hmap :
353 Subgroup.map q (derivedSeries (FuchsianPresentedGroup σ) 3) =
354 derivedSeries (FuchsianPresentedGroup σ ⧸ H) 3 :=
355 derivedSeries_map_surjective q (QuotientGroup.mk'_surjective H) 3
356 apply le_antisymm
357 · intro y hy
358 rw [← hmap] at hy
359 rcases hy with ⟨x, hx, rfl⟩
360 exact Subgroup.mem_bot.mpr
361 ((QuotientGroup.eq_one_iff x).2 (hHQuot hx))
362 · exact bot_le
364private theorem compactDiscreteNormalQuotientGeneratorImage_inertia_order
365 (Δ : ProfiniteFGroup.{u})
366 (hCompact : Δ.signature.IsCompact)
367 (hPeriods : 3 ≤ Δ.signature.numPeriods)
368 (H : Subgroup
370 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
371 [H.Normal]
372 (hHTF : IsTorsionFreeGroup H)
373 (k : Fin Δ.signature.numPeriods) :
374 orderOf
376 Δ hCompact hPeriods H
377 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =
378 Δ.signature.periods k := by
379 let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
380 let q : FuchsianPresentedGroup σ →*
381 FuchsianPresentedGroup σ ⧸ H :=
382 QuotientGroup.mk' H
383 have hKerTF : IsTorsionFreeGroup q.ker := by
385 rw [QuotientGroup.ker_mk']
386 exact hHTF
387 have hFinite : IsOfFinOrder (ellipticElement σ k) := by
388 rw [← orderOf_pos_iff]
389 rw [compactPresentationHomToProfinite_elliptic_order Δ hCompact hPeriods k]
390 exact lt_of_lt_of_le (by decide : 0 < 2) (Δ.signature.period_ge_two k)
391 calc
392 orderOf
394 Δ hCompact hPeriods H
395 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =
396 orderOf (q (ellipticElement σ k)) := by
397 rfl
398 _ = orderOf (ellipticElement σ k) :=
399 orderOf_map_eq_of_torsionFree_ker q hKerTF hFinite
400 _ = Δ.signature.periods k :=
401 compactPresentationHomToProfinite_elliptic_order Δ hCompact hPeriods k
404 (Δ : ProfiniteFGroup.{u})
405 (hCompact : Δ.signature.IsCompact)
406 (hPeriods : 3 ≤ Δ.signature.numPeriods)
407 (H : Subgroup
409 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
410 [H.Normal]
411 (hHTF : IsTorsionFreeGroup H)
412 (k : Fin Δ.signature.numPeriods) :
413 orderOf
415 Δ hCompact hPeriods H
416 (ULift.up (ProfiniteFenchelGenerator.inertia k))) =
417 Δ.signature.periods k := by
418 have horder :=
419 orderOf_injective
420 ((MulEquiv.ulift :
421 ULift.{u, 0}
423 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
425 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).toMonoidHom)
426 (MulEquiv.ulift :
427 ULift.{u, 0}
429 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
431 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).injective
432 (compactDiscreteNormalQuotientGeneratorImage Δ hCompact hPeriods H
433 (ULift.up (ProfiniteFenchelGenerator.inertia k)))
434 rw [← horder]
435 exact
437 Δ hCompact hPeriods H hHTF k
439private noncomputable def compactDiscreteNormalQuotientSmoothData
440 (Δ : ProfiniteFGroup.{u})
441 (hCompact : Δ.signature.IsCompact)
442 (hPeriods : 3 ≤ Δ.signature.numPeriods)
443 (H : Subgroup
445 (compactFuchsianSignature Δ.signature hCompact hPeriods)))
446 (hHFiniteIndex : H.FiniteIndex)
447 (hHNormal : H.Normal)
448 (hHTF : IsTorsionFreeGroup H)
449 (hHQuot : SubgroupQuotientHasDerivedLengthAtMost H 3) :
450 ProfiniteSmoothQuotientData Δ 3 := by
451 letI : H.Normal := hHNormal
452 letI : H.FiniteIndex := hHFiniteIndex
453 letI :
454 TopologicalSpace
455 (ULift.{u, 0}
457 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H)) :=
458 ⊥
459 letI :
460 DiscreteTopology
461 (ULift.{u, 0}
463 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H)) :=
464 ⟨rfl⟩
465 letI :
466 Finite
467 (ULift.{u, 0}
469 (compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H)) := by
470 infer_instance
471 exact
472 ProfiniteSmoothQuotientData.ofPresentationLiftToFiniteOfRelationsOfDerivedSeries
473 Δ (compactDiscreteNormalQuotientGeneratorImage Δ hCompact hPeriods H)
475 Δ hCompact hPeriods H)
477 Δ hCompact hPeriods H)
480 Δ hCompact hPeriods H hHQuot))
482 Δ hCompact hPeriods H hHTF)
485 (Δ : ProfiniteFGroup.{u})
486 (hNonPerfect : Δ.IsNonPerfect)
487 (hCompact : Δ.signature.IsCompact)
488 (hZero : Δ.signature.orbitGenus = 0)
489 (hPeriods : 3 ≤ Δ.signature.numPeriods) :
490 ∃ H : Subgroup
492 (compactFuchsianSignature Δ.signature hCompact hPeriods)),
493 H.FiniteIndex ∧ IsTorsionFreeGroup H ∧
494 SubgroupQuotientHasDerivedLengthAtMost H 3 := by
495 classical
496 let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
497 have hZeroσ : σ.orbitGenus = 0 := by
498 simpa [σ, compactFuchsianSignature] using hZero
499 rcases
501 Δ hNonPerfect hZero hCompact with
502 ⟨p, hpPrime, i, j, hij, hpi, hpj⟩
503 let D : FirstReductionPeriodData σ :=
504 firstReductionPeriodDataOfPrimePair σ hpPrime hij
505 (by simpa [σ, compactFuchsianSignature] using hpi)
506 (by simpa [σ, compactFuchsianSignature] using hpj)
507 exact threeStep_sourceSubgroup_exists_of_zeroGenus_periodData σ hZeroσ D
509/-- Compact zero-genus profinite bridge: explicit zero-genus discrete period data transports through
510an exact profinite Fenchel presentation to the required profinite open-normal conclusion. -/
512 (Δ : ProfiniteFGroup.{u})
513 (hNonPerfect : Δ.IsNonPerfect)
514 (hCompact : Δ.signature.IsCompact)
515 (hZero : Δ.signature.orbitGenus = 0)
516 (hPeriods : 3 ≤ Δ.signature.numPeriods) :
518 Δ.carrier 3 := by
519 classical
520 let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
522 Δ hNonPerfect hCompact hZero hPeriods with
523 ⟨Hsource, hHsourceFiniteIndex, hHsourceTF, hHsourceQuot⟩
524 haveI : Hsource.FiniteIndex := hHsourceFiniteIndex
525 rcases
527 Hsource hHsourceTF hHsourceQuot with
528 ⟨H, hHFiniteIndex, hHNormal, hHTF, hHQuot⟩
529 exact
531 Δ hCompact hPeriods H hHFiniteIndex hHNormal hHTF hHQuot
536end FenchelNielsen