FenchelNielsenZomorrodian/Profinite/TorsionFrontier.lean
1import FenchelNielsenZomorrodian.Profinite.FGroup
2import ProCGroups.Generation.WordProductsAndClosure
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Profinite/TorsionFrontier.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 profinite torsion-classification frontier:
17-/
19namespace FenchelNielsen
21universe u
23namespace ProfiniteFGroup
25/-- A subgroup is contained in a conjugate of one inertia group, up to powers. -/
27 (Δ : ProfiniteFGroup.{u}) (K : Subgroup Δ.carrier) : Prop :=
28 ∃ i : Fin Δ.signature.numPeriods, ∃ c : Δ.carrier,
29 ∀ k : K, ∃ n : ℤ,
30 (k : Δ.carrier) = c * Δ.inertia i ^ n * c⁻¹
32/- FRONTIER `profinite-fgroup-torsion-theorem`.
35a profinite F-group are controlled by the stack inertia groups. It is kept
36separate from the discrete Fuchsian torsion frontier.
37-/
38/-- Finite nontrivial profinite `F`-subgroups lie in conjugates of inertia groups. -/
40 (Δ : ProfiniteFGroup.{u})
41 (K : Subgroup Δ.carrier) [Finite K]
42 (hK : K ≠ ⊥) :
43 Δ.finiteSubgroupLeConjInertia K
45/-- A nontrivial finite-order element is conjugate to a power of an inertia element. -/
47 (Δ : ProfiniteFGroup.{u}) (g : Δ.carrier)
48 (hg : IsOfFinOrder g) (hgne : g ≠ 1) :
49 ∃ i : Fin Δ.signature.numPeriods, ∃ n : ℤ,
50 IsConj g (Δ.inertia i ^ n) := by
51 classical
52 let K : Subgroup Δ.carrier := Subgroup.zpowers g
53 letI : Fintype K := Fintype.ofEquiv (Fin (orderOf g)) (finEquivZPowers hg)
54 letI : Finite K := Finite.of_fintype K
55 have hKne : K ≠ ⊥ := by
56 intro hK
57 have hgmem : g ∈ K := Subgroup.mem_zpowers g
58 have hgbot : g ∈ (⊥ : Subgroup Δ.carrier) := by
59 simpa [K, hK] using hgmem
60 exact hgne (Subgroup.mem_bot.mp hgbot)
61 rcases finiteSubgroup_le_conj_inertia Δ K hKne with
62 ⟨i, c, hcontain⟩
63 rcases hcontain ⟨g, Subgroup.mem_zpowers g⟩ with ⟨n, hn⟩
64 exact ⟨i, n, (isConj_iff.2 ⟨c, hn.symm⟩).symm⟩
66/-- An open normal subgroup avoids the nontrivial profinite inertia powers. -/
68 (Δ : ProfiniteFGroup.{u}) (U : OpenNormalSubgroup Δ.carrier) : Prop :=
69 ∀ i : Fin Δ.signature.numPeriods, ∀ n : ℤ,
70 Δ.inertia i ^ n ∈ (U : Subgroup Δ.carrier) →
71 Δ.inertia i ^ n = 1
73/-- Avoiding nontrivial inertia powers makes an open normal subgroup torsion-free. -/
75 (Δ : ProfiniteFGroup.{u}) (U : OpenNormalSubgroup Δ.carrier)
76 (hAvoid : Δ.avoidsNontrivialInertia U) :
77 ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier U := by
78 intro x hx hxfin
79 by_cases hx1 : x = 1
80 · exact hx1
81 · rcases finiteOrder_isConj_inertia_zpow_of_ne_one Δ x hxfin hx1 with
82 ⟨i, n, hconj⟩
83 have hinU : Δ.inertia i ^ n ∈ (U : Subgroup Δ.carrier) := by
84 rcases isConj_iff.1 hconj with ⟨c, hc⟩
85 rw [← hc]
86 exact U.isNormal'.conj_mem x hx c
87 have hpow1 : Δ.inertia i ^ n = 1 := hAvoid i n hinU
88 exact isConj_one_left.mp (by simpa [hpow1] using hconj)
90/-- There is an open normal subgroup avoiding all nontrivial inertia powers. -/
92 (Δ : ProfiniteFGroup.{u}) :
93 ∃ U : OpenNormalSubgroup Δ.carrier,
94 Δ.avoidsNontrivialInertia U := by
95 classical
96 have hEach :
97 ∀ i : Fin Δ.signature.numPeriods,
98 ∃ U : OpenNormalSubgroup Δ.carrier,
99 ((U : Subgroup Δ.carrier) ⊓
100 Subgroup.zpowers (Δ.inertia i)) = ⊥ := by
101 intro i
102 let K : Subgroup Δ.carrier := Subgroup.zpowers (Δ.inertia i)
103 have hfinord : IsOfFinOrder (Δ.inertia i) := by
104 rw [← orderOf_pos_iff]
105 rw [Δ.inertia_order i]
106 exact lt_of_lt_of_le (by decide : 0 < 2) (Δ.signature.period_ge_two i)
107 letI : Fintype K :=
108 Fintype.ofEquiv (Fin (orderOf (Δ.inertia i)))
109 (finEquivZPowers hfinord)
110 letI : Finite K := Finite.of_fintype K
111 exact
113 (G := Δ.carrier) Δ.isProfinite K
114 choose U hU using hEach
115 by_cases hnonempty :
116 (Finset.univ : Finset (Fin Δ.signature.numPeriods)).Nonempty
117 · let V : OpenNormalSubgroup Δ.carrier :=
118 (Finset.univ : Finset (Fin Δ.signature.numPeriods)).inf' hnonempty U
119 refine ⟨V, ?_⟩
120 intro i n hn
121 have hVle : V ≤ U i := by
122 dsimp [V]
123 exact Finset.inf'_le
124 (s := (Finset.univ : Finset (Fin Δ.signature.numPeriods)))
125 (f := U) (b := i) (by simp only [Finset.mem_univ])
126 have hmemU : Δ.inertia i ^ n ∈ (U i : Subgroup Δ.carrier) :=
127 hVle hn
128 have hmemZ : Δ.inertia i ^ n ∈ Subgroup.zpowers (Δ.inertia i) :=
129 Subgroup.mem_zpowers_iff.2 ⟨n, rfl⟩
130 have hbot :
131 Δ.inertia i ^ n ∈ (⊥ : Subgroup Δ.carrier) := by
132 have hInf :
133 Δ.inertia i ^ n ∈
134 ((U i : Subgroup Δ.carrier) ⊓
135 Subgroup.zpowers (Δ.inertia i)) :=
136 ⟨hmemU, hmemZ⟩
137 simpa [hU i] using hInf
138 exact Subgroup.mem_bot.mp hbot
139 · refine ⟨⊤, ?_⟩
140 intro i
141 exact False.elim (hnonempty ⟨i, by simp only [Finset.mem_univ]⟩)
143/-- Every profinite `F`-group has a torsion-free open normal subgroup. -/
145 (Δ : ProfiniteFGroup.{u}) :
146 ∃ U : OpenNormalSubgroup Δ.carrier,
147 ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier U := by
148 rcases exists_openNormal_avoidsNontrivialInertia Δ with ⟨U, hU⟩
149 exact ⟨U, torsionFree_of_avoidsNontrivialInertia Δ U hU⟩
153end FenchelNielsen