FenchelNielsenZomorrodian/Discrete/FiniteIndex/Smooth.lean
1import FenchelNielsenZomorrodian.Discrete.FiniteIndex.NormalCore
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/FiniteIndex/Smooth.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-index torsion-free subgroup data
14Abstract finite-index and smooth quotient data, kernel transfer, normal core, and derived-length predicates for discrete Fuchsian groups.
15-/
17namespace FenchelNielsen
19structure SmoothQuotientData
20 (G : Type*) [Group G]
21 (ι : Type*) (periods : ι → ℕ) (elliptic : ι → G)
22 (m : ℕ) where
23 Q : Type
24 [group : Group Q]
26 φ : G →* Q
27 derived_length : derivedSeries Q m = ⊥
28 elliptic_exact : ∀ i : ι, orderOf (φ (elliptic i)) = periods i
30namespace SmoothQuotientData
32def kernel {G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
33 {elliptic : ι → G} {m : ℕ}
34 (D : SmoothQuotientData G ι periods elliptic m) : Subgroup G := by
35 letI : Group D.Q := D.group
36 exact D.φ.ker
38theorem kernel_quotient_has_derivedLengthAtMost
39 {G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
40 {elliptic : ι → G} {m : ℕ}
41 (D : SmoothQuotientData G ι periods elliptic m) :
42 SubgroupQuotientHasDerivedLengthAtMost D.kernel m := by
43 intro g hg
44 letI : Group D.Q := D.group
45 change g ∈ D.φ.ker
46 rw [MonoidHom.mem_ker]
47 have hmap : D.φ g ∈ (derivedSeries G m).map D.φ := by
48 exact ⟨g, hg, rfl⟩
49 have hle : (derivedSeries G m).map D.φ ≤ derivedSeries D.Q m :=
50 map_derivedSeries_le_derivedSeries D.φ m
51 have hderived : D.φ g ∈ derivedSeries D.Q m := hle hmap
52 rw [D.derived_length] at hderived
53 simpa using hderived
56 {G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
57 {elliptic : ι → G} {m : ℕ}
58 (D : SmoothQuotientData G ι periods elliptic m)
59 (hEllipticZPow :
60 ∀ i : ι, ∀ n : ℤ, (periods i : ℤ) ∣ n → elliptic i ^ n = 1)
61 (g : G)
62 (hgKernel : g ∈ D.kernel)
63 (hConj : ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)) :
64 g = 1 := by
65 letI : Group D.Q := D.group
66 have hgKernel_eq : D.φ g = 1 := by
67 change g ∈ D.φ.ker at hgKernel
68 exact MonoidHom.mem_ker.mp hgKernel
69 rcases hConj with ⟨i, n, hconj⟩
70 have hφconj : IsConj (D.φ g) (D.φ (elliptic i ^ n)) :=
71 D.φ.map_isConj hconj
72 have hφtarget : D.φ (elliptic i ^ n) = 1 := by
73 exact isConj_one_right.mp <| by simpa [hgKernel_eq] using hφconj
74 have hdiv : (periods i : ℤ) ∣ n := by
75 rw [← D.elliptic_exact i]
76 exact orderOf_dvd_iff_zpow_eq_one.mpr (by
77 simpa [MonoidHom.map_zpow] using hφtarget)
78 have htargetOne : elliptic i ^ n = 1 :=
79 hEllipticZPow i n hdiv
80 exact isConj_one_left.mp <| by simpa [htargetOne] using hconj
83 {G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
84 {elliptic : ι → G} {m : ℕ}
85 (D : SmoothQuotientData G ι periods elliptic m)
86 (hEllipticZPow :
87 ∀ i : ι, ∀ n : ℤ, (periods i : ℤ) ∣ n → elliptic i ^ n = 1)
88 (hFiniteOrder :
89 ∀ g : G, IsOfFinOrder g →
90 g = 1 ∨ ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)) :
91 IsTorsionFreeGroup D.kernel := by
92 intro g hgfin
93 have hgfinSource : IsOfFinOrder (g : G) := by
94 simpa using
95 (Submonoid.isOfFinOrder_coe
96 (H := D.kernel.toSubmonoid) (x := g)).2 hgfin
97 rcases hFiniteOrder (g : G) hgfinSource with hgOne | hConj
98 · exact Subtype.ext hgOne
99 · exact Subtype.ext
100 (D.source_element_eq_one_of_kernel_conjugate_elliptic_zpow
101 hEllipticZPow (g : G) g.2 hConj)
104 {G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
105 {elliptic : ι → G} {m : ℕ}
106 (D : SmoothQuotientData G ι periods elliptic m)
107 (hEllipticZPow :
108 ∀ i : ι, ∀ n : ℤ, (periods i : ℤ) ∣ n → elliptic i ^ n = 1)
109 (hFiniteOrder :
110 ∀ g : G, IsOfFinOrder g →
111 g = 1 ∨ ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)) :
112 ∃ L : Subgroup G,
113 L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
114 SubgroupQuotientHasDerivedLengthAtMost L m := by
115 have hfinite : D.kernel.FiniteIndex := by
116 letI : Group D.Q := D.group
117 letI : Finite D.Q := D.finite
118 change D.φ.ker.FiniteIndex
119 exact Subgroup.finiteIndex_of_finite_quotient
120 exact ⟨D.kernel, hfinite,
121 D.kernel_torsionFree_of_finiteOrderClassification
122 hEllipticZPow hFiniteOrder,
123 D.kernel_quotient_has_derivedLengthAtMost⟩
127end FenchelNielsen