FenchelNielsenZomorrodian/Discrete/Torsion/CompactFiniteOrder.lean
1import FenchelNielsenZomorrodian.Discrete.Torsion.FuchsianFiniteSubgroupFrontier
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Torsion/CompactFiniteOrder.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14Compact finite-order lemmas and the remaining finite-subgroup theorem for Fuchsian orbifold groups.
15-/
17namespace FenchelNielsen
20 (σ : FuchsianSignature) (g : FuchsianPresentedGroup σ)
21 (hg : IsOfFinOrder g) (hgne : g ≠ 1) :
22 ∃ i : Fin σ.numPeriods, ∃ n : ℤ,
23 IsConj g (ellipticElement σ i ^ n) := by
24 exact
26 (fun K hKfinite hKne => by
27 haveI : Finite K := hKfinite
28 exact finiteSubgroup_le_conj_ellipticStabilizer σ K hKne)
29 g hg hgne
32 (σ : FuchsianSignature) (g : FuchsianPresentedGroup σ)
33 (hg : IsOfFinOrder g) :
34 g = 1 ∨ ∃ i : Fin σ.numPeriods, ∃ n : ℤ,
35 IsConj g (ellipticElement σ i ^ n) := by
36 exact
38 (fun K hKfinite hKne => by
39 haveI : Finite K := hKfinite
40 exact finiteSubgroup_le_conj_ellipticStabilizer σ K hKne)
41 g hg
43end FenchelNielsen