FenchelNielsenZomorrodian/Discrete/CompactFuchsian/Quotients.lean
1import FenchelNielsenZomorrodian.Discrete.Abelianization.EllipticAbelianization
2import FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodQuotient
3import FenchelNielsenZomorrodian.Discrete.FiniteIndex.SmoothQuotientData
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/Quotients.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Compact Fuchsian quotient constructions
17-/
19namespace FenchelNielsen
21noncomputable def finiteSolvableSmoothQuotientData_one_of_lcmCondition
22 (σ : FuchsianSignature)
23 (hLCM : LCMCondition σ.toFenchelSignature) :
24 FiniteSolvableSmoothQuotientData σ 1 where
25 Q := Multiplicative (PeriodAbelianization σ)
27 letI : Finite (PeriodAbelianization σ) := periodAbelianization_finite σ
28 infer_instance
29 φ := ellipticAbelianizationHom σ
30 derived_length := by
32 (Multiplicative (PeriodAbelianization σ))
33 elliptic_exact := by
34 intro i
35 simpa [ellipticAbelianizationHom_elliptic] using
36 periodClass_orderOf_eq_period σ hLCM i
39 (σ : FuchsianSignature) {m : ℕ} (hm : 1 ≤ m)
40 (hLCM : LCMCondition σ.toFenchelSignature) :
41 ∃ L : Subgroup (FuchsianPresentedGroup σ),
42 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
43 SubgroupQuotientHasDerivedLengthAtMost L m := by
44 have hSubgroupOne :
45 ∃ L : Subgroup (FuchsianPresentedGroup σ),
46 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
49 exact
51 (G := FuchsianPresentedGroup σ) (m := 1) (n := m) hm hSubgroupOne
53end FenchelNielsen