FenchelNielsenZomorrodian/Discrete/Torsion/FuchsianFiniteSubgroupFrontier.lean
1import FenchelNielsenZomorrodian.Discrete.Core.EllipticCompact
2import Mathlib.GroupTheory.OrderOfElement
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Torsion/FuchsianFiniteSubgroupFrontier.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15Isolates the remaining discrete Fuchsian finite-subgroup theorem: every finite subgroup of a compact
16Fuchsian presentation is conjugate into an elliptic stabilizer.
17-/
19namespace FenchelNielsen
21/-!
22The approved torsion-classification frontier.
26of an elliptic stabilizer. It replaces the older, more downstream smooth-kernel
27torsion-free axiom.
28-/
30/-- A subgroup is contained in a conjugate of one elliptic stabilizer, up to powers. -/
32 (σ : FuchsianSignature) (K : Subgroup (FuchsianPresentedGroup σ)) : Prop :=
33 ∃ i : Fin σ.numPeriods, ∃ c : FuchsianPresentedGroup σ,
34 ∀ k : K, ∃ n : ℤ,
35 (k : FuchsianPresentedGroup σ) =
36 c * ellipticElement σ i ^ n * c⁻¹
38/- FRONTIER `fuchsian-finite-subgroup-elliptic-stabilizer`.
40This is the sole approved discrete axiom frontier in `FenchelNielsen`. It is the compact
41no-cusp presentation currently consumed by the compact Fuchsian three-step route. -/
42/-- Finite nontrivial Fuchsian subgroups lie in conjugates of elliptic stabilizers. -/
44 (σ : FuchsianSignature)
45 (K : Subgroup (FuchsianPresentedGroup σ)) [Finite K]
46 (hK : K ≠ ⊥) :
49/-- A nontrivial finite-order element is conjugate to a power of an elliptic generator. -/
51 {G ι : Type*} [Group G] (elliptic : ι → G)
52 (frontier : ∀ K : Subgroup G, Finite K → K ≠ ⊥ →
53 ∃ i : ι, ∃ c : G, ∀ k : K, ∃ n : ℤ,
54 (k : G) = c * elliptic i ^ n * c⁻¹)
55 (g : G) (hg : IsOfFinOrder g) (hgne : g ≠ 1) :
56 ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n) := by
57 classical
58 let K : Subgroup G := Subgroup.zpowers g
59 letI : Fintype K := Fintype.ofEquiv (Fin (orderOf g)) (finEquivZPowers hg)
60 let hKfinite : Finite K := Finite.of_fintype K
61 have hKne : K ≠ ⊥ := by
62 intro hK
63 have hgmem : g ∈ K := Subgroup.mem_zpowers g
64 have hgbot : g ∈ (⊥ : Subgroup G) := by
65 simpa [K, hK] using hgmem
66 exact hgne (Subgroup.mem_bot.mp hgbot)
67 rcases frontier K hKfinite hKne with ⟨i, c, hcontain⟩
68 rcases hcontain ⟨g, Subgroup.mem_zpowers g⟩ with ⟨n, hn⟩
69 exact ⟨i, n, (isConj_iff.2 ⟨c, hn.symm⟩).symm⟩
71/-- A finite-order element is either trivial or conjugate to a power of an elliptic generator. -/
73 {G ι : Type*} [Group G] (elliptic : ι → G)
74 (frontier : ∀ K : Subgroup G, Finite K → K ≠ ⊥ →
75 ∃ i : ι, ∃ c : G, ∀ k : K, ∃ n : ℤ,
76 (k : G) = c * elliptic i ^ n * c⁻¹)
77 (g : G) (hg : IsOfFinOrder g) :
78 g = 1 ∨ ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n) := by
79 by_cases hgne : g = 1
80 · exact Or.inl hgne
81 · exact Or.inr
82 (finiteOrder_isConj_elliptic_zpow_of_frontier elliptic frontier g hg hgne)
84end FenchelNielsen