FenchelNielsenZomorrodian/Profinite/Perfectness.lean
1import FenchelNielsenZomorrodian.Discrete.Arithmetic.PrimeDivisors
2import FenchelNielsenZomorrodian.Profinite.FGroup
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Profinite/Perfectness.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Perfectness numerics for profinite Fenchel groups
15This file isolates the abelianization computation used in the non-perfect
17-/
19namespace FenchelNielsen
21universe u
23namespace ProfiniteFGroup
25/-- In a compact zero-genus no-cusp profinite Fenchel group, every commutative quotient kills the
26`otherPeriodsLcm`-power of each inertia image. -/
28 (Δ : ProfiniteFGroup.{u})
29 (hZero : Δ.signature.orbitGenus = 0)
30 (hNoCusps : Δ.signature.numCusps = 0)
31 {A : Type u} [CommGroup A]
32 (φ : Δ.carrier →* A) (i : Fin Δ.signature.numPeriods) :
33 φ (Δ.inertia i) ^ otherPeriodsLcm Δ.signature i = 1 := by
34 let ξ : Fin Δ.signature.numPeriods → A := fun j => φ (Δ.inertia j)
35 have hpow : ∀ j : Fin Δ.signature.numPeriods,
36 ξ j ^ Δ.signature.periods j = 1 := by
37 intro j
38 have hsource : Δ.inertia j ^ Δ.signature.periods j = 1 := by
39 rw [← Δ.inertia_order j]
40 exact pow_orderOf_eq_one (Δ.inertia j)
41 simpa [ξ] using congrArg φ hsource
42 have hprodList :
43 ((List.finRange Δ.signature.numPeriods).map fun j => ξ j).prod = 1 := by
44 have hrel := congrArg φ Δ.presentation_relation
45 have hrelFull :
46 (List.map (fun i : Fin Δ.signature.orbitGenus =>
47 φ ⁅Δ.surfaceA i, Δ.surfaceB i⁆)
48 (List.finRange Δ.signature.orbitGenus)).prod *
49 (List.map (fun j : Fin Δ.signature.numCusps => φ (Δ.cusp j))
50 (List.finRange Δ.signature.numCusps)).prod *
51 (List.map (fun k : Fin Δ.signature.numPeriods => φ (Δ.inertia k))
52 (List.finRange Δ.signature.numPeriods)).prod = 1 := by
53 simpa [profiniteFenchelTotalRelation, map_list_prod, Function.comp_def,
54 map_commutatorElement] using hrel
55 have hSurface :
56 (List.map (fun i : Fin Δ.signature.orbitGenus =>
57 φ ⁅Δ.surfaceA i, Δ.surfaceB i⁆)
58 (List.finRange Δ.signature.orbitGenus)).prod = 1 := by
59 apply List.prod_eq_one
60 intro x hx
61 rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
62 exfalso
63 rw [hZero] at j
64 exact Nat.not_lt_zero _ j.2
65 have hCusp :
66 (List.map (fun j : Fin Δ.signature.numCusps => φ (Δ.cusp j))
67 (List.finRange Δ.signature.numCusps)).prod = 1 := by
68 apply List.prod_eq_one
69 intro x hx
70 rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
71 exfalso
72 rw [hNoCusps] at j
73 exact Nat.not_lt_zero _ j.2
74 rw [hSurface, hCusp, one_mul, one_mul] at hrelFull
75 simpa [ξ] using hrelFull
76 have hprod : ∏ j : Fin Δ.signature.numPeriods, ξ j = 1 := by
77 simpa [Fin.prod_univ_def] using hprodList
78 let L := otherPeriodsLcm Δ.signature i
79 have hsplit' : ((Finset.univ.erase i).prod ξ) * ξ i = 1 := by
80 calc
81 ((Finset.univ.erase i).prod ξ) * ξ i = ∏ j, ξ j := by
82 exact Finset.prod_erase_mul
83 (s := Finset.univ) (f := ξ) (a := i) (Finset.mem_univ i)
84 _ = 1 := hprod
85 have hsplit : ξ i * ((Finset.univ.erase i).prod ξ) = 1 := by
86 simpa [mul_comm] using hsplit'
87 have hOthers :
88 ((Finset.univ.erase i).prod ξ) ^ L = 1 := by
89 rw [← Finset.prod_pow]
90 refine Finset.prod_eq_one ?_
91 intro j hj
92 obtain ⟨m, hm⟩ :=
93 Finset.dvd_lcm (s := Finset.univ.erase i)
94 (f := Δ.signature.periods) hj
95 rw [show L = Δ.signature.periods j * m by
96 simpa [L, otherPeriodsLcm] using hm,
97 pow_mul, hpow j, one_pow]
98 have hPow : ξ i ^ L = 1 := by
99 have hsplitPow := congrArg (fun a : A => a ^ L) hsplit
100 simp only at hsplitPow
101 rw [mul_pow, hOthers, mul_one] at hsplitPow
102 simpa [L] using hsplitPow
103 simpa [ξ, L] using hPow
105/-- Under the characteristic perfect numerical condition, every commutative quotient kills each
106inertia image. -/
108 (Δ : ProfiniteFGroup.{u})
109 (hChar : Δ.CharPerfectNumericalCondition)
110 {A : Type u} [CommGroup A]
111 (φ : Δ.carrier →* A)
112 (i : Fin Δ.signature.numPeriods) :
113 φ (Δ.inertia i) = 1 := by
114 rcases hChar with ⟨hZero, hNoCusps, hPair⟩
115 let ξ : Fin Δ.signature.numPeriods → A := fun j => φ (Δ.inertia j)
116 have hpow : ξ i ^ Δ.signature.periods i = 1 := by
117 have hsource : Δ.inertia i ^ Δ.signature.periods i = 1 := by
118 rw [← Δ.inertia_order i]
119 exact pow_orderOf_eq_one (Δ.inertia i)
120 simpa [ξ] using congrArg φ hsource
121 have hPow : ξ i ^ otherPeriodsLcm Δ.signature i = 1 :=
123 Δ hZero hNoCusps φ i
124 have hCoprimeProd :
125 Nat.Coprime (Δ.signature.periods i)
126 ((Finset.univ.erase i : Finset (Fin Δ.signature.numPeriods)).prod
127 Δ.signature.periods) := by
128 rw [Nat.coprime_prod_right_iff]
129 intro j hj
130 exact hPair i j (Finset.mem_erase.mp hj).1.symm
131 have hLDiv :
132 otherPeriodsLcm Δ.signature i ∣
133 (Finset.univ.erase i : Finset (Fin Δ.signature.numPeriods)).prod
134 Δ.signature.periods := by
135 dsimp [otherPeriodsLcm]
136 exact Finset.lcm_dvd (fun j hj => Finset.dvd_prod_of_mem _ hj)
137 have hCoprime :
138 Nat.Coprime (Δ.signature.periods i)
139 (otherPeriodsLcm Δ.signature i) :=
140 hCoprimeProd.of_dvd_right hLDiv
141 have hOrder : orderOf (ξ i) = 1 := by
142 exact Nat.eq_one_of_dvd_coprimes hCoprime
143 (orderOf_dvd_of_pow_eq_one hpow)
144 (orderOf_dvd_of_pow_eq_one hPow)
145 simpa [ξ] using orderOf_eq_one_iff.mp hOrder
147/-- The characteristic perfect numerical condition implies perfectness. -/
149 (Δ : ProfiniteFGroup.{u})
150 (hChar : Δ.CharPerfectNumericalCondition) :
151 Δ.IsPerfect := by
152 rcases hChar with ⟨hZero, hNoCusps, hPair⟩
153 let Q : Type u :=
155 let q : Δ.carrier →ₜ* Q :=
157 Δ.carrier 1
158 have hComm : Std.Commutative (fun a b : Q => a * b) := by
159 refine (Subgroup.Normal.quotient_commutative_iff_commutator_le
161 Δ.carrier 1)).2 ?_
162 change
163 ⁅(⊤ : Subgroup Δ.carrier), (⊤ : Subgroup Δ.carrier)⁆ ≤
165 change
166 ⁅(⊤ : Subgroup Δ.carrier), (⊤ : Subgroup Δ.carrier)⁆ ≤
167 (⁅(⊤ : Subgroup Δ.carrier), (⊤ : Subgroup Δ.carrier)⁆).topologicalClosure
168 exact Subgroup.le_topologicalClosure
169 (s := ⁅(⊤ : Subgroup Δ.carrier), (⊤ : Subgroup Δ.carrier)⁆)
170 letI : CommGroup Q :=
171 { inferInstanceAs (Group Q) with
172 mul_comm := hComm.comm }
173 have hInertia :
174 ∀ i : Fin Δ.signature.numPeriods, q (Δ.inertia i) = 1 := by
175 intro i
176 exact
178 Δ ⟨hZero, hNoCusps, hPair⟩ q.toMonoidHom i
179 have hq_eq_one : q = 1 := by
180 apply
182 Δ.presentation_generates
183 intro x hx
184 rcases hx with hxABC | hxInertia
185 · rcases hxABC with hxAB | hxCusp
186 · rcases hxAB with hxA | hxB
187 · rcases hxA with ⟨i, rfl⟩
188 exfalso
189 rw [hZero] at i
190 exact Nat.not_lt_zero _ i.2
191 · rcases hxB with ⟨i, rfl⟩
192 exfalso
193 rw [hZero] at i
194 exact Nat.not_lt_zero _ i.2
195 · rcases hxCusp with ⟨j, rfl⟩
196 exfalso
197 rw [hNoCusps] at j
198 exact Nat.not_lt_zero _ j.2
199 · rcases hxInertia with ⟨i, rfl⟩
200 simpa using hInertia i
201 apply le_antisymm
202 · exact le_top
203 · intro x _hx
204 have hxq : q x = 1 := by
206 ProCGroups.FiniteStepSolvableQuotients.closedDerivedSeries_zero, hq_eq_one, ContinuousMonoidHom.one_toFun]
207 exact
209 (G := Δ.carrier) (m := 1) (x := x)).1 hxq
211/-- Non-perfect compact zero-genus Fenchel groups have two periods with a common prime divisor.
213This numerical extraction is used directly by the compact discrete bridge, so the bridge does not
214need to prove non-perfectness again on the discrete presentation side. -/
216 (Δ : ProfiniteFGroup.{u})
217 (hNonPerfect : Δ.IsNonPerfect)
218 (hZero : Δ.signature.orbitGenus = 0)
219 (hNoCusps : Δ.signature.numCusps = 0) :
220 ∃ p : ℕ, p.Prime ∧
221 ∃ i j : Fin Δ.signature.numPeriods,
222 i ≠ j ∧ p ∣ Δ.signature.periods i ∧
223 p ∣ Δ.signature.periods j := by
224 exact
226 (periods := Δ.signature.periods)).mp
227 (by
228 intro hPair
229 exact hNonPerfect
230 (isPerfect_of_charPerfectNumericalCondition Δ ⟨hZero, hNoCusps, hPair⟩))
232/-- In the compact zero-genus non-perfect branch, fewer than three periods forces exactly two
235 (Δ : ProfiniteFGroup.{u})
236 (hNonPerfect : Δ.IsNonPerfect)
237 (hZero : Δ.signature.orbitGenus = 0)
238 (hNoCusps : Δ.signature.numCusps = 0)
239 (hNotThree : ¬ 3 ≤ Δ.signature.numPeriods) :
240 Δ.signature.numPeriods = 2 := by
241 rcases
243 Δ hNonPerfect hZero hNoCusps with
244 ⟨_p, _hpPrime, i, j, hij, _hpi, _hpj⟩
245 have hvne : i.val ≠ j.val := by
246 intro h
247 exact hij (Fin.ext h)
248 have hi := i.2
249 have hj := j.2
250 omega
254end FenchelNielsen