Yamaguchi Lean 4 Library
Yama2026_Sections_1_And_2_1/main.lean
Yama2026_Sections_1_And_2_1/main/Source

Yama2026_Sections_1_And_2_1/main.lean

1import ProCGroups.FiniteStepSolvableQuotients.AbelianActions.SlimnessAndTorsion
2import ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic
3import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality
4import FoxDifferential.Completed.ProCIntegerCoefficients.Core
5import ProCGroups.Categorical.QuotientPullbackEquivalences
6import ProCGroups.FreeProducts.UniversalProperty
7import ProCGroups.FreeProC.Abelianization
8import ProCGroups.FreeProC.SolvableQuotients
9import ProCGroups.Generation.Basic
10import ProCGroups.GroupTheory.Subgroups
11import ProCGroups.Order.Basic
12import CrowellExactSequence.Profinite.FiniteRank
13import ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower
14import Mathlib.NumberTheory.Padics.PadicVal.Basic
16/-
17PUBLIC_PAGE_SNAPSHOT
18generated_at: 2026-05-27T09:47:29+09:00
19lean_source: lean4/Yama2026_Sections_1_And_2_1/main.lean
20translation_root: data/translation
21purpose: identifies the local data snapshot used to build pages/
22placement: after imports, never before imports
23-/
24/-!
25# Yama2026: Section 1 and Subsection 2.1
27This file is the complete Lean public module for the currently formalized part of the Yama2026
28paper: Section 1 and Subsection 2.1. It intentionally keeps the theorem-numbered declarations in
29this file, rather than hiding them behind section-named modules or wrapper-only imports.
31The Section 1 part proves the free pro-`Σ` centralizer calculation, the completed abelianization
32non-zero-divisor lemma, the center-freeness theorem for maximal solvable quotients of free
33pro-`Σ` groups, and the slimness corollary. The Subsection 2.1 part records the
34ab-torsion-freeness and ab-faithfulness consequences used later in the paper.
35-/
37universe u v w z
39namespace CenterFreenessFiniteStepSolvable
41open scoped BigOperators
42open scoped Topology
43open ProCGroups.FiniteStepSolvableQuotients
44open ProCGroups.Abelian
45open ProCGroups.FreeProC
46open ProCGroups.GroupTheory
47open ProCGroups.Generation
48open ProCGroups.ProC
51-- Local notation used only in this file to keep paper-facing statements readable.
52local notation "Qm" => MaxSolvQuot
53local notation "AbTop" => TopologicalAbelianization
54local notation "SigmaGroup[" σ "]" => ProCGroups.FiniteGroupClass.sigmaGroup σ
55local notation "ProSigmaGroup[" σ "]" => ProCGroups.ProC.IsProCGroup (SigmaGroup[σ])
56local notation "IsFreeProSigmaProduct[" σ "]" =>
57 ProCGroups.FreeProducts.IsFreeProCProduct
60local instance sigmaGroupVarietyFact (sigma : Set ℕ) :
61 Fact (ProCGroups.FiniteGroupClass.Variety (SigmaGroup[sigma])) :=
62 ⟨ProCGroups.FiniteGroupClass.sigmaGroup_variety sigma⟩
64local instance sigmaGroupIsomClosedFact (sigma : Set ℕ) :
65 Fact (ProCGroups.FiniteGroupClass.IsomClosed (SigmaGroup[sigma])) :=
66 ⟨ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed sigma⟩
68variable {C : ProCGroups.FiniteGroupClass.{u}}
69variable [hCVariety : Fact (ProCGroups.FiniteGroupClass.Variety C)]
70variable [hCIsomClosed : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
72variable {G Q F Ω A P H : Type u}
73variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
74variable [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
75variable [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
76variable [TopologicalSpace Ω] [Group Ω] [IsTopologicalGroup Ω]
77variable [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
78variable [TopologicalSpace P] [Group P] [IsTopologicalGroup P]
79variable [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
82 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ) (a : G₀) :
83 ((G₀ ⧸ H) → ZMod K) ≃+
84 ((G₀ ⧸ H) → ZMod K) where
85 toFun f := fun q => f (a⁻¹ • q)
86 invFun f := fun q => f (a • q)
87 left_inv := by
88 intro f
89 ext q
90 simp only [inv_smul_smul]
91 right_inv := by
92 intro f
93 ext q
94 simp only [smul_inv_smul]
95 map_add' := by
96 intro f h
97 rfl
100 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ) :
101 G₀ × H →* MulAut (Multiplicative ((G₀ ⧸ H) → ZMod K)) where
102 toFun p := (cosetModuleAddEquiv H K p.1).toMultiplicative
103 map_one' := by
104 ext f q
105 simp only [cosetModuleAddEquiv, Prod.fst_one, inv_one, one_smul,
106 AddEquiv.toMultiplicative_apply_apply, AddEquiv.toAddMonoidHom_eq_coe,
107 AddMonoidHom.toMultiplicative_apply_apply, AddMonoidHom.coe_coe, AddEquiv.coe_mk,
108 Equiv.coe_fn_mk, ofAdd_toAdd, MulAut.one_apply]
109 map_mul' := by
110 intro p q
111 ext f x
112 simp only [cosetModuleAddEquiv, Prod.fst_mul, mul_inv_rev, mul_smul,
113 AddEquiv.toMultiplicative_apply_apply, AddEquiv.toAddMonoidHom_eq_coe,
114 AddMonoidHom.toMultiplicative_apply_apply, AddMonoidHom.coe_coe, AddEquiv.coe_mk,
115 Equiv.coe_fn_mk, toAdd_ofAdd, MulAut.mul_apply]
117/-- The finite coset-module semidirect product used in Lemma 1.2 and Proposition 1.3.
118This is kept as a type abbreviation because the full semidirect product type is repeated in
119projection maps, cyclic maps, and the finite-discrete `ProC` target. -/
121 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ) :=
122 Multiplicative ((G₀ ⧸ H) → ZMod K) ⋊[cosetModuleAction H K] (G₀ × H)
124-- The semidirect targets are used only as finite discrete test groups in this file.
125local instance
126 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ) :
127 TopologicalSpace (FreeprocenterCosetTarget H K) :=
128 ⊥
130local instance
131 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ) :
132 DiscreteTopology (FreeprocenterCosetTarget H K) :=
133 ⟨rfl⟩
135local instance
136 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ) :
137 IsTopologicalGroup (FreeprocenterCosetTarget H K) := by
138 infer_instance
140private def cosetBasis
141 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
142 [DecidableEq ((G₀ ⧸ H))] :
143 (G₀ ⧸ H) → ZMod K :=
144 Pi.single (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) (1 : ZMod K)
147 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
148 [DecidableEq ((G₀ ⧸ H))] {a : G₀} (ha : a ∈ H) :
150 ext q
151 change cosetBasis H K (a⁻¹ • q) = cosetBasis H K q
152 let e : (G₀ ⧸ H) := QuotientGroup.mk (1 : G₀)
153 have hbase : a • e = e := by
154 have hstab : a ∈ MulAction.stabilizer G₀ e := by
155 simpa [e, MulAction.stabilizer_quotient] using ha
156 exact (MulAction.mem_stabilizer_iff).1 hstab
157 have hbase_inv : a⁻¹ • e = e := by
158 have hstab : a⁻¹ ∈ MulAction.stabilizer G₀ e := by
159 simpa [e, MulAction.stabilizer_quotient] using H.inv_mem ha
160 exact (MulAction.mem_stabilizer_iff).1 hstab
161 by_cases hq : a⁻¹ • q = e
162 · have hq' : q = e := by
163 have := congrArg (fun r => a • r) hq
164 simpa [e, smul_smul, hbase] using this
165 rw [hq, hq']
166 · have hne :
167 a⁻¹ • q ≠ (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) := by
168 simpa [e] using hq
169 have hqbase : q ≠ (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) := by
170 intro hqbase
171 exact hq (by simpa [e, hqbase] using hbase_inv)
172 change
173 Pi.single (M := fun _ : (G₀ ⧸ H) => ZMod K)
174 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) (1 : ZMod K)
175 (a⁻¹ • q) =
176 Pi.single (M := fun _ : (G₀ ⧸ H) => ZMod K)
177 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) (1 : ZMod K) q
178 rw [Pi.single_eq_of_ne (M := fun _ => ZMod K) hne,
179 Pi.single_eq_of_ne (M := fun _ => ZMod K) hqbase]
182 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
183 [DecidableEq ((G₀ ⧸ H))]
184 {n : ℕ} (hn : (n : ZMod K) ≠ 0)
185 (b : (G₀ ⧸ H) → ZMod K) (a h : G₀) (hh : h ∈ H)
186 (heq :
187 b + cosetModuleAddEquiv H K a (n • cosetBasis H K) =
188 n • cosetBasis H K + cosetModuleAddEquiv H K h b) :
189 a ∈ H := by
190 have hcoord := congrFun heq (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H))
191 have hfixed :
193 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) =
194 b (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) := by
195 have hbase :
196 h⁻¹ • (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) =
197 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) :=
198 by
199 have hstab :
200 h⁻¹ ∈ MulAction.stabilizer G₀
201 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) := by
202 simpa [MulAction.stabilizer_quotient] using H.inv_mem hh
203 exact (MulAction.mem_stabilizer_iff).1 hstab
204 change b (h⁻¹ • (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H))) =
205 b (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H))
206 rw [hbase]
207 have hleft :
208 (cosetModuleAddEquiv H K a (n • cosetBasis H K))
209 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) = (n : ZMod K) := by
210 have hcoord0 : b (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) +
211 (cosetModuleAddEquiv H K a (n • cosetBasis H K))
212 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) =
213 (n : ZMod K) +
214 b (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) := by
215 simpa only [Pi.add_apply, Pi.smul_apply, Pi.mul_apply, cosetBasis, Pi.single_eq_same,
216 hfixed, nsmul_eq_mul, mul_one] using hcoord
217 have hcoord' : b (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) +
218 (cosetModuleAddEquiv H K a (n • cosetBasis H K))
219 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) =
220 b (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) + (n : ZMod K) := by
221 rw [add_comm (n : ZMod K)
222 (b (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)))] at hcoord0
223 exact hcoord0
224 exact add_left_cancel hcoord'
225 by_contra ha
226 have hzero :
227 (cosetModuleAddEquiv H K a (n • cosetBasis H K))
228 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) = 0 := by
229 change (n • cosetBasis H K)
230 (a⁻¹ • (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H))) = 0
231 have hne :
232 a⁻¹ • (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) ≠
233 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) := by
234 intro hbase
235 have hmem_inv : a⁻¹ ∈ H := by
236 have hstab :
237 a⁻¹ ∈ MulAction.stabilizer G₀
238 (QuotientGroup.mk (1 : G₀) : (G₀ ⧸ H)) :=
239 (MulAction.mem_stabilizer_iff).2 hbase
240 simpa [MulAction.stabilizer_quotient] using hstab
241 exact ha (by simpa using H.inv_mem hmem_inv)
242 simp only [Pi.smul_apply, cosetBasis, Pi.single_eq_of_ne (M := fun _ => ZMod K) hne,
243 nsmul_zero]
244 exact hn (hleft.symm.trans hzero)
247 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
248 [DecidableEq ((G₀ ⧸ H))] (g : G₀) (hg : g ∈ H) :
250 ⟨Multiplicative.ofAdd (cosetBasis H K), (g, ⟨g, hg⟩)⟩
253 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
254 [DecidableEq ((G₀ ⧸ H))] (g : G₀) (hg : g ∈ H) (n : ℕ) :
256 ⟨Multiplicative.ofAdd (n • cosetBasis H K), (g ^ n, ⟨g ^ n, H.pow_mem hg n⟩)⟩
258private theorem cosetTestElement_pow
259 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
260 [DecidableEq ((G₀ ⧸ H))]
261 (g : G₀) (hg : g ∈ H) (n : ℕ) :
262 cosetTestElement H K g hg ^ n = cosetTestPowerElement H K g hg n := by
263 induction n with
264 | zero =>
265 apply SemidirectProduct.ext
266 · apply Multiplicative.ofAdd.injective
267 ext q
268 simp only [pow_zero, SemidirectProduct.one_left, toAdd_ofAdd, toAdd_one,
269 Pi.zero_apply, cosetTestPowerElement, zero_nsmul, ofAdd_zero,
270 SemidirectProduct.mk_eq_inl_mul_inr, map_one, one_mul, SemidirectProduct.left_inr]
271 · change (1 : G₀ × H) = (g ^ 0, (⟨g ^ 0, H.pow_mem hg 0⟩ : H))
272 ext
273 · simp only [Prod.fst_one, pow_zero]
274 · simp only [Prod.snd_one, pow_zero, OneMemClass.coe_one]
275 | succ n ih =>
276 rw [pow_succ, ih]
277 apply SemidirectProduct.ext
278 · apply Multiplicative.ofAdd.injective
279 change
280 n • cosetBasis H K +
281 cosetModuleAddEquiv H K (g ^ n) (cosetBasis H K) =
282 Nat.succ n • cosetBasis H K
283 rw [action_basis_eq_self_of_mem H K (H.pow_mem hg n)]
284 exact (succ_nsmul (cosetBasis H K) n).symm
285 · ext <;> simp only [cosetTestPowerElement, nsmul_eq_mul,
286 SemidirectProduct.mk_eq_inl_mul_inr, cosetTestElement, mul_assoc,
287 SemidirectProduct.mul_right, SemidirectProduct.right_inl, SemidirectProduct.right_inr,
288 one_mul, Prod.mk_mul_mk, MulMemClass.mk_mul_mk, Nat.cast_add, Nat.cast_one,
289 pow_succ]
292 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
293 [DecidableEq ((G₀ ⧸ H))]
294 (g : G₀) (hg : g ∈ H) {s : ℕ}
295 (hgs : g ^ s = 1) (hs : (s : ZMod K) = 0) :
296 cosetTestElement H K g hg ^ s = 1 := by
297 rw [cosetTestElement_pow H K g hg s]
299 apply SemidirectProduct.ext
300 · change Multiplicative.ofAdd (s • cosetBasis H K) = 1
301 apply Multiplicative.ofAdd.injective
302 ext q
303 change (s • cosetBasis H K) q = 0
304 simp only [Pi.smul_apply, nsmul_eq_mul, hs, zero_mul]
305 · change ((g ^ s, (⟨g ^ s, H.pow_mem hg s⟩ : H)) : G₀ × H) = 1
306 ext <;> assumption
309 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ)
310 [DecidableEq ((G₀ ⧸ H))]
311 {n : ℕ} (hn : (n : ZMod K) ≠ 0)
312 {g : G₀} (hg : g ∈ H) (y : FreeprocenterCosetTarget H K)
313 (hy : y * cosetTestPowerElement H K g hg n = cosetTestPowerElement H K g hg n * y) :
314 y.right.1 ∈ H := by
315 have hleft := congrArg (fun z : FreeprocenterCosetTarget H K => z.left.toAdd) hy
316 have hmodule :
317 y.left.toAdd + cosetModuleAddEquiv H K y.right.1 (n • cosetBasis H K) =
318 n • cosetBasis H K + cosetModuleAddEquiv H K (g ^ n) y.left.toAdd :=
319 by
320 change
321 y.left.toAdd +
322 ((cosetModuleAction H K y.right)
323 (Multiplicative.ofAdd (n • cosetBasis H K))).toAdd =
324 (n • cosetBasis H K) +
325 ((cosetModuleAction H K (g ^ n, ⟨g ^ n, H.pow_mem hg n⟩))
326 y.left).toAdd at hleft
327 simpa using hleft
328 exact
329 mem_of_coset_centralizer_module_equation H K hn y.left.toAdd y.right.1 (g ^ n)
330 (H.pow_mem hg n) hmodule
332/-- Lemma 1.2 in the paper, in the equivalent nat-power form used after choosing
333`z τ^n z⁻¹ = τ^r`.
335Here `H = Subgroup.zpowers g`, the target is
336`(ZMod N)[G₀/H] ⋊ (G₀ × H)`, and `τ` is the element
337`([H], (g, g))`. If `z τ^n` is equal to a power of `τ` times `z`, and the image of
338`n` in `ZMod N` is nonzero with `N ∣ orderOf g`, then the first projection of `z`
339lies in `H`. -/
341 {G₀ : Type u} [Group G₀] (g : G₀) (N n : ℕ)
342 [DecidableEq ((G₀ ⧸ Subgroup.zpowers g))]
343 (hN : N ∣ orderOf g) (hn : (n : ZMod N) ≠ 0)
344 (z : FreeprocenterCosetTarget (Subgroup.zpowers g) N)
345 (hz :
346 ∃ r : ℕ,
347 z * (cosetTestElement (Subgroup.zpowers g) N g
348 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩)) ^ n =
349 (cosetTestElement (Subgroup.zpowers g) N g
350 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩)) ^ r * z) :
351 z.right.1 ∈ Subgroup.zpowers g := by
352 let H : Subgroup G₀ := Subgroup.zpowers g
353 let hg : g ∈ H := by
354 dsimp [H]
355 exact Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩
357 change z.right.1 ∈ H
358 rcases hz with ⟨r, hzr⟩
359 change z * τ ^ n = τ ^ r * z at hzr
360 have hzr' :
361 z * cosetTestPowerElement H N g hg n =
362 cosetTestPowerElement H N g hg r * z := by
363 simpa [τ, cosetTestElement_pow] using hzr
364 have hright := congrArg (fun y : FreeprocenterCosetTarget H N => y.right) hzr'
365 have hrightH := congrArg Prod.snd hright
366 change
367 z.right.2 * (⟨g ^ n, H.pow_mem hg n⟩ : H) =
368 (⟨g ^ r, H.pow_mem hg r⟩ : H) * z.right.2 at hrightH
369 letI : IsMulCommutative H := by
370 dsimp [H]
371 infer_instance
372 have hHpow :
373 (⟨g ^ n, H.pow_mem hg n⟩ : H) =
374 (⟨g ^ r, H.pow_mem hg r⟩ : H) := by
375 rw [mul_comm z.right.2 (⟨g ^ n, H.pow_mem hg n⟩ : H)] at hrightH
376 exact mul_right_cancel hrightH
377 have hpow_g : g ^ n = g ^ r := congrArg Subtype.val hHpow
378 have hmod_order :
379 (n : ℤ) ≡ (r : ℤ) [ZMOD (orderOf g : ℤ)] := by
380 exact
381 (zpow_eq_zpow_iff_modEq (x := g) (m := n) (n := r)).mp (by
382 simpa only [zpow_natCast] using hpow_g)
383 have hmod_N :
384 (n : ℤ) ≡ (r : ℤ) [ZMOD (N : ℤ)] := by
385 exact Int.ModEq.of_dvd (Int.ofNat_dvd.mpr hN) hmod_order
386 have hcast : (n : ZMod N) = (r : ZMod N) := by
387 have hcastInt : ((n : ℤ) : ZMod N) = ((r : ℤ) : ZMod N) :=
388 (ZMod.intCast_eq_intCast_iff (n : ℤ) (r : ℤ) N).2 hmod_N
389 simpa using hcastInt
390 have hleft := congrArg (fun y : FreeprocenterCosetTarget H N => y.left.toAdd) hzr'
391 have hmodule0 :
392 z.left.toAdd + cosetModuleAddEquiv H N z.right.1 (n • cosetBasis H N) =
393 r • cosetBasis H N + cosetModuleAddEquiv H N (g ^ r) z.left.toAdd := by
394 change
395 z.left.toAdd +
396 ((cosetModuleAction H N z.right)
397 (Multiplicative.ofAdd (n • cosetBasis H N))).toAdd =
398 (r • cosetBasis H N) +
399 ((cosetModuleAction H N (g ^ r, ⟨g ^ r, H.pow_mem hg r⟩))
400 z.left).toAdd at hleft
401 simpa using hleft
402 have hbasis : r • cosetBasis H N = n • cosetBasis H N := by
403 ext q
404 simp only [Pi.smul_apply, nsmul_eq_mul]
405 rw [hcast.symm]
406 exact
407 mem_of_coset_centralizer_module_equation H N hn z.left.toAdd z.right.1
408 (g ^ r) (H.pow_mem hg r) (by simpa [hbasis] using hmodule0)
410/-- Lemma 1.2 in the paper: if `z τ^n z⁻¹` lies in the cyclic subgroup generated by
411`τ = ([H], (g, g))`, then the first projection of `z` lies in `H = Subgroup.zpowers g`. -/
413 {G₀ : Type u} [Group G₀] (g : G₀) (N n : ℕ)
414 [DecidableEq ((G₀ ⧸ Subgroup.zpowers g))]
415 (hfin : IsOfFinOrder g) (hN : N ∣ orderOf g) (hn : (n : ZMod N) ≠ 0)
416 (z : FreeprocenterCosetTarget (Subgroup.zpowers g) N)
417 (hz :
418 let τ := cosetTestElement (Subgroup.zpowers g) N g
419 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩)
420 z * τ ^ n * z⁻¹ ∈ Subgroup.zpowers τ) :
421 z.right.1 ∈ Subgroup.zpowers g := by
422 let H : Subgroup G₀ := Subgroup.zpowers g
423 let hg : g ∈ H := by
424 dsimp [H]
425 exact Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩
427 change
428 z.right.1 ∈ H
429 change z * τ ^ n * z⁻¹ ∈ Subgroup.zpowers τ at hz
430 have hcastOrder : (orderOf g : ZMod N) = 0 :=
431 (ZMod.natCast_eq_zero_iff (orderOf g) N).2 hN
432 have hτpow : τ ^ orderOf g = 1 :=
433 cosetTestElement_pow_eq_one_of H N g hg (pow_orderOf_eq_one g) hcastOrder
434 have hτfin : IsOfFinOrder τ :=
435 isOfFinOrder_iff_pow_eq_one.mpr ⟨orderOf g, hfin.orderOf_pos, hτpow⟩
436 rcases (hτfin.mem_powers_iff_mem_zpowers).2 hz with ⟨r, hr⟩
437 have hzr : z * τ ^ n = τ ^ r * z := by
438 calc
439 z * τ ^ n = (z * τ ^ n * z⁻¹) * z := by simp only [mul_assoc, inv_mul_cancel, mul_one]
440 _ = τ ^ r * z := by rw [← hr]
441 exact
443 change z * τ ^ n = τ ^ r * z
444 exact hzr⟩
447 {G₀ : Type u} [Group G₀] (H : Subgroup G₀) (K : ℕ) :
448 FreeprocenterCosetTarget H K →* G₀ where
449 toFun z := z.right.1
450 map_one' := rfl
451 map_mul' _ _ := rfl
454 {G₀ : Type u} [TopologicalSpace G₀] [Group G₀] [IsTopologicalGroup G₀] [T1Space G₀]
455 (H : Subgroup G₀) (K : ℕ) [IsMulCommutative H]
456 {m : ℕ} (hm : 2 ≤ m)
457 (hG : topDerivedTop G₀ (m - 1) = (⊥ : Subgroup G₀)) :
459 let T : Type u := FreeprocenterCosetTarget H K
460 let topLeftT : T →* G₀ := cosetTargetTopLeftHom H K
461 let rightSubT : T →* H :=
462 { toFun := fun z => z.right.2
463 map_one' := rfl
464 map_mul' := by
465 intro _ _
466 rfl }
467 let topLeftTₜ : T →ₜ* G₀ :=
468 { toMonoidHom := topLeftT
469 continuous_toFun := continuous_of_discreteTopology }
470 let rightSubTₜ : T →ₜ* H :=
471 { toMonoidHom := rightSubT
472 continuous_toFun := continuous_of_discreteTopology }
473 let D : Subgroup T := topDerivedTop T (m - 1)
474 have hD_left : D ≤ topLeftT.ker := by
475 intro z hz
476 have hzG : topLeftT z ∈ topDerivedTop G₀ (m - 1) :=
477 (topDerivedTop_le_comap (f := topLeftTₜ) (m := m - 1)) hz
478 rw [hG] at hzG
479 exact (MonoidHom.mem_ker).2 (by simpa using hzG)
480 have hm_pred : 1 ≤ m - 1 := by omega
481 letI : CommGroup H := inferInstance
482 have hH : topDerivedTop H (m - 1) = (⊥ : Subgroup H) :=
484 have hD_right : D ≤ rightSubT.ker := by
485 intro z hz
486 have hzH : rightSubT z ∈ topDerivedTop H (m - 1) :=
487 (topDerivedTop_le_comap (f := rightSubTₜ) (m := m - 1)) hz
488 rw [hH] at hzH
489 exact (MonoidHom.mem_ker).2 (by simpa using hzH)
490 have commutator_eq_one_of_right_eq_one :
491 ∀ {z w : FreeprocenterCosetTarget H K}, z.right = 1 → w.right = 1 → ⁅z, w⁆ = 1 := by
492 intro z w hz hw
493 apply SemidirectProduct.ext
494 · simp only [commutatorElement_def, SemidirectProduct.mul_left, hz, map_one,
495 MulAut.one_apply, SemidirectProduct.mul_right, hw, mul_one,
496 SemidirectProduct.inv_left, inv_one, mul_inv_cancel_comm,
497 SemidirectProduct.inv_right, mul_inv_cancel, SemidirectProduct.one_left]
498 · simp only [commutatorElement_def, SemidirectProduct.mul_right, hz, hw, mul_one,
499 SemidirectProduct.inv_right, inv_one, SemidirectProduct.one_right]
500 have hcomm : ⁅D, D⁆ ≤ (⊥ : Subgroup T) := by
501 rw [Subgroup.commutator_le]
502 intro z hz w hw
503 have hzL := (MonoidHom.mem_ker).1 (hD_left hz)
504 have hzR := (MonoidHom.mem_ker).1 (hD_right hz)
505 have hwL := (MonoidHom.mem_ker).1 (hD_left hw)
506 have hwR := (MonoidHom.mem_ker).1 (hD_right hw)
507 have hzRight : z.right = 1 := Prod.ext hzL hzR
508 have hwRight : w.right = 1 := Prod.ext hwL hwR
509 have hzw : ⁅z, w⁆ = (1 : T) :=
510 commutator_eq_one_of_right_eq_one hzRight hwRight
511 simpa [Subgroup.mem_bot] using hzw
512 have hclosed : IsClosed (((⊥ : Subgroup T) : Set T)) := by
513 exact isClosed_discrete _
514 have hclosedComm : closedCommutator D D ≤ (⊥ : Subgroup T) := by
515 exact Subgroup.topologicalClosure_minimal ⁅D, D⁆ hcomm hclosed
516 have hmEq : m = (m - 1) + 1 := (Nat.sub_add_cancel (le_trans (by decide : 1 ≤ 2) hm)).symm
517 apply le_antisymm ?_ bot_le
519 exact hclosedComm
522 {sigmaSet : Set ℕ} {G₀ : Type u} [Group G₀]
523 (H : Subgroup G₀) {ℓ r : ℕ} [Fact ℓ.Prime]
525 (hℓsigma : ℓ ∈ sigmaSet) :
528 (G := FreeprocenterCosetTarget H (ℓ ^ r)) := by
529 classical
530 letI : Finite G₀ := hG₀.1
532 (ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed sigmaSet) H hG₀
533 letI : Finite H := hH.1
534 letI : Finite ((G₀ ⧸ H)) := inferInstance
535 have hK :
538 (sigma := sigmaSet) hℓsigma (Fact.out : ℓ.Prime)
539 have hZ :
540 ProCGroups.FiniteGroupClass.IsSigmaNumber sigmaSet (Nat.card (ZMod (ℓ ^ r))) := by
541 simpa [Nat.card_zmod] using hK
542 have hM :
544 (Nat.card ((G₀ ⧸ H) → ZMod (ℓ ^ r))) := by
545 letI : Fintype ((G₀ ⧸ H)) := Fintype.ofFinite ((G₀ ⧸ H))
546 simpa [Nat.card_pi] using
547 ProCGroups.FiniteGroupClass.IsSigmaNumber.prod (sigma := sigmaSet) Finset.univ
548 (fun _ : (G₀ ⧸ H) => Nat.card (ZMod (ℓ ^ r))) (fun _ _ => hZ)
549 have hMmul :
551 (Nat.card (Multiplicative ((G₀ ⧸ H) → ZMod (ℓ ^ r)))) := by
552 simpa using hM
553 have hRight :
554 ProCGroups.FiniteGroupClass.IsSigmaNumber sigmaSet (Nat.card (G₀ × H)) := by
555 rw [Nat.card_prod]
557 letI : Finite (Multiplicative ((G₀ ⧸ H) → ZMod (ℓ ^ r))) := inferInstance
558 letI : Finite (G₀ × H) := inferInstance
559 letI : Finite (FreeprocenterCosetTarget H (ℓ ^ r)) :=
560 Finite.of_equiv
561 (Multiplicative ((G₀ ⧸ H) → ZMod (ℓ ^ r)) × (G₀ × H))
562 (SemidirectProduct.equivProd
563 (N := Multiplicative ((G₀ ⧸ H) → ZMod (ℓ ^ r)))
564 (G := G₀ × H)
565 (φ := cosetModuleAction H (ℓ ^ r))).symm
566 have hTclass :
568 (FreeprocenterCosetTarget H (ℓ ^ r)) := by
569 refine ⟨inferInstance, ?_⟩
570 rw [SemidirectProduct.card]
572 exact
575 (G := FreeprocenterCosetTarget H (ℓ ^ r))
576 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed sigmaSet)
577 hTclass
580 {G₀ H₀ : Type u} [Group G₀] [Group H₀] {H : Subgroup G₀} (K : ℕ)
581 (q : H₀ →* G₀) :
582 H₀ →* FreeprocenterCosetTarget H K where
583 toFun h := ⟨Multiplicative.ofAdd 0, (q h, 1)⟩
584 map_one' := by
585 apply SemidirectProduct.ext
586 · rfl
587 · ext <;> simp
588 map_mul' a b := by
589 apply SemidirectProduct.ext
590 · apply Multiplicative.ofAdd.injective
591 ext x
592 simp only [ofAdd_zero, toAdd_ofAdd, toAdd_one, Pi.zero_apply, SemidirectProduct.mk_eq_inl_mul_inr, map_one,
593 one_mul, SemidirectProduct.mul_left, SemidirectProduct.left_inr, SemidirectProduct.right_inr, mul_one]
594 · ext <;> simp
596private noncomputable def cosetTargetCyclicHom
597 {G₀ : Type u} [Group G₀] (K : ℕ) (g : G₀)
598 [DecidableEq ((G₀ ⧸ Subgroup.zpowers g))]
599 (hK : K ∣ orderOf g) :
600 ↥(Subgroup.zpowers g) →*
601 FreeprocenterCosetTarget (Subgroup.zpowers g) K := by
602 let H : Subgroup G₀ := Subgroup.zpowers g
603 let gH : H := ⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩⟩
604 let targetGen : FreeprocenterCosetTarget H K :=
605 cosetTestElement H K g (show g ∈ H by exact gH.2)
606 have hcast : (orderOf g : ZMod K) = 0 := (ZMod.natCast_eq_zero_iff (orderOf g) K).2 hK
607 have hpow : targetGen ^ orderOf g = 1 :=
608 cosetTestElement_pow_eq_one_of H K g (show g ∈ H by exact gH.2)
609 (pow_orderOf_eq_one g) hcast
610 have htargetOrder : orderOf targetGen ∣ orderOf g :=
611 (orderOf_dvd_iff_pow_eq_one (x := targetGen) (n := orderOf g)).2 hpow
612 have hcycOrder : orderOf gH = orderOf g := by
613 simp only [Subgroup.orderOf_mk, gH]
614 have htargetOrder' : orderOf targetGen ∣ orderOf gH := by
615 simpa [hcycOrder] using htargetOrder
616 have hgen : ∀ z : H, z ∈ Subgroup.zpowers gH := by
617 simpa [H, gH] using
619 exact
620 monoidHomOfForallMemZpowers
621 (G := H) (G' := FreeprocenterCosetTarget H K)
622 (g := gH) (g' := targetGen) hgen htargetOrder'
625 {Q G₀ : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q] [Group G₀]
626 (q : Q →* G₀) (x y : Q) (n : ℤ)
627 (K : ℕ) [DecidableEq ((G₀ ⧸ Subgroup.zpowers (q x)))]
628 (hn : (n.natAbs : ZMod K) ≠ 0)
629 (ψ : Q →* FreeprocenterCosetTarget (Subgroup.zpowers (q x)) K)
630 (hleftψ : (cosetTargetTopLeftHom (Subgroup.zpowers (q x)) K).comp ψ = q)
631 (hψx :
632 ψ x =
633 cosetTestElement (Subgroup.zpowers (q x)) K (q x)
634 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩))
635 (hy : y ∈ centralizerOf (x ^ n)) :
636 q y ∈
637 ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
638 Subgroup Q).map q := by
639 have hn_ne_zero : n ≠ 0 := by
640 intro h0
641 exact hn (by simp only [h0, Int.natAbs_zero, Nat.cast_zero])
642 have hyψz : ψ y ∈ centralizerOf ((ψ x) ^ n) := by
643 rw [mem_centralizerOf_iff] at hy ⊢
644 calc
645 ψ y * (ψ x) ^ n = ψ y * ψ (x ^ n) := by simp only [map_zpow]
646 _ = ψ (y * x ^ n) := by simp only [map_zpow, map_mul]
647 _ = ψ (x ^ n * y) := by rw [hy]
648 _ = ψ (x ^ n) * ψ y := by simp only [map_mul, map_zpow]
649 _ = (ψ x) ^ n * ψ y := by simp only [map_zpow]
650 have hyψNat :
651 ψ y ∈ centralizerOf ((ψ x) ^ (n.natAbs : ℤ)) :=
653 have hyψNat' :
654 ψ y ∈ centralizerOf ((ψ x) ^ n.natAbs) := by
655 rw [zpow_natCast] at hyψNat
656 exact hyψNat
657 have hyTarget :
659 (cosetTestPowerElement (Subgroup.zpowers (q x)) K (q x)
660 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩) n.natAbs) := by
661 rw [hψx, cosetTestElement_pow] at hyψNat'
662 exact hyψNat'
663 have hcyc :
664 (ψ y).right.1 ∈ Subgroup.zpowers (q x) :=
666 (Subgroup.zpowers (q x)) K (n := n.natAbs) hn (g := q x)
667 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩) (ψ y)
668 (mem_centralizerOf_iff.mp hyTarget)
669 have hqy : q y ∈ Subgroup.zpowers (q x) := by
670 have hleft_y := congrArg (fun f : Q →* G₀ => f y) hleftψ
671 change (ψ y).right.1 = q y at hleft_y
672 simpa [hleft_y.symm] using hcyc
675omit [IsTopologicalGroup P] in
676/-- In the free product quotient used in `freeprocenter`, a nontrivial power from the procyclic
677left factor does not lie in the previous derived subgroup. -/
679 {sigma : Set ℕ}
680 (ιC : A →ₜ* Ω) (ιP : P →ₜ* Ω)
681 (hOmega : IsFreeProSigmaProduct[sigma] ιC ιP)
682 (hAProSigma : ProSigmaGroup[sigma] A)
684 (x : A) (m : ℕ) (hm : 2 ≤ m) (n : ℤ) (hn : x ^ n ≠ 1) :
685 let qx : MaxSolvQuot Ω m := continuousToMaxSolvQuot Ω m (ιC x)
686 qx ^ n ∉ topDerivedTop (MaxSolvQuot Ω m) (m - 1) := by
687 intro qx hmem
688 let rΩA : Ω →ₜ* A :=
689 hOmega.lift hAProSigma (ContinuousMonoidHom.id A) (1 : P →ₜ* A)
690 have hr_left : rΩA.comp ιC = ContinuousMonoidHom.id A := by
691 exact hOmega.lift_left hAProSigma (ContinuousMonoidHom.id A) (1 : P →ₜ* A)
692 have hm_pos : 1 ≤ m := le_trans (by decide : 1 ≤ 2) hm
693 have hDmA : topDerivedTop A m = (⊥ : Subgroup A) :=
695 have hker : topDerivedTop Ω m ≤ (rΩA : Ω →* A).ker := by
696 intro z hz
697 have hzA : rΩA z ∈ topDerivedTop A m :=
698 (topDerivedTop_le_comap (f := rΩA) m) hz
699 rw [hDmA] at hzA
700 simpa using hzA
701 let rQ : MaxSolvQuot Ω m →ₜ* A :=
702 QuotientGroup.liftₜ (topDerivedTop Ω m) rΩA hker
703 have hm_pred : 1 ≤ m - 1 := by
704 simpa using Nat.sub_le_sub_right hm 1
705 have hDpredA : topDerivedTop A (m - 1) = (⊥ : Subgroup A) :=
707 have hmemA : rQ (qx ^ n) ∈ topDerivedTop A (m - 1) :=
708 (topDerivedTop_le_comap (f := rQ) (m - 1)) hmem
709 rw [hDpredA] at hmemA
710 have hrqx : rQ qx = x := by
711 change rΩA (ιC x) = x
712 have h := congrArg (fun f : A →ₜ* A => f x) hr_left
713 simpa using h
714 have hxone : x ^ n = 1 := by
715 have hmap : rQ (qx ^ n) = x ^ n := by
716 simp only [map_zpow, hrqx]
717 change rQ (qx ^ n) = 1 at hmemA
718 simpa [hmap] using hmemA
719 exact hn hxone
721omit [IsTopologicalGroup A] [IsTopologicalGroup P] in
722/-- Maximal solvable quotients of a free pro-`Σ` product remain pro-`Σ`. -/
724 {sigma : Set ℕ}
725 (ιC : A →ₜ* Ω) (ιP : P →ₜ* Ω)
726 (hOmega : IsFreeProSigmaProduct[sigma] ιC ιP)
727 (m : ℕ) :
728 ProSigmaGroup[sigma] (MaxSolvQuot Ω m) := by
729 exact
731 (C := SigmaGroup[sigma])
732 (ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed sigma)
733 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed sigma)
734 hOmega.isProC
736 (show IsClosed ((topDerivedTop Ω m : Subgroup Ω) : Set Ω) by infer_instance)
738omit [IsTopologicalGroup A] [IsTopologicalGroup P] in
739/-- Open normal quotients of `Q_m(Ω)` in the free pro-`Σ` product setting are finite
740`Σ`-groups. -/
742 {sigma : Set ℕ}
743 (ιC : A →ₜ* Ω) (ιP : P →ₜ* Ω)
744 (hOmega : IsFreeProSigmaProduct[sigma] ιC ιP)
745 (m : ℕ) (V : OpenNormalSubgroup (MaxSolvQuot Ω m)) :
746 SigmaGroup[sigma] ((MaxSolvQuot Ω m) ⧸ (V : Subgroup (MaxSolvQuot Ω m))) := by
747 exact
748 ProCGroups.ProC.IsProCGroup.quotient_mem
749 (C := SigmaGroup[sigma])
750 (ProCGroups.FiniteGroupClass.sigmaGroup_formation sigma)
752 (sigma := sigma) ιC ιP hOmega m)
753 V
755omit [IsTopologicalGroup P] in
756/-- Finite coset-module input for Proposition `freeprocenter`.
758For every open normal quotient of `Q_m(Ω)`, this chooses a smaller quotient which still detects
759`x^n`, kills the last derived subgroup, and satisfies the cyclic containment obtained from the
760permutation module on the left cosets of the cyclic image of `x`. -/
762 {sigma : Set ℕ}
763 (ιC : A →ₜ* Ω) (ιP : P →ₜ* Ω)
764 (hOmega : IsFreeProSigmaProduct[sigma] ιC ιP)
765 (hAProSigma : ProSigmaGroup[sigma] A)
766 (x : A) (hxgen : ProCGroups.Generation.TopologicallyGenerates (G := A) ({x} : Set A))
767 (m : ℕ) (hm : 2 ≤ m) (n : ℤ) (hn : x ^ n ≠ 1) :
768 ∀ U : OpenNormalSubgroup (MaxSolvQuot Ω m),
769 ∃ W : OpenNormalSubgroup (MaxSolvQuot Ω m),
770 (W : Subgroup (MaxSolvQuot Ω m)) ≤ (U : Subgroup (MaxSolvQuot Ω m)) ∧
771 let qx : MaxSolvQuot Ω m := continuousToMaxSolvQuot Ω m (ιC x)
772 let K : Subgroup (MaxSolvQuot Ω m) := topDerivedTop (MaxSolvQuot Ω m) (m - 1)
773 let V : OpenNormalSubgroup (MaxSolvQuot Ω m) := openNormalSubgroup_sup_normal K W
774 ∀ y : MaxSolvQuot Ω m, y ∈ centralizerOf (qx ^ n) →
775 QuotientGroup.mk' (V : Subgroup (MaxSolvQuot Ω m)) y ∈
776 ((closedSubgroupGenerated ({qx} : Set (MaxSolvQuot Ω m)) :
777 ClosedSubgroup (MaxSolvQuot Ω m)) :
778 Subgroup (MaxSolvQuot Ω m)).map
779 (QuotientGroup.mk' (V : Subgroup (MaxSolvQuot Ω m))) := by
780 /-
781 The finite-stage argument uses the quotient `G₀` of `Q_m(Ω)`, the cyclic subgroup
782 `H = <ρ(x)>`, and the permutation module `(Z / ℓ^r Z)[G₀/H]`. The chosen prime
783 power divides the order of `ρ(x)` but not `n`, so the coset coefficient of `[H]`
784 detects whether the first projection of a centralizing element lies in `H`.
785 -/
786 have hAprocyclic : ProCGroups.ProC.IsProcyclicGroup A := by
787 exact
789 (G := A) hAProSigma.isProfinite hxgen
790 letI : CompactSpace A := hAProSigma.isProfinite.compactSpace
791 letI : T2Space A := hAProSigma.isProfinite.t2Space
792 letI : TotallyDisconnectedSpace A := hAProSigma.isProfinite.totallyDisconnectedSpace
793 let qx : MaxSolvQuot Ω m := continuousToMaxSolvQuot Ω m (ιC x)
794 let K : Subgroup (MaxSolvQuot Ω m) := topDerivedTop (MaxSolvQuot Ω m) (m - 1)
795 have hnotK : qx ^ n ∉ K := by
796 change qx ^ n ∉ topDerivedTop (MaxSolvQuot Ω m) (m - 1)
797 exact
799 (sigma := sigma) ιC ιP hOmega hAProSigma hAprocyclic x m hm n hn
800 let Q : Type u := MaxSolvQuot Ω m
801 let hΩprof : ProCGroups.IsProfiniteGroup Ω :=
804 let hQprof : ProCGroups.IsProfiniteGroup Q := by
805 simpa [Q, MaxSolvQuot] using
807 (G := Ω) hΩprof
808 (show IsClosed ((topDerivedTop Ω m : Subgroup Ω) : Set Ω) by infer_instance))
809 letI : CompactSpace Q := hQprof.compactSpace
810 letI : T2Space Q := hQprof.t2Space
811 letI : TotallyDisconnectedSpace Q := hQprof.totallyDisconnectedSpace
812 haveI : K.Normal := by
813 dsimp [K]
814 infer_instance
815 have hKclosed : IsClosed (K : Set (MaxSolvQuot Ω m)) := by
816 dsimp [K]
817 infer_instance
818 refine
820 (Q := Q) qx n K hKclosed hnotK ?_
821 intro W hdetect
822 change
823 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
824 ∀ y : Q, y ∈ centralizerOf (qx ^ n) →
825 QuotientGroup.mk' (V : Subgroup Q) y ∈
826 ((closedSubgroupGenerated ({qx} : Set Q) : ClosedSubgroup Q) :
827 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))
828 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
829 let G₀ : Type u := Q ⧸ (V : Subgroup Q)
830 let q : Q →* G₀ := QuotientGroup.mk' (V : Subgroup Q)
831 let g : G₀ := q qx
832 have hG₀pi : SigmaGroup[sigma] G₀ := by
833 simpa [Q, G₀, V] using
835 (sigma := sigma) ιC ιP hOmega m V
836 letI : Finite G₀ := hG₀pi.1
837 letI : Fintype G₀ := Fintype.ofFinite G₀
838 letI : DecidableEq G₀ := Classical.decEq G₀
839 have hgpow_ne : g ^ n ≠ 1 := by
840 intro hg
841 apply hdetect
842 change qx ^ n ∈ (V : Subgroup Q)
843 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup Q)) (qx ^ n)).1 (by
844 simpa [q, g, map_zpow] using hg)
845 have hn_ne_zero : n ≠ 0 := by
846 intro hn0
847 apply hgpow_ne
848 simp only [hn0, zpow_zero]
849 have hg_finiteOrder : IsOfFinOrder g := isOfFinOrder_of_finite g
850 have horder_ne : orderOf g ≠ 0 :=
851 Nat.ne_of_gt ((orderOf_pos_iff).2 hg_finiteOrder)
852 letI : NeZero (orderOf g) := ⟨horder_ne⟩
853 rcases
854 ProCGroups.FiniteGroupClass.exists_prime_power_orderOf_gt_padicValNat_of_zpow_ne_one
855 (sigma := sigma) hG₀pi hgpow_ne with
856 ⟨ℓ, r, hℓprime, hrpos, hℓsigma, hpadicInt, hℓr_order⟩
857 have hpadic : padicValNat ℓ n.natAbs < r := by
858 simpa using hpadicInt
859 letI : Fact ℓ.Prime := ⟨hℓprime⟩
860 letI : Fact (0 < r) := ⟨hrpos⟩
861 have hnAbs_ne : n.natAbs ≠ 0 := by
862 exact Int.natAbs_ne_zero.mpr hn_ne_zero
863 have hn_not_dvd : ¬ ℓ ^ r ∣ n.natAbs := by
864 intro hdvd
865 have hle :
866 r ≤ padicValNat ℓ n.natAbs :=
867 (padicValNat_dvd_iff_le (p := ℓ) (a := n.natAbs) (n := r) hnAbs_ne).1 hdvd
868 exact (not_le_of_gt hpadic) hle
869 have hnCoeff : (n.natAbs : ZMod (ℓ ^ r)) ≠ 0 := by
870 intro hzero
871 exact hn_not_dvd ((ZMod.natCast_eq_zero_iff n.natAbs (ℓ ^ r)).1 hzero)
872 let H : Subgroup G₀ := Subgroup.zpowers g
873 let T : Type u := FreeprocenterCosetTarget H (ℓ ^ r)
874 letI : DecidableEq ((G₀ ⧸ H)) := Classical.decEq _
875 letI : IsMulCommutative H := by
876 dsimp [H]
877 infer_instance
878 let πΩ : Ω →ₜ* Q := continuousToMaxSolvQuot Ω m
879 let qΩ : Ω →* G₀ := q.comp πΩ
880 have hqΩcont : Continuous qΩ := by
881 simpa [qΩ, πΩ, q] using
882 (continuous_quotient_mk'.comp
883 (continuousToMaxSolvQuot Ω m).continuous_toFun :
884 Continuous (fun z : Ω => QuotientGroup.mk' (V : Subgroup Q)
886 have hqΩ_mem_zpowers : ∀ a : A, qΩ (ιC a) ∈ H := by
887 intro a
888 simpa [Q, qΩ, πΩ, q, qx, g, H] using
890 (q := q) (hq := (continuous_quotient_mk' : Continuous q))
891 ιC (x := x) (a := a) hxgen)
892 let qAcyc : A →* H :=
893 { toFun := fun a =>
894 ⟨qΩ (ιC a), hqΩ_mem_zpowers a⟩
895 map_one' := by
896 apply Subtype.ext
897 simp only [map_one, OneMemClass.coe_one, qΩ]
898 map_mul' := by
899 intro a b
900 apply Subtype.ext
901 simp only [map_mul, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, MulMemClass.mk_mul_mk, qΩ]}
902 have hqAcyc_cont : Continuous qAcyc := by
903 change Continuous (fun a : A => (⟨qΩ (ιC a), hqΩ_mem_zpowers a⟩ : H))
904 exact Continuous.subtype_mk (hqΩcont.comp ιC.continuous_toFun) hqΩ_mem_zpowers
905 let qAcycT : A →ₜ* H :=
906 { toMonoidHom := qAcyc
907 continuous_toFun := hqAcyc_cont }
908 let φH : H →* T := by
909 change H →* FreeprocenterCosetTarget (Subgroup.zpowers g) (ℓ ^ r)
910 exact cosetTargetCyclicHom (ℓ ^ r) g hℓr_order
911 have htopLeftφH :
912 (cosetTargetTopLeftHom H (ℓ ^ r)).comp φH = H.subtype := by
913 change (cosetTargetTopLeftHom (Subgroup.zpowers g) (ℓ ^ r)).comp
914 (cosetTargetCyclicHom (ℓ ^ r) g hℓr_order) =
915 (Subgroup.zpowers g).subtype
916 let Hcyc : Subgroup G₀ := Subgroup.zpowers g
917 let gH : Hcyc := ⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩⟩
918 have hgen : ∀ z : Hcyc, z ∈ Subgroup.zpowers gH := by
919 simpa [Hcyc, gH] using
921 apply (MonoidHom.eq_iff_eq_on_generator hgen _ _).2
923 dsimp only
924 simp only [MonoidHom.coe_comp, Function.comp_apply]
925 rw [monoidHomOfForallMemZpowers_apply_gen]
926 rfl
927 let φC₀ : A →* T :=
928 φH.comp qAcyc
929 let φG₀ : G₀ →* T :=
930 topLeftOnlyCosetTargetHom (H := H) (ℓ ^ r) (MonoidHom.id G₀)
931 let φP₀ : P →* T :=
932 φG₀.comp (qΩ.comp ιP)
933 let φC : A →ₜ* T :=
934 { toMonoidHom := φC₀
935 continuous_toFun := by
936 exact (continuous_of_discreteTopology : Continuous φH).comp hqAcyc_cont }
937 let φP : P →ₜ* T :=
938 { toMonoidHom := φP₀
939 continuous_toFun := by
940 have hqPcont : Continuous (qΩ.comp ιP : P → G₀) :=
941 hqΩcont.comp ιP.continuous_toFun
942 exact (continuous_of_discreteTopology : Continuous φG₀).comp hqPcont }
943 let ΦΩ : Ω →ₜ* T :=
944 hOmega.lift (cosetTarget_isProC_sigmaGroup H hG₀pi hℓsigma) φC φP
945 let topLeftT : T →* G₀ := cosetTargetTopLeftHom H (ℓ ^ r)
946 let topLeftΦΩ : Ω →ₜ* G₀ :=
947 { toMonoidHom := topLeftT.comp ΦΩ
948 continuous_toFun := by
949 exact (continuous_of_discreteTopology : Continuous topLeftT).comp ΦΩ.continuous_toFun }
950 let qΩT : Ω →ₜ* G₀ :=
951 { toMonoidHom := qΩ
952 continuous_toFun := hqΩcont }
953 have hG₀ProC :
955 (SigmaGroup[sigma])) (G := G₀) := by
956 exact
959 (G := G₀)
960 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed sigma)
961 hG₀pi
962 have htopLeftΦΩ : topLeftΦΩ = qΩT := by
963 apply hOmega.hom_ext hG₀ProC
964 · ext a
965 have hleft :
966 ΦΩ (ιC a) = φC a := by
967 have h := congrArg (fun f : A →ₜ* T => f a)
968 (hOmega.lift_left
969 (cosetTarget_isProC_sigmaGroup H hG₀pi hℓsigma) φC φP)
970 exact h
971 change topLeftT (ΦΩ (ιC a)) = qΩ (ιC a)
972 rw [hleft]
973 change ((cosetTargetTopLeftHom H (ℓ ^ r)).comp φH) (qAcyc a) = qΩ (ιC a)
974 rw [htopLeftφH]
975 rfl
976 · ext p
977 have hright :
978 ΦΩ (ιP p) = φP p := by
979 have h := congrArg (fun f : P →ₜ* T => f p)
980 (hOmega.lift_right
981 (cosetTarget_isProC_sigmaGroup H hG₀pi hℓsigma) φC φP)
982 exact h
983 change topLeftT (ΦΩ (ιP p)) = qΩ (ιP p)
984 rw [hright]
985 change ((cosetTargetTopLeftHom H (ℓ ^ r)).comp
986 (topLeftOnlyCosetTargetHom (H := H) (ℓ ^ r) (MonoidHom.id G₀)))
987 (qΩ (ιP p)) = qΩ (ιP p)
988 rfl
989 let qT : Q →ₜ* G₀ :=
990 { toMonoidHom := q
991 continuous_toFun := continuous_quotient_mk' }
992 have hqsurj : Function.Surjective q := by
993 simpa [q] using (QuotientGroup.mk_surjective (s := (V : Subgroup Q)))
994 have hK_le_V : K ≤ (V : Subgroup Q) := by
995 intro z hz
996 change z ∈ K ⊔ (W : Subgroup Q)
997 exact (le_sup_left : K ≤ K ⊔ (W : Subgroup Q)) hz
998 have hK_map_q_bot : K.map q = (⊥ : Subgroup G₀) := by
999 ext z
1000 constructor
1001 · rintro ⟨k, hk, rfl⟩
1002 exact (Subgroup.mem_bot).2 (by
1003 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup Q)) k).2 (hK_le_V hk))
1004 · intro hz
1005 rw [Subgroup.mem_bot] at hz
1006 subst z
1007 exact ⟨1, K.one_mem, by simp only [map_one, q]⟩
1008 have hG₀der : topDerivedTop G₀ (m - 1) = (⊥ : Subgroup G₀) := by
1009 have hclosed_comm :
1010 ∀ n : ℕ,
1011 IsClosed (((closedCommutator (topDerivedTop Q n) (topDerivedTop Q n)).map
1012 (qT : Q →* G₀) : Subgroup G₀) : Set G₀) := by
1013 intro _
1014 exact isClosed_discrete _
1015 have hmap :=
1016 topDerived_map_eq_of_surj (f := qT) hqsurj hclosed_comm (m - 1)
1017 rw [← hmap]
1018 simpa [K, qT] using hK_map_q_bot
1019 have hTder : topDerivedTop T m = (⊥ : Subgroup T) := by
1020 exact
1022 have hkerΦΩ : topDerivedTop Ω m ≤ (ΦΩ : Ω →* T).ker := by
1023 intro z hz
1024 have hzT : ΦΩ z ∈ topDerivedTop T m :=
1025 (topDerivedTop_le_comap (f := ΦΩ) (m := m)) hz
1026 rw [hTder] at hzT
1027 exact (MonoidHom.mem_ker).2 (by simpa using hzT)
1028 let ψ : Q →ₜ* T :=
1029 QuotientGroup.liftₜ (topDerivedTop Ω m) ΦΩ hkerΦΩ
1030 have hψ_topLeft : (cosetTargetTopLeftHom H (ℓ ^ r)).comp ψ = q := by
1031 ext ω
1032 simp only [MonoidHom.coe_comp, Function.comp_apply]
1033 have hψω :
1034 (ψ : Q →* T) ((QuotientGroup.mk' (topDerivedTop Ω m)) ω) = ΦΩ ω := by
1035 simpa [ψ] using
1036 (QuotientGroup.liftₜ_apply_mk (N := topDerivedTop Ω m)
1037 (f := ΦΩ) hkerΦΩ ω)
1038 rw [hψω]
1039 have happ := congrArg (fun f : Ω →ₜ* G₀ => f ω) htopLeftΦΩ
1040 simpa [topLeftΦΩ, qΩT, topLeftT, qΩ, πΩ] using happ
1041 have hψ_qx :
1042 ψ qx =
1043 cosetTestElement H (ℓ ^ r) g
1044 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one, g]⟩) := by
1045 have hψπ :
1046 ψ (πΩ (ιC x)) = ΦΩ (ιC x) := by
1047 simpa [ψ, πΩ] using
1048 (QuotientGroup.liftₜ_apply_mk (N := topDerivedTop Ω m)
1049 (f := ΦΩ) hkerΦΩ (ιC x))
1050 have hleft :
1051 ΦΩ (ιC x) = φC x := by
1052 have h := congrArg (fun f : A →ₜ* T => f x)
1053 (hOmega.lift_left
1054 (cosetTarget_isProC_sigmaGroup H hG₀pi hℓsigma) φC φP)
1055 exact h
1056 change ψ (πΩ (ιC x)) =
1057 cosetTestElement H (ℓ ^ r) g
1058 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one, g]⟩)
1059 rw [hψπ, hleft]
1060 change φH (qAcyc x) =
1061 cosetTestElement H (ℓ ^ r) g (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one, g]⟩)
1062 have hqAcyc_x :
1063 qAcyc x =
1064 (⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one, g]⟩⟩ : H) := by
1065 apply Subtype.ext
1066 rfl
1067 rw [hqAcyc_x]
1068 change cosetTargetCyclicHom (ℓ ^ r) g hℓr_order
1069 ⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩⟩ =
1070 cosetTestElement (Subgroup.zpowers g) (ℓ ^ r) g
1071 (Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩)
1073 dsimp only
1074 rw [monoidHomOfForallMemZpowers_apply_gen]
1075 show ∀ y : Q, y ∈ centralizerOf (qx ^ n) →
1076 QuotientGroup.mk' (V : Subgroup Q) y ∈
1077 ((closedSubgroupGenerated ({qx} : Set Q) : ClosedSubgroup Q) :
1078 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))
1079 intro yQ hy
1080 exact
1082 (q := q) (x := qx) (y := yQ) (n := n) (K := ℓ ^ r)
1083 hnCoeff ψ hψ_topLeft hψ_qx hy
1085omit [IsTopologicalGroup P] in
1086/-- Proposition 1.3 (`freeprocenter`) in the paper: the centralizer containment for a free
1087pro-`Σ` product whose left factor is procyclic pro-`Σ`. -/
1089 {sigma : Set ℕ}
1090 (ιC : A →ₜ* Ω) (ιP : P →ₜ* Ω)
1091 (hOmega : IsFreeProSigmaProduct[sigma] ιC ιP)
1092 (hAProSigma : ProSigmaGroup[sigma] A)
1093 (x : A) (hxgen : ProCGroups.Generation.TopologicallyGenerates (G := A) ({x} : Set A))
1094 (m : ℕ) (hm : 2 ≤ m) (n : ℤ) (hn : x ^ n ≠ 1) :
1095 centralizerOf (continuousToMaxSolvQuot Ω m ((ιC x) ^ n)) ≤
1097 Subgroup (MaxSolvQuot Ω m)) ⊔
1098 (topDerivedTop (MaxSolvQuot Ω m) (m - 1)) := by
1099 let Q : Type u := MaxSolvQuot Ω m
1100 let hΩprof : ProCGroups.IsProfiniteGroup Ω :=
1103 letI : CompactSpace Ω := hΩprof.compactSpace
1104 letI : T2Space Ω := hΩprof.t2Space
1105 letI : TotallyDisconnectedSpace Ω := hΩprof.totallyDisconnectedSpace
1106 let hQprof : ProCGroups.IsProfiniteGroup Q := by
1107 simpa [Q, MaxSolvQuot] using
1109 (G := Ω) hΩprof
1110 (show IsClosed ((topDerivedTop Ω m : Subgroup Ω) : Set Ω) by infer_instance))
1111 letI : CompactSpace Q := hQprof.compactSpace
1112 letI : T2Space Q := hQprof.t2Space
1113 letI : TotallyDisconnectedSpace Q := hQprof.totallyDisconnectedSpace
1114 let qx : Q := continuousToMaxSolvQuot Ω m (ιC x)
1115 let K : Subgroup Q := topDerivedTop Q (m - 1)
1116 have hqpow : continuousToMaxSolvQuot Ω m ((ιC x) ^ n) = qx ^ n := by
1117 simp only [qx, map_zpow]
1118 haveI : K.Normal := by
1119 dsimp [K]
1120 infer_instance
1121 have hKclosed : IsClosed (K : Set Q) := by
1122 dsimp [K]
1123 infer_instance
1124 have hcriterion :
1125 centralizerOf (qx ^ n) ≤
1126 ((closedSubgroupGenerated ({qx} : Set Q) : ClosedSubgroup Q) :
1127 Subgroup Q) ⊔ K := by
1128 refine
1130 (Q := Q) qx n K hKclosed ?_
1131 simpa only [Q, qx, K] using
1133 ιC ιP hOmega hAProSigma x hxgen m hm n hn
1134 simpa only [Q, qx, K, hqpow] using hcriterion
1136/-- Internal finite quotient class form of `lem:non-zero-div-free`.
1138The element is the completed group-algebra term `\bar x_i^n - 1`. The paper only needs the
1139pro-`Σ` case; this version abstracts only the harmless choice between the concrete
1140`SigmaGroup[sigma]` class and the finite quotient class induced by `proSigmaProC`. -/
1142 {sigma : Set ℕ} (C : ProCGroups.FiniteGroupClass.{u})
1143 (hC_to_sigma : ∀ {Q : Type u} [Group Q] [Finite Q], C Q → SigmaGroup[sigma] Q)
1144 (hsigma_to_C : ∀ {Q : Type u} [Group Q], SigmaGroup[sigma] Q → C Q)
1145 {r : ℕ} (X : Fin r → F)
1146 (hFree :
1147 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1149 (SigmaGroup[sigma])) (Fin r) F X)
1150 (i : Fin r) (n : ℤ) (hn : n ≠ 0) :
1151 IsLeftRegular
1152 (FoxDifferential.zcGroupLike
1154 (TopologicalAbelianization F)
1156 classical
1157 let HAb : Type u := TopologicalAbelianization F
1159 change IsLeftRegular (FoxDifferential.zcGroupLike C HAb (xbar ^ n) - 1)
1160 rw [isLeftRegular_iff_right_eq_zero_of_mul]
1161 intro y hy
1163 intro j
1165 let K : ℕ := j.1.modulus
1166 let U : ProCGroups.ProC.OpenNormalSubgroupInClass C HAb := OrderDual.ofDual j.2
1167 let Q : Type u := HAb ⧸ (U.1 : Subgroup HAb)
1168 let qU : HAb →ₜ* Q :=
1170 let aQ : Q := qU xbar
1171 let a : Q := aQ ^ n
1172 have hQC : C Q := by
1173 simpa only [Q, U] using U.2
1174 letI : Finite Q := ProCGroups.FiniteGroupClass.finite (C := C) hQC
1175 have hQsigma : SigmaGroup[sigma] Q := hC_to_sigma hQC
1176 letI : Fintype Q := Fintype.ofFinite Q
1177 letI : DecidableEq Q := Classical.decEq Q
1178 let d : ℕ := orderOf a
1179 let A : ℕ := n.natAbs
1180 let B : ℕ := K * d
1181 let M : ℕ := B ^ (A + 1)
1182 have hKpos : 0 < K := by
1183 simpa only [K] using j.1.positive
1184 have hApos : 0 < A := by
1185 exact Int.natAbs_pos.mpr hn
1186 have hdpos : 0 < d := by
1187 simpa only [d] using orderOf_pos a
1188 have hBpos : 0 < B := by
1189 exact Nat.mul_pos hKpos hdpos
1190 have hMpos : 0 < M := by
1191 exact pow_pos hBpos (A + 1)
1192 have hKMpos : 0 < K * M := by
1193 exact Nat.mul_pos hKpos hMpos
1194 letI : NeZero (K * M) := ⟨Nat.ne_of_gt hKMpos⟩
1195 letI : NeZero M := ⟨Nat.ne_of_gt hMpos⟩
1196 have hKsigma : ProCGroups.FiniteGroupClass.IsSigmaNumber sigma K := by
1197 let T : Type u := ULift.{u} (Multiplicative (ZMod j.1.modulus))
1198 letI : Group T := inferInstance
1199 letI : Finite T := ProCGroups.FiniteGroupClass.finite (C := C) j.1.cyclic_mem
1200 have hTsigma : SigmaGroup[sigma] T := hC_to_sigma j.1.cyclic_mem
1201 rcases hTsigma with ⟨_, hsigmaT⟩
1202 letI : NeZero j.1.modulus := ⟨Nat.ne_of_gt j.1.positive⟩
1203 have hcard : Nat.card T = j.1.modulus := by
1204 calc
1205 Nat.card T = Nat.card (Multiplicative (ZMod j.1.modulus)) :=
1206 Nat.card_congr (MulEquiv.ulift :
1207 T ≃* Multiplicative (ZMod j.1.modulus)).toEquiv
1208 _ = j.1.modulus := by
1209 simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
1210 simpa only [K, T, hcard] using hsigmaT
1211 have hdsigma : ProCGroups.FiniteGroupClass.IsSigmaNumber sigma d := by
1212 simpa only [d] using
1214 (orderOf_dvd_natCard a)
1215 have hBsigma : ProCGroups.FiniteGroupClass.IsSigmaNumber sigma B := by
1216 simpa only [B] using
1218 have hMsigma : ProCGroups.FiniteGroupClass.IsSigmaNumber sigma M := by
1219 simpa only [M] using
1221 have hKMsigma : ProCGroups.FiniteGroupClass.IsSigmaNumber sigma (K * M) := by
1223 rcases
1225 (sigma := sigma) (r := r) (L := K * M) hKMpos hKMsigma X hFree i with
1226 ⟨χ, hχ⟩
1227 have hTargetLsigma : SigmaGroup[sigma] (Q × Multiplicative (ZMod (K * M))) :=
1228 ProCGroups.FiniteGroupClass.sigmaGroup_prod_multiplicativeZMod
1229 (sigma := sigma) (Q := Q) hQsigma hKMpos hKMsigma
1230 let ΦL : HAb →ₜ* Q × Multiplicative (ZMod (K * M)) :=
1231 ContinuousMonoidHom.prod qU χ
1232 let red : Multiplicative (ZMod (K * M)) →ₜ* Multiplicative (ZMod M) :=
1233 { toMonoidHom := finiteCyclicReduction M K
1234 continuous_toFun := continuous_of_discreteTopology }
1235 let χM : HAb →ₜ* Multiplicative (ZMod M) := red.comp χ
1236 have hTargetMsigma : SigmaGroup[sigma] (Q × Multiplicative (ZMod M)) :=
1237 ProCGroups.FiniteGroupClass.sigmaGroup_prod_multiplicativeZMod
1238 (sigma := sigma) (Q := Q) hQsigma hMpos hMsigma
1239 let ΦM : HAb →ₜ* Q × Multiplicative (ZMod M) :=
1240 ContinuousMonoidHom.prod qU χM
1244 (by
1245 have hquotSigma : SigmaGroup[sigma] (HAb ⧸ ΦL.toMonoidHom.ker) :=
1246 let e : HAb ⧸ ΦL.toMonoidHom.ker ≃* ΦL.toMonoidHom.range :=
1247 QuotientGroup.quotientKerEquivRange ΦL.toMonoidHom
1248 have hRange : SigmaGroup[sigma] ΦL.toMonoidHom.range :=
1249 (ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed sigma)
1250 (H := ΦL.toMonoidHom.range) hTargetLsigma
1251 (ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed sigma) ⟨e.symm⟩ hRange
1252 exact hsigma_to_C hquotSigma)
1256 (by
1257 have hquotSigma : SigmaGroup[sigma] (HAb ⧸ ΦM.toMonoidHom.ker) :=
1258 let e : HAb ⧸ ΦM.toMonoidHom.ker ≃* ΦM.toMonoidHom.range :=
1259 QuotientGroup.quotientKerEquivRange ΦM.toMonoidHom
1260 have hRange : SigmaGroup[sigma] ΦM.toMonoidHom.range :=
1261 (ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed sigma)
1262 (H := ΦM.toMonoidHom.range) hTargetMsigma
1263 (ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed sigma) ⟨e.symm⟩ hRange
1264 exact hsigma_to_C hquotSigma)
1265 have hULUM : (UL.1 : Subgroup HAb) ≤ (UM.1 : Subgroup HAb) := by
1266 intro z hz
1267 have hzL : ΦL z = 1 := by
1268 change z ∈ ΦL.toMonoidHom.ker at hz
1269 exact MonoidHom.mem_ker.mp hz
1270 have hq : qU z = 1 := congrArg Prod.fst hzL
1271 have hχz : χ z = 1 := congrArg Prod.snd hzL
1272 change ΦM z = 1
1273 change (qU z, χM z) = (1, 1)
1274 rw [hq]
1275 change (1, red (χ z)) = (1, 1)
1276 rw [hχz]
1277 simp only [Lean.Elab.WF.paramLet, map_one, red]
1278 have hUMU : (UM.1 : Subgroup HAb) ≤ (U.1 : Subgroup HAb) := by
1279 intro z hz
1280 have hzM : ΦM z = 1 := by
1281 change z ∈ ΦM.toMonoidHom.ker at hz
1282 exact MonoidHom.mem_ker.mp hz
1283 have hq : qU z = 1 := congrArg Prod.fst hzM
1284 exact
1286 (C := C) (U := U)).mp hq
1288 (j.1, OrderDual.toDual UL)
1290 (j.1, OrderDual.toDual UM)
1291 have hkML : kM ≤ kL := by
1292 constructor
1293 · exact dvd_rfl
1294 · change (UL.1 : Subgroup HAb) ≤ (UM.1 : Subgroup HAb)
1295 exact hULUM
1296 have hjM : j ≤ kM := by
1297 constructor
1298 · exact dvd_rfl
1299 · change (UM.1 : Subgroup HAb) ≤ (U.1 : Subgroup HAb)
1300 exact hUMU
1305 let embL :
1307 Q × Multiplicative (ZMod (K * M)) :=
1308 quotientKerEmbedding ΦL.toMonoidHom
1309 let embM :
1311 Q × Multiplicative (ZMod M) :=
1312 quotientKerEmbedding ΦM.toMonoidHom
1313 have hstageL :
1314 (MonoidAlgebra.of (ZMod K)
1316 ((QuotientGroup.mk' (UL.1 : Subgroup HAb) xbar :
1318 1) * yL = 0 := by
1319 simpa only [yL, kL, K] using
1320 FoxDifferential.zcCompletedGroupAlgebra_projection_zpow_sub_one_mul_eq_zero
1321 C HAb xbar n y kL hy
1322 have hembL_x :
1323 embL
1324 (QuotientGroup.mk' (UL.1 : Subgroup HAb) xbar :
1326 (aQ, Multiplicative.ofAdd (1 : ZMod (K * M))) := by
1327 have hχx : χ xbar = Multiplicative.ofAdd (1 : ZMod (K * M)) := by
1329 change
1330 quotientKerEmbedding ΦL.toMonoidHom
1331 (QuotientGroup.mk' ΦL.toMonoidHom.ker xbar) =
1332 (aQ, Multiplicative.ofAdd (1 : ZMod (K * M)))
1334 change (qU xbar, χ xbar) = (aQ, Multiplicative.ofAdd (1 : ZMod (K * M)))
1335 simp only [hχx, aQ]
1336 have hembL_x_pow :
1337 (embL
1338 (QuotientGroup.mk' (UL.1 : Subgroup HAb) xbar :
1340 (a, Multiplicative.ofAdd (n : ZMod (K * M))) := by
1341 rw [hembL_x]
1342 ext
1343 · simp only [Prod.pow_mk, aQ, a]
1344 · change (Multiplicative.ofAdd (1 : ZMod (K * M))) ^ n =
1345 Multiplicative.ofAdd (n : ZMod (K * M))
1346 change Multiplicative.ofAdd (n • (1 : ZMod (K * M))) =
1347 Multiplicative.ofAdd (n : ZMod (K * M))
1348 simp only [zsmul_eq_mul, mul_one]
1349 have hrelProd :
1350 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
1351 (a, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) *
1352 MonoidAlgebra.mapDomainRingHom (ZMod K) embL yL = 0 := by
1353 have hpush :=
1355 (R := ZMod K)
1357 (OrderDual.toDual UL))
1358 (H := Q × Multiplicative (ZMod (K * M)))
1359 embL
1360 (QuotientGroup.mk' (UL.1 : Subgroup HAb) xbar :
1362 n yL hstageL
1363 rw [hembL_x_pow] at hpush
1364 exact hpush
1365 have hd_order : a ^ d = 1 := by
1366 simp only [pow_orderOf_eq_one, d]
1367 have hnatAbs_mul : (((d : ℤ) * n).natAbs) = d * A := by
1368 simp only [Int.natAbs_mul, Int.natAbs_natCast, A]
1369 have hgcd : Nat.gcd (((d : ℤ) * n).natAbs) (K * M) ∣ M := by
1370 simpa only [M, B, A, hnatAbs_mul] using
1372 (K := K) (d := d) (A := A) hKpos hdpos hApos
1373 have hzProd :
1374 MonoidAlgebra.mapDomainRingHom (ZMod K) (finiteProductCyclicReduction Q M K)
1375 (MonoidAlgebra.mapDomainRingHom (ZMod K) embL yL) = 0 := by
1376 exact
1378 (Q := Q) (M := M) (K := K) (a := a) (n := n) (d := d)
1379 hd_order hgcd (MonoidAlgebra.mapDomainRingHom (ZMod K) embL yL) hrelProd
1380 have hpoint :
1381 ∀ q : FoxDifferential.CompletedGroupAlgebraQuotientInClass HAb C (OrderDual.toDual UL),
1382 embM
1384 (C := C) (G := HAb) (U := UM) (V := UL) hULUM q) =
1385 finiteProductCyclicReduction Q M K (embL q) := by
1386 intro q
1387 refine Quotient.inductionOn q ?_
1388 intro z
1389 change
1390 quotientKerEmbedding ΦM.toMonoidHom
1391 (QuotientGroup.mk' ΦM.toMonoidHom.ker z) =
1393 (quotientKerEmbedding ΦL.toMonoidHom
1394 (QuotientGroup.mk' ΦL.toMonoidHom.ker z))
1396 change (qU z, red (χ z)) = (qU z, finiteCyclicReduction M K (χ z))
1397 rfl
1398 let qmapLM :
1402 (C := C) (G := HAb) (U := UM) (V := UL) hULUM
1403 have hcomp :
1404 embM.comp qmapLM = (finiteProductCyclicReduction Q M K).comp embL := by
1405 apply MonoidHom.ext
1406 intro q
1407 exact hpoint q
1408 have htransitionMap :
1410 MonoidAlgebra.mapDomainRingHom (ZMod K) qmapLM := by
1411 simpa only [kM, kL, K, qmapLM] using
1412 FoxDifferential.zcCompletedGroupAlgebraTransition_sameCoeff
1413 (C := C) (H := HAb) (coeff := j.1) (U := UM) (V := UL) hULUM
1414 have hmapTransition :
1415 MonoidAlgebra.mapDomainRingHom (ZMod K) embM
1417 MonoidAlgebra.mapDomainRingHom (ZMod K) (finiteProductCyclicReduction Q M K)
1418 (MonoidAlgebra.mapDomainRingHom (ZMod K) embL yL) := by
1419 calc
1420 MonoidAlgebra.mapDomainRingHom (ZMod K) embM
1422 = MonoidAlgebra.mapDomainRingHom (ZMod K) embM
1423 (MonoidAlgebra.mapDomainRingHom (ZMod K) qmapLM yL) := by
1424 rw [htransitionMap]
1425 _ = MonoidAlgebra.mapDomainRingHom (ZMod K) (embM.comp qmapLM) yL := by
1426 rw [← RingHom.comp_apply,
1428 _ = MonoidAlgebra.mapDomainRingHom (ZMod K)
1429 ((finiteProductCyclicReduction Q M K).comp embL) yL := by
1430 rw [hcomp]
1431 _ = MonoidAlgebra.mapDomainRingHom (ZMod K) (finiteProductCyclicReduction Q M K)
1432 (MonoidAlgebra.mapDomainRingHom (ZMod K) embL yL) := by
1433 rw [← RingHom.comp_apply,
1435 have hmapMzero : MonoidAlgebra.mapDomainRingHom (ZMod K) embM yM = 0 := by
1436 have htrans :
1439 rw [← htrans]
1440 exact hmapTransition.trans hzProd
1441 have hyM : yM = 0 := by
1442 exact
1443 (MonoidAlgebra.mapDomain_injective (R := ZMod K)
1445 (by simpa only [MonoidAlgebra.mapDomainRingHom_apply, embM] using hmapMzero)
1446 calc
1450 _ = 0 := by simp only [hyM, map_zero]
1452/-- The non-zero-divisor statement for completed abelianization over the concrete `Σ` class. -/
1454 {sigma : Set ℕ}
1455 {r : ℕ} (X : Fin r → F)
1456 (hFree :
1457 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1459 (SigmaGroup[sigma])) (Fin r) F X)
1460 (i : Fin r) (n : ℤ) (hn : n ≠ 0) :
1461 IsLeftRegular
1462 (FoxDifferential.zcGroupLike
1463 (SigmaGroup[sigma])
1464 (TopologicalAbelianization F)
1468 (fun hQ => hQ)
1469 (fun hQ => hQ)
1470 X hFree i n hn
1472/-- The closed cyclic subgroups generated by two distinct free generators have trivial
1473intersection. -/
1475 {ι : Type v} (X : ι → F)
1476 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
1477 {i j : ι} (hij : i ≠ j) (m : ℕ) :
1479 Subgroup (MaxSolvQuot F m)) ⊓
1481 Subgroup (MaxSolvQuot F m)) = ⊥ := by
1482 classical
1483 let S : Finset ι := {i}
1484 let r : MaxSolvQuot F m →ₜ* MaxSolvQuot F m :=
1486 (hFree.collapseToFinset S) m
1487 let Fix : Subgroup (MaxSolvQuot F m) :=
1488 (r : MaxSolvQuot F m →* MaxSolvQuot F m).eqLocus (MonoidHom.id _)
1489 have hFixClosed : IsClosed (Fix : Set (MaxSolvQuot F m)) := by
1490 change IsClosed {x : MaxSolvQuot F m | r x = x}
1491 exact isClosed_eq r.continuous continuous_id
1492 have hcycFix :
1493 closedSubgroupGenerated ({continuousToMaxSolvQuot F m (X i)} : Set _) ≤ Fix := by
1494 have hself : hFree.collapseToFinset S (X i) = X i := by
1495 exact hFree.collapseToFinset_apply_mem (S := S) (by simp only [Finset.mem_singleton, S])
1496 have hri :
1499 change
1500 QuotientGroup.map
1501 (N := topDerivedTop F m)
1502 (M := topDerivedTop F m)
1503 (f := (hFree.collapseToFinset S : F →* F))
1505 (G := F) (Q := F) (f := hFree.collapseToFinset S) m)
1506 ((QuotientGroup.mk' (topDerivedTop F m)) (X i)) =
1507 (QuotientGroup.mk' (topDerivedTop F m)) (X i)
1508 rw [QuotientGroup.map_mk']
1509 exact congrArg (QuotientGroup.mk' (topDerivedTop F m)) hself
1510 have hsingle :
1511 ({continuousToMaxSolvQuot F m (X i)} : Set (MaxSolvQuot F m)) ⊆ Fix := by
1512 intro y hy
1513 rw [Set.mem_singleton_iff] at hy
1514 subst y
1515 exact hri
1516 exact
1517 Subgroup.topologicalClosure_minimal _
1518 ((Subgroup.closure_le (K := Fix)).2 hsingle) hFixClosed
1519 have hkerClosed : IsClosed (((r : MaxSolvQuot F m →* MaxSolvQuot F m).ker :
1520 Subgroup (MaxSolvQuot F m)) : Set (MaxSolvQuot F m)) := by
1521 change IsClosed {x : MaxSolvQuot F m | r x = 1}
1522 exact isClosed_singleton.preimage r.continuous
1523 have hcycKer :
1525 (r : MaxSolvQuot F m →* MaxSolvQuot F m).ker := by
1526 have hne : hFree.collapseToFinset S (X j) = 1 := by
1527 have hjS : j ∉ S := by
1528 simpa [S] using hij.symm
1529 exact hFree.collapseToFinset_apply_not_mem (S := S) hjS
1530 have hrj :
1531 r (continuousToMaxSolvQuot F m (X j)) = 1 := by
1532 change
1533 QuotientGroup.map
1534 (N := topDerivedTop F m)
1535 (M := topDerivedTop F m)
1536 (f := (hFree.collapseToFinset S : F →* F))
1538 (G := F) (Q := F) (f := hFree.collapseToFinset S) m)
1539 ((QuotientGroup.mk' (topDerivedTop F m)) (X j)) = 1
1540 rw [QuotientGroup.map_mk']
1541 simpa using congrArg (QuotientGroup.mk' (topDerivedTop F m)) hne
1542 have hsingle :
1543 ({continuousToMaxSolvQuot F m (X j)} : Set (MaxSolvQuot F m)) ⊆
1544 (r : MaxSolvQuot F m →* MaxSolvQuot F m).ker := by
1545 intro y hy
1546 rw [Set.mem_singleton_iff] at hy
1547 subst y
1548 exact hrj
1549 exact
1550 Subgroup.topologicalClosure_minimal _
1551 ((Subgroup.closure_le
1552 (K := (r : MaxSolvQuot F m →* MaxSolvQuot F m).ker)).2 hsingle) hkerClosed
1553 rw [Subgroup.eq_bot_iff_forall]
1554 intro z hz
1555 have hfix : z ∈ Fix := hcycFix hz.1
1556 have hker : z ∈ (r : MaxSolvQuot F m →* MaxSolvQuot F m).ker := hcycKer hz.2
1557 change r z = z at hfix
1558 change r z = 1 at hker
1559 calc
1560 z = r z := hfix.symm
1561 _ = 1 := hker
1563omit hCVariety hCIsomClosed in
1564/-- Transfer a finite basis family to the finite-rank case indexed by `Fin r`. -/
1566 {ι : Type v} [Fintype ι] (X : ι → F)
1567 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X) :
1568 let r : ℕ := Fintype.card ι
1569 let e : ι ≃ Fin r := Fintype.equivFin ι
1570 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) (Fin r) F (fun k : Fin r => X (e.symm k)) := by
1571 classical
1572 let r : ℕ := Fintype.card ι
1573 let e : ι ≃ Fin r := Fintype.equivFin ι
1574 exact
1575 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet.precompEquiv
1576 hFree e.symm
1578omit hCVariety hCIsomClosed in
1579/-- A finite-rank free pro-`Σ` group splits as the free pro-`Σ` product of the retract generated
1580by one chosen basis element and the retract generated by the complementary finite set. -/
1582 {sigma : Set ℕ} {r : ℕ} (X : Fin (r + 2) → F)
1583 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1585 (Fin (r + 2)) F X)
1586 (i : Fin (r + 2)) :
1587 let S : Finset (Fin (r + 2)) := {i}
1588 let T : Finset (Fin (r + 2)) := Finset.univ.erase i
1589 IsFreeProSigmaProduct[sigma]
1590 (hFree.collapseToFinsetInclusion S)
1591 (hFree.collapseToFinsetInclusion T) := by
1592 classical
1593 let S : Finset (Fin (r + 2)) := {i}
1594 let T : Finset (Fin (r + 2)) := Finset.univ.erase i
1595 let A : Type u := hFree.FinsetSupportRetract S
1596 let P : Type u := hFree.FinsetSupportRetract T
1597 let ιA : A →ₜ* F := hFree.collapseToFinsetInclusion S
1598 let ιP : P →ₜ* F := hFree.collapseToFinsetInclusion T
1599 have hιA_basis (s : S) :
1600 ιA (hFree.finsetSupportBasis S s) = X s.1 := rfl
1601 have hιP_basis (t : T) :
1602 ιP (hFree.finsetSupportBasis T t) = X t.1 := rfl
1603 change IsFreeProSigmaProduct[sigma] ιA ιP
1604 refine ⟨hFree.isProC, ?_⟩
1605 intro K _ _ _ hK φA φP
1606 let φ : Fin (r + 2) → K := fun j =>
1607 if hj : j ∈ S then
1608 φA (hFree.finsetSupportBasis S ⟨j, hj⟩)
1609 else
1610 φP (hFree.finsetSupportBasis T ⟨j, by
1611 simp only [Finset.mem_singleton, Finset.mem_erase, ne_eq, Finset.mem_univ, and_true, S, T] at hj ⊢
1612 exact hj⟩)
1613 have hφconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := K) φ :=
1614 ProCGroups.FreeProC.FamilyConvergesToOne.of_finite_domain (G := K) φ
1615 rcases
1616 hFree.existsUnique_liftHom_of_convergesToOne_of_finiteGroupClass
1617 (SigmaGroup[sigma])
1618 (ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed sigma)
1619 (ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed sigma)
1620 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed sigma)
1621 hK φ hφconv with
1622 ⟨ψ, hψ, hψuniq⟩
1623 refine ⟨ψ, ?_, ?_⟩
1624 · constructor
1625 · let hKprof : ProCGroups.IsProfiniteGroup K :=
1627 (SigmaGroup[sigma]) hK
1628 letI : T2Space K := hKprof.t2Space
1629 apply
1631 (hFree.isFreeProCGroupOnConvergingSet_finsetSupportBasis S).generates_range
1632 rintro _ ⟨s, rfl⟩
1633 have hψi := hψ i
1634 change ψ (ιA (hFree.finsetSupportBasis S s)) =
1635 φA (hFree.finsetSupportBasis S s)
1636 rw [hιA_basis]
1637 have hsEq : (s : Fin (r + 2)) = i :=
1638 Finset.mem_singleton.mp s.2
1639 have hsSubtype : s = (⟨i, by simp only [Finset.mem_singleton, S]⟩ : S) := Subtype.ext hsEq
1640 rw [hsSubtype]
1641 simpa [φ, S] using hψi
1642 · let hKprof : ProCGroups.IsProfiniteGroup K :=
1644 (SigmaGroup[sigma]) hK
1645 letI : T2Space K := hKprof.t2Space
1646 apply
1648 (hFree.isFreeProCGroupOnConvergingSet_finsetSupportBasis T).generates_range
1649 rintro _ ⟨t, rfl⟩
1650 have htS : (t : Fin (r + 2)) ∉ S := by
1651 have hne : (t : Fin (r + 2)) ≠ i := by
1652 exact (Finset.mem_erase.mp t.2).1
1653 simpa [S] using hne
1654 have hψt := hψ (t : Fin (r + 2))
1655 change ψ (ιP (hFree.finsetSupportBasis T t)) =
1656 φP (hFree.finsetSupportBasis T t)
1657 rw [hιP_basis]
1658 have htNe : (t : Fin (r + 2)) ≠ i := by
1659 simpa [S] using htS
1660 simpa [φ, S, htNe] using hψt
1661 · intro χ hχ
1662 apply hψuniq χ
1663 intro j
1664 by_cases hj : j ∈ S
1665 · have hleft := congrArg (fun f : A →ₜ* K =>
1666 f (hFree.finsetSupportBasis S ⟨j, hj⟩)) hχ.1
1667 change χ (ιA (hFree.finsetSupportBasis S ⟨j, hj⟩)) =
1668 φA (hFree.finsetSupportBasis S ⟨j, hj⟩) at hleft
1669 rw [hιA_basis] at hleft
1670 have hjEq : j = i := by
1671 simpa [S] using hj
1672 simpa [φ, S, hjEq] using hleft
1673 · have hjT : j ∈ T := by
1674 have hne : j ≠ i := by
1675 simpa [S] using hj
1676 exact Finset.mem_erase.mpr ⟨hne, by simp only [Finset.mem_univ]⟩
1677 have hright := congrArg (fun f : P →ₜ* K =>
1678 f (hFree.finsetSupportBasis T ⟨j, hjT⟩)) hχ.2
1679 change χ (ιP (hFree.finsetSupportBasis T ⟨j, hjT⟩)) =
1680 φP (hFree.finsetSupportBasis T ⟨j, hjT⟩) at hright
1681 rw [hιP_basis] at hright
1682 have hjNe : j ≠ i := by
1683 simpa [S] using hj
1684 simpa [φ, S, hjNe] using hright
1687 {ι : Type v} (X : ι → F)
1688 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1690 (i : ι) (m : ℕ) :
1692 Subgroup (MaxSolvQuot F m)) ⊓
1693 topDerivedTop (MaxSolvQuot F m) 1 = ⊥ := by
1694 classical
1695 let S : Finset ι := {i}
1696 let R : Type u := hFree.FinsetSupportRetract S
1697 let B : S → R := hFree.finsetSupportBasis S
1698 let iS : S := ⟨i, by simp only [Finset.mem_singleton, S]⟩
1699 let QF : Type u := MaxSolvQuot F m
1700 let QR : Type u := MaxSolvQuot R m
1701 let xQ : QF := continuousToMaxSolvQuot F m (X i)
1702 let xR : QR := continuousToMaxSolvQuot R m (B iS)
1703 let ρ : QF →ₜ* QR := finsetSupportRangeQuot X hFree S m
1704 let ιQ : QR →ₜ* QF := finsetSupportInclusionQuot X hFree S m
1705 let collapse : QF →ₜ* QF := collapseToFinsetQuot X hFree S m
1706 have hxρ : ρ xQ = xR := by
1707 have hxRange : hFree.collapseToFinsetRange S (X i) = B iS := by
1708 apply Subtype.ext
1709 change (hFree.collapseToFinset S (X i) : F) = X i
1710 simpa [B, ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet.collapseToFinsetRange,
1711 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet.finsetSupportBasis] using
1712 hFree.collapseToFinset_apply_mem (S := S) (by simp only [Finset.mem_singleton, S])
1713 change
1717 exact congrArg (continuousToMaxSolvQuot R m) hxRange
1718 have hcomp : ∀ z : QF, ιQ (ρ z) = collapse z := by
1719 intro z
1720 obtain ⟨a, rfl⟩ := continuousToMaxSolvQuot_surjective (G := F) m z
1721 have hcompF :
1722 (hFree.collapseToFinsetInclusion S).comp (hFree.collapseToFinsetRange S) =
1723 hFree.collapseToFinset S := by
1724 ext a
1725 rfl
1726 change
1731 exact congrArg
1732 (fun y : F => continuousToMaxSolvQuot F m y)
1733 (congrArg (fun f : F →ₜ* F => f a) hcompF)
1734 let Fix : Subgroup QF := (collapse : QF →* QF).eqLocus (MonoidHom.id QF)
1735 have hFixClosed : IsClosed (Fix : Set QF) := by
1736 change IsClosed {z : QF | collapse z = z}
1737 exact isClosed_eq collapse.continuous continuous_id
1738 have hcycFix :
1739 closedSubgroupGenerated ({xQ} : Set QF) ≤ Fix := by
1740 have hself : hFree.collapseToFinset S (X i) = X i := by
1741 exact hFree.collapseToFinset_apply_mem (S := S) (by simp only [Finset.mem_singleton, S])
1742 have hri : collapse xQ = xQ := by
1743 change
1744 QuotientGroup.map
1745 (N := topDerivedTop F m)
1746 (M := topDerivedTop F m)
1747 (f := (hFree.collapseToFinset S : F →* F))
1749 (G := F) (Q := F) (f := hFree.collapseToFinset S) m)
1750 ((QuotientGroup.mk' (topDerivedTop F m)) (X i)) =
1751 (QuotientGroup.mk' (topDerivedTop F m)) (X i)
1752 rw [QuotientGroup.map_mk']
1753 exact congrArg (QuotientGroup.mk' (topDerivedTop F m)) hself
1754 have hsingle : ({xQ} : Set QF) ⊆ Fix := by
1755 intro z hz
1756 rw [Set.mem_singleton_iff] at hz
1757 subst z
1758 exact hri
1759 exact
1760 Subgroup.topologicalClosure_minimal _
1761 ((Subgroup.closure_le (K := Fix)).2 hsingle) hFixClosed
1762 have hFreeR :
1763 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1765 hFree.isFreeProCGroupOnConvergingSet_finsetSupportBasis S
1766 have hRangeB : Set.range B = ({B iS} : Set R) := by
1767 ext y
1768 constructor
1769 · rintro ⟨s, rfl⟩
1770 have hsEq : (s : ι) = i := Finset.mem_singleton.mp s.2
1771 have hsSubtype : s = iS := Subtype.ext hsEq
1772 simp only [hsSubtype, Set.mem_singleton_iff, B]
1773 · intro hy
1774 rcases Set.mem_singleton_iff.mp hy with rfl
1775 exact ⟨iS, rfl⟩
1776 have hgenR :
1777 ProCGroups.Generation.TopologicallyGenerates (G := R) ({B iS} : Set R) := by
1778 simpa [hRangeB] using hFreeR.generates_range
1779 have hgenQR :
1780 ProCGroups.Generation.TopologicallyGenerates (G := QR) ({xR} : Set QR) := by
1781 let qR : R →ₜ* QR := continuousToMaxSolvQuot R m
1782 have hsurj : Function.Surjective qR := by
1783 simpa [qR, QR] using continuousToMaxSolvQuot_surjective (G := R) m
1784 have himage :
1786 (qR '' ({B iS} : Set R)) := by
1787 exact
1789 (f := qR.toMonoidHom) qR.continuous hsurj hgenR
1790 have hImageEq : qR '' ({B iS} : Set R) = ({xR} : Set QR) := by
1791 ext y
1792 constructor
1793 · rintro ⟨z, hz, rfl⟩
1794 rcases Set.mem_singleton_iff.mp hz with rfl
1795 change qR (B iS) = xR
1796 rfl
1797 · intro hy
1798 rcases Set.mem_singleton_iff.mp hy with rfl
1799 refine ⟨B iS, by simp only [Set.mem_singleton_iff], ?_⟩
1800 change qR (B iS) = xR
1801 rfl
1802 simpa [hImageEq] using himage
1803 have hQRder : topDerivedTop QR 1 = ⊥ :=
1805 (Q := QR) xR hgenQR
1806 rw [Subgroup.eq_bot_iff_forall]
1807 intro z hz
1808 have hfix : z ∈ Fix := by
1809 simpa [xQ] using hcycFix hz.1
1810 have hzρder : ρ z ∈ topDerivedTop QR 1 := by
1811 exact topDerived_map_le (f := ρ) (m := 1) ⟨z, hz.2, rfl⟩
1812 have hzρ_one : ρ z = 1 := by
1813 change ρ z ∈ topDerivedTop QR 1 at hzρder
1814 rw [hQRder] at hzρder
1815 exact Subgroup.mem_bot.mp hzρder
1816 have hcollapse_one : collapse z = 1 := by
1817 calc
1818 collapse z = ιQ (ρ z) := (hcomp z).symm
1819 _ = 1 := by simp only [hzρ_one, map_one]
1820 change collapse z = z at hfix
1821 calc
1822 z = collapse z := hfix.symm
1823 _ = 1 := hcollapse_one
1825/-- Finite-rank Theorem 1.5 inputs satisfy the cyclic-join containment supplied by
1826Proposition 1.3. -/
1828 {sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p)
1829 {r m : ℕ} (X : Fin (r + 2) → F)
1830 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1832 (Fin (r + 2)) F X)
1833 (i : Fin (r + 2)) (hm : 2 ≤ m) (n : ℤ) (hn : n ≠ 0) :
1836 Subgroup (MaxSolvQuot F m)) ⊔
1837 topDerivedTop (MaxSolvQuot F m) (m - 1) := by
1838 classical
1839 let S : Finset (Fin (r + 2)) := {i}
1840 let T : Finset (Fin (r + 2)) := Finset.univ.erase i
1841 let A : Type u := hFree.FinsetSupportRetract S
1842 let P : Type u := hFree.FinsetSupportRetract T
1843 let ιA : A →ₜ* F := hFree.collapseToFinsetInclusion S
1844 let ιP : P →ₜ* F := hFree.collapseToFinsetInclusion T
1845 let xA : A := hFree.finsetSupportBasis S ⟨i, by simp only [Finset.mem_singleton, S]⟩
1846 have hΩ : IsFreeProSigmaProduct[sigma] ιA ιP := by
1847 simpa [S, T, ιA, ιP] using
1849 (F := F) (sigma := sigma) (r := r) X hFree i
1850 have hAProSigma : ProSigmaGroup[sigma] A := by
1851 simpa [A, S] using hFree.isProCGroup_finsetSupportRetract S
1852 have hxgen : ProCGroups.Generation.TopologicallyGenerates (G := A) ({xA} : Set A) := by
1853 have hFreeS :=
1854 hFree.isFreeProCGroupOnConvergingSet_finsetSupportBasis S
1855 have hRange :
1856 Set.range (hFree.finsetSupportBasis S) = ({xA} : Set A) := by
1857 ext y
1858 constructor
1859 · rintro ⟨s, rfl⟩
1860 have hsEq : (s : Fin (r + 2)) = i :=
1861 Finset.mem_singleton.mp s.2
1862 have hsSubtype : s = (⟨i, by simp only [Finset.mem_singleton, S]⟩ : S) := Subtype.ext hsEq
1863 simp only [hsSubtype, Set.mem_singleton_iff, xA]
1864 · intro hy
1865 rcases Set.mem_singleton_iff.mp hy with rfl
1866 exact ⟨⟨i, by simp only [Finset.mem_singleton, S]⟩, rfl⟩
1867 simpa [hRange, xA] using hFreeS.generates_range
1868 have hιAx : ιA xA = X i := rfl
1869 have hxzn : xA ^ n ≠ 1 :=
1870 (hFree.isFreeProCGroupOnConvergingSet_finsetSupportBasis S).generator_zpow_ne_one_of_sigma
1871 hsigma
1872 ⟨i, by simp only [Finset.mem_singleton, S]⟩ n hn
1873 have hle :=
1875 ιA ιP hΩ hAProSigma xA hxgen m hm n hxzn
1876 simpa [S, T, A, P, ιA, ιP, xA, hιAx, map_zpow] using hle
1878/-- The non-zero-divisor lemma in the finite quotient class induced by `proSigmaProC`.
1879This is the coefficient class used by the CES finite-coordinate APIs. -/
1881 {sigma : Set ℕ}
1882 {r : ℕ} (X : Fin r → F)
1883 (hFree :
1884 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1886 (SigmaGroup[sigma])) (Fin r) F X)
1887 (i : Fin r) (n : ℤ) (hn : n ≠ 0) :
1888 IsLeftRegular
1889 (FoxDifferential.zcGroupLike
1890 (ProCGroups.ProC.proSigmaProC.{u} sigma).finiteQuotientClass
1891 (TopologicalAbelianization F)
1894 (ProCGroups.ProC.proSigmaProC.{u} sigma).finiteQuotientClass
1895 (fun hQ =>
1897 (fun hQ => by
1900 X hFree i n hn
1902omit hCVariety hCIsomClosed in
1903/-- The finite-rank rank-one case of Theorem 1.5. -/
1905 (X : Fin 1 → F)
1906 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) (Fin 1) F X)
1907 (m : ℕ) (n : ℤ) :
1910 let x : F := X 0
1911 let q : F →ₜ* MaxSolvQuot F m := continuousToMaxSolvQuot F m
1912 let qx : MaxSolvQuot F m := q x
1916 (N := topDerivedTop F m) (by infer_instance)
1917 letI : CompactSpace (MaxSolvQuot F m) := hQprof.compactSpace
1918 letI : T2Space (MaxSolvQuot F m) := hQprof.t2Space
1919 have hRangeX : Set.range X = ({x} : Set F) := by
1920 ext y
1921 constructor
1922 · rintro ⟨j, rfl⟩
1923 have hj : j = 0 := by
1924 fin_cases j
1925 rfl
1926 simp only [Fin.isValue, hj, Set.mem_singleton_iff, x]
1927 · intro hy
1928 rcases Set.mem_singleton_iff.mp hy with rfl
1929 exact ⟨0, rfl⟩
1930 have hgenFset : ProCGroups.Generation.TopologicallyGenerates (G := F) ({x} : Set F) := by
1931 have hXgen := hFree.generates_range
1932 simpa [hRangeX] using hXgen
1933 have hgenQset :
1935 ({qx} : Set (MaxSolvQuot F m)) := by
1936 have hsurj : Function.Surjective q := continuousToMaxSolvQuot_surjective (G := F) m
1937 have himage :
1939 (q '' ({x} : Set F)) := by
1940 exact
1942 (f := q.toMonoidHom) q.continuous hsurj hgenFset
1943 have hImageEq : q '' ({x} : Set F) = ({qx} : Set (MaxSolvQuot F m)) := by
1944 ext y
1945 constructor
1946 · rintro ⟨z, hz, rfl⟩
1947 rcases Set.mem_singleton_iff.mp hz with rfl
1948 simp only [Set.mem_singleton_iff, qx]
1949 · intro hy
1950 rcases Set.mem_singleton_iff.mp hy with rfl
1951 exact ⟨x, by simp only [Set.mem_singleton_iff], rfl⟩
1952 simpa [hImageEq] using himage
1953 simpa [x, q, qx, map_zpow] using
1955 (G := MaxSolvQuot F m) qx n hgenQset
1957/-- The pro-`Σ` finite-rank metabelian case of Theorem 1.5. -/
1959 {sigma : Set ℕ} (_hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p)
1960 {r : ℕ} (X : Fin (r + 2) → F)
1961 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
1963 (Fin (r + 2)) F X)
1964 (i : Fin (r + 2)) (n : ℤ) (hn : n ≠ 0) :
1967 apply le_antisymm
1968 · intro g hg
1969 let q : F →ₜ* MaxSolvQuot F 2 := continuousToMaxSolvQuot F 2
1970 let x : MaxSolvQuot F 2 := q (X i)
1971 let Cx : Subgroup (MaxSolvQuot F 2) :=
1973 let D : Subgroup (MaxSolvQuot F 2) :=
1975 have hqpow : q ((X i) ^ n) = x ^ n := by
1976 simp only [x, map_zpow]
1977 have hjoin : g ∈ Cx ⊔ D := by
1978 have hle :=
1980 (F := F) _hsigma X hFree i (m := 2) (by decide) n hn
1981 have hgpow : g ∈ centralizerOf (x ^ n) := by
1982 simpa only [hqpow] using hg
1983 exact hle hgpow
1984 have hDnormal : D.Normal := by
1985 change (topDerivedTop (MaxSolvQuot F 2) 1).Normal
1986 infer_instance
1987 letI : D.Normal := hDnormal
1988 rcases (Subgroup.mem_sup_of_normal_right (s := Cx) (t := D)).1 hjoin with
1989 ⟨c, hc, d, hd, hcd⟩
1990 have hcCent : c ∈ centralizerOf (x ^ n) :=
1992 (G := MaxSolvQuot F 2) (x := x) n (by simpa [Cx] using hc)
1993 have hcdCent : c * d ∈ centralizerOf (x ^ n) := by
1994 rw [hcd]
1995 simpa only [hqpow] using hg
1996 have hdCent : d ∈ centralizerOf (x ^ n) :=
1998 have hd_eq_one : d = 1 := by
1999 classical
2002 (SigmaGroup[sigma]) hFree.isProC
2003 letI : CompactSpace F := hFprof.compactSpace
2004 letI : T2Space F := hFprof.t2Space
2007 (G := F) hFprof (N := topDerivedTop F 2) (by infer_instance)
2008 letI : T2Space (MaxSolvQuot F 2) := hQprof.t2Space
2009 have hmap1 :
2010 (topDerivedTop F 1).map (q : F →* MaxSolvQuot F 2) =
2012 exact
2016 have hdmap : d ∈ (topDerivedTop F 1).map (q : F →* MaxSolvQuot F 2) := by
2017 rw [hmap1]
2018 simpa [D] using hd
2019 rcases hdmap with ⟨a, ha_der, hqa⟩
2020 let HAb : Type u := TopologicalAbelianization F
2022 have hψa : ψ a = 1 := by
2027 exact ha_der
2028 have hcommQ : ⁅x ^ n, d⁆ = 1 := by
2029 exact
2030 commutatorElement_eq_one_iff_mul_comm.2
2031 ((mem_centralizerOf_iff.mp hdCent).symm)
2032 have hqcomm : q ⁅(X i) ^ n, a⁆ = 1 := by
2033 rw [map_commutatorElement]
2034 rw [map_zpow]
2035 have hqa' : q a = d := by simpa using hqa
2036 rw [hqa']
2037 simpa [x] using hcommQ
2038 have hcomm_der2 : ⁅(X i) ^ n, a⁆ ∈ topDerivedTop F 2 :=
2040 (x := ⁅(X i) ^ n, a⁆)).1 hqcomm
2041 have hψcomm : ψ ⁅(X i) ^ n, a⁆ = 1 := by
2042 change
2044 change ⁅(X i) ^ n, a⁆ ∈ ProCGroups.ProC.ProfiniteKernelSubgroup
2047 exact (topDerivedTop_antitone (G := F) (by decide : 1 ≤ 2)) hcomm_der2
2048 let ProC := ProCGroups.ProC.proSigmaProC.{u} sigma
2049 let C : ProCGroups.FiniteGroupClass.{u} := ProC.finiteQuotientClass
2051 have hcommKernel :
2052 (⟨⁅(X i) ^ n, a⁆, hψcomm⟩ : ProCGroups.ProC.ProfiniteKernelSubgroup ψ) ∈
2055 (G := F) hψcomm).1 hcomm_der2
2056 have hboundary :=
2058 (G := F) (H := HAb) C ψ hcommKernel
2059 have hδcomm_zero : δ ⁅(X i) ^ n, a⁆ = 0 := by
2060 change Multiplicative.ofAdd (δ ⁅(X i) ^ n, a⁆) = 1 at hboundary
2061 simpa using congrArg Multiplicative.toAdd hboundary
2062 have hδcomm_formula :
2063 δ ⁅(X i) ^ n, a⁆ =
2064 (FoxDifferential.zcGroupLike C HAb (ψ ((X i) ^ n)) - 1) • δ a := by
2065 exact
2067 C ψ.toMonoidHom ((X i) ^ n) a hψa
2068 have hsmul_zero :
2069 (FoxDifferential.zcGroupLike C HAb
2071 δ a = 0 := by
2072 have hψ_pow :
2073 ψ ((X i) ^ n) =
2075 change
2078 simp only [map_zpow]
2079 rw [hδcomm_formula] at hδcomm_zero
2080 simpa only [hψ_pow] using hδcomm_zero
2081 let E :=
2083 (F := F) X hFree
2084 have hE_smul_zero : E ((FoxDifferential.zcGroupLike C HAb
2086 δ a) = 0 := by
2087 rw [hsmul_zero]
2088 simp only [ContinuousMonoidHom.coe_toMonoidHom, map_zero]
2089 have hE_delta_zero : E (δ a) = 0 := by
2090 funext j
2091 have hj := congrFun hE_smul_zero j
2092 have hreg :=
2094 (F := F) X hFree i n hn
2095 exact
2096 (isLeftRegular_iff_right_eq_zero_of_mul.mp hreg)
2097 (E (δ a) j)
2098 (by
2099 simpa only [LinearMap.map_smul, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
2100 using hj)
2101 have ha_der2 : a ∈ topDerivedTop F 2 :=
2103 (F := F) X hFree hψa hE_delta_zero
2104 have hqa_one : q a = 1 :=
2105 (continuousToMaxSolvQuot_eq_one_iff (G := F) (m := 2) (x := a)).2 ha_der2
2106 calc
2107 d = q a := hqa.symm
2108 _ = 1 := hqa_one
2109 have hg_eq_c : g = c := by
2110 calc
2111 g = c * d := hcd.symm
2112 _ = c := by rw [hd_eq_one, mul_one]
2113 rw [hg_eq_c]
2114 simpa only [Cx] using hc
2115 · simpa [map_zpow] using
2117 (G := MaxSolvQuot F 2) (continuousToMaxSolvQuot F 2 (X i)) n)
2119/-- The Reidemeister--Schreier input used in the induction step for Section 1.
2121For an open subgroup of a finite-rank free pro-`C` group, if the first positive power `x^N` of a
2122basis element `x` lies in the subgroup, one can choose a finite-rank Reidemeister--Schreier basis
2123whose image contains `x^N`. The hypothesis `hpow_ne` is the nontriviality input actually needed:
2124it supplies, from outside this lemma, that no positive power of the free generator is trivial. -/
2127 (hcyc :
2128 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
2129 C A ∧ IsCyclic A ∧ Nontrivial A)
2130 {X : Type u} [Finite X]
2131 {ι : X → F}
2132 (hF : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2134 (H : OpenSubgroup F) (x : X)
2135 (hpow_ne : ∀ N : ℕ, 0 < N → (ι x) ^ N ≠ 1) :
2136 ∃ N : ℕ, ∃ _hN : 0 < N,
2137 ∃ hpow : (ι x) ^ N ∈ (H : Subgroup F),
2138 (∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) ∧
2139 ∃ Fdata : ProCGroups.FreeProC.FreeProCGroupOnConvergingSetData
2141 ∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
2142 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
2143 Set.range (e ∘ Fdata.inclusion) ∧
2144 Cardinal.mk Fdata.basis =
2145 (_root_.ReidemeisterSchreier.Schreier.rankTransform
2146 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := by
2147 classical
2150 letI : CompactSpace F := hFprof.compactSpace
2151 letI : T2Space F := hFprof.t2Space
2152 letI : Finite (Set.range ι) := (Set.finite_range ι).to_subtype
2153 letI : DiscreteTopology (Set.range ι) :=
2154 DiscreteTopology.of_finite_of_isClosed_singleton fun _ => isClosed_singleton
2155 let P : ℕ → Prop := fun N => 0 < N ∧ (ι x) ^ N ∈ (H : Subgroup F)
2156 have hP : ∃ N : ℕ, P N :=
2158 let N : ℕ := Nat.find hP
2159 have hNpow : P N := Nat.find_spec hP
2160 have hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F) := by
2161 intro m hm hlt hmH
2162 exact Nat.find_min hP hlt ⟨hm, hmH⟩
2163 have hVar : ProCGroups.FiniteGroupClass.Variety C := Fact.out
2164 have hIso : ProCGroups.FiniteGroupClass.IsomClosed C := hCIsomClosed.out
2166 rcases
2168 (C := C) hVar hIso hExt hcyc hF H x hNpow.1 hNpow.2
2169 (hpow_ne N hNpow.1) hmin with
2170 ⟨Fdata, e, hpower_range, hcard⟩
2171 exact ⟨N, hNpow.1, hNpow.2, hmin, Fdata, e, hpower_range, hcard⟩
2173/-- The pro-`Σ` finite-rank induction step for Theorem 1.5. -/
2175 {sigma : Set ℕ} (_hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p)
2176 {r m : ℕ} (X : Fin (r + 2) → F)
2177 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2179 (Fin (r + 2)) F X)
2180 (hm : 3 ≤ m)
2181 (ih :
2182 ∀ {F' : Type u} [TopologicalSpace F'] [Group F'] [IsTopologicalGroup F'],
2183 ∀ {r' : ℕ} (Y : Fin r' → F'),
2184 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2186 (Fin r') F' Y →
2187 ∀ i : Fin r', ∀ n : ℤ, n ≠ 0 →
2188 centralizerOf (continuousToMaxSolvQuot F' (m - 1) ((Y i) ^ n)) =
2190 (i : Fin (r + 2)) (n : ℤ) (hn : n ≠ 0) :
2193 apply le_antisymm
2194 · intro g hg
2195 let q : F →ₜ* MaxSolvQuot F m := continuousToMaxSolvQuot F m
2196 let x : MaxSolvQuot F m := q (X i)
2197 let Cx : Subgroup (MaxSolvQuot F m) :=
2199 let D : Subgroup (MaxSolvQuot F m) :=
2201 have hqpow : q ((X i) ^ n) = x ^ n := by
2202 simp only [x, map_zpow]
2203 have hjoin : g ∈ Cx ⊔ D := by
2204 have hle :=
2206 (F := F) _hsigma X hFree i (m := m) (Nat.le_trans (by decide) hm) n hn
2207 have hgpow : g ∈ centralizerOf (x ^ n) := by
2208 simpa only [hqpow] using hg
2209 exact hle hgpow
2210 have hDnormal : D.Normal := by
2211 change (topDerivedTop (MaxSolvQuot F m) (m - 1)).Normal
2212 infer_instance
2213 letI : D.Normal := hDnormal
2214 rcases (Subgroup.mem_sup_of_normal_right (s := Cx) (t := D)).1 hjoin with
2215 ⟨c, hc, d, hd, hcd⟩
2216 have hcCent : c ∈ centralizerOf (x ^ n) :=
2218 (G := MaxSolvQuot F m) (x := x) n (by simpa [Cx] using hc)
2219 have hcdCent : c * d ∈ centralizerOf (x ^ n) := by
2220 rw [hcd]
2221 simpa only [hqpow] using hg
2222 have hdCent : d ∈ centralizerOf (x ^ n) :=
2224 have hd_eq_one : d = 1 := by
2225 classical
2228 (SigmaGroup[sigma]) hFree.isProC
2229 letI : CompactSpace F := hFprof.compactSpace
2230 letI : T2Space F := hFprof.t2Space
2233 (G := F) hFprof (N := topDerivedTop F m) (by infer_instance)
2234 letI : CompactSpace (MaxSolvQuot F m) := hQprof.compactSpace
2235 letI : T2Space (MaxSolvQuot F m) := hQprof.t2Space
2236 letI : TotallyDisconnectedSpace (MaxSolvQuot F m) :=
2237 hQprof.totallyDisconnectedSpace
2238 have hQm : topDerivedTop (MaxSolvQuot F m) m = ⊥ := by
2239 have hmapm :
2240 (topDerivedTop F m).map (q : F →* MaxSolvQuot F m) =
2242 exact
2246 rw [← hmapm]
2247 refine
2248 (Subgroup.map_eq_bot_iff
2249 (f := (q : F →* MaxSolvQuot F m)) (H := topDerivedTop F m)).2 ?_
2250 intro y hy
2251 exact (MonoidHom.mem_ker).2
2252 ((continuousToMaxSolvQuot_eq_one_iff (G := F) (m := m) (x := y)).2 hy)
2253 exact
2255 (Q := MaxSolvQuot F m) hm hQm (by
2256 intro H hH
2257 let Q : Type u := MaxSolvQuot F m
2258 let Hopen : OpenSubgroup Q := H.toOpenSubgroup
2259 let Hpre : OpenSubgroup F := preimageOpenSubgroup q Hopen
2260 let qH : ↥(Hpre : Subgroup F) →ₜ* ↥(H : Subgroup Q) := by
2261 simpa [Hpre, Hopen, Q] using
2262 (q.restrictPreimage (H : Subgroup Q))
2263 have hmap_last :
2264 (topDerivedTop F (m - 1)).map (q : F →* Q) =
2265 topDerivedTop Q (m - 1) := by
2266 exact
2270 have hdmap : d ∈ (topDerivedTop F (m - 1)).map (q : F →* Q) := by
2271 rw [hmap_last]
2272 simpa [D, Q] using hd
2273 rcases hdmap with ⟨a, ha_der, hqa⟩
2274 have hm_pred_one : 1 ≤ m - 1 := by omega
2275 have hm_one : 1 ≤ m := le_trans (by decide : 1 ≤ 3) hm
2276 have hF1_le_Hpre : topDerivedTop F 1 ≤ (Hpre : Subgroup F) := by
2277 intro y hy
2278 change q y ∈ (H : Subgroup Q)
2279 exact hH ((topDerivedTop_le_comap (f := q) (m := 1)) hy)
2280 have hD_le_one : topDerivedTop Q (m - 1) ≤ topDerivedTop Q 1 := by
2281 exact topDerivedTop_antitone (G := Q) hm_pred_one
2282 have hdH : d ∈ (H : Subgroup Q) :=
2283 hH (hD_le_one (by simpa [D, Q] using hd))
2284 have haHpre : a ∈ (Hpre : Subgroup F) := by
2285 change q a ∈ (H : Subgroup Q)
2286 have hqa' : q a = d := by simpa using hqa
2287 rw [hqa']
2288 exact hdH
2289 let aH : ↥(Hpre : Subgroup F) := ⟨a, haHpre⟩
2290 have hFm_le_Hpre :
2292 (topDerivedTop ↥(Hpre : Subgroup F) (m - 1)).map
2293 (Subgroup.subtype (Hpre : Subgroup F)) :=
2295 (G := F) Hpre hm_one hF1_le_Hpre
2296 have haH_der_one : aH ∈ topDerivedTop ↥(Hpre : Subgroup F) 1 := by
2297 have hm_pred_pred_one : 1 ≤ (m - 1) - 1 := by
2298 omega
2299 have ha_map :
2300 a ∈ (topDerivedTop ↥(Hpre : Subgroup F) ((m - 1) - 1)).map
2301 (Subgroup.subtype (Hpre : Subgroup F)) :=
2303 (G := F) Hpre hm_pred_one hF1_le_Hpre ha_der
2304 rcases ha_map with ⟨b, hb, hba⟩
2305 have hb1 : b ∈ topDerivedTop ↥(Hpre : Subgroup F) 1 :=
2306 topDerivedTop_antitone (G := ↥(Hpre : Subgroup F)) hm_pred_pred_one hb
2307 have hb_eq : b = aH := by
2308 apply Subtype.ext
2309 simpa [aH] using hba
2310 simpa [hb_eq] using hb1
2311 have haH_last : aH ∈ topDerivedTop ↥(Hpre : Subgroup F) (m - 1) := by
2312 letI : Fact (ProCGroups.FiniteGroupClass.ExtensionClosed (SigmaGroup[sigma])) :=
2313 ⟨ProCGroups.FiniteGroupClass.sigmaGroup_extensionClosed sigma⟩
2314 let XU : ULift.{u} (Fin (r + 2)) → F := fun k => X k.down
2315 have hFreeU :
2316 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2318 (ULift.{u} (Fin (r + 2))) F XU := by
2319 simpa [XU] using
2320 hFree.precompEquiv (Equiv.ulift : ULift.{u} (Fin (r + 2)) ≃ Fin (r + 2))
2321 rcases
2323 (C := SigmaGroup[sigma])
2324 (hcyc := ProCGroups.FiniteGroupClass.sigmaGroup_nontrivialCyclic
2325 (sigma := sigma) _hsigma)
2326 (F := F) (X := ULift.{u} (Fin (r + 2))) (ι := XU)
2327 hFreeU Hpre (ULift.up i)
2328 (fun N hN =>
2329 by
2330 simpa [XU] using
2331 hFree.generator_pow_ne_one_of_sigma _hsigma i N hN) with
2332 ⟨N, hNpos, hpow, _hmin, Fdata, e, hpower_range, hcard⟩
2333 have hFdataFinite : Finite Fdata.basis := by
2334 have hlt : Cardinal.mk Fdata.basis < Cardinal.aleph0 := by
2335 rw [hcard]
2336 exact Cardinal.natCast_lt_aleph0
2337 exact Cardinal.lt_aleph0_iff_finite.mp hlt
2338 letI : Fintype Fdata.basis := Fintype.ofFinite Fdata.basis
2339 let rH : ℕ := Fintype.card Fdata.basis
2340 let eFin : Fin rH ≃ Fdata.basis := (Fintype.equivFin Fdata.basis).symm
2341 let Y : Fin rH → ↥(Hpre : Subgroup F) :=
2342 fun k => e (Fdata.inclusion (eFin k))
2343 have hHpreProC :
2345 (G := ↥(Hpre : Subgroup F)) := by
2346 exact
2348 (ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed sigma)
2349 (ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed sigma)
2350 (ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed sigma)
2351 hFree.isProC (Hpre : Subgroup F)
2353 have hFreeY :
2354 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2356 (Fin rH) ↥(Hpre : Subgroup F) Y := by
2357 have hpre :=
2358 Fdata.isFree.precompEquiv eFin
2359 exact hpre.ofContinuousMulEquiv e hHpreProC
2360 rcases hpower_range with ⟨b0, hb0⟩
2361 let j0 : Fin rH := eFin.symm b0
2362 let xN_H : ↥(Hpre : Subgroup F) := ⟨(XU (ULift.up i)) ^ N, hpow⟩
2363 have hYj0 : Y j0 = xN_H := by
2364 change e (Fdata.inclusion (eFin (eFin.symm b0))) = xN_H
2365 simpa [Y, j0, xN_H] using hb0
2366 have hdCentN : d ∈ centralizerOf ((x ^ N) ^ n) := by
2367 have hdNat :
2368 d ∈ centralizerOf (x ^ (n.natAbs : ℤ)) :=
2370 have hdNatNat :
2371 d ∈ centralizerOf (x ^ n.natAbs) := by
2372 rw [zpow_natCast] at hdNat
2373 exact hdNat
2374 have hdPow :
2375 d ∈ centralizerOf ((x ^ n.natAbs) ^ N) :=
2377 have hdTargetNat :
2378 d ∈ centralizerOf ((x ^ N) ^ (n.natAbs : ℤ)) := by
2379 have hpoweq : (x ^ N) ^ n.natAbs = (x ^ n.natAbs) ^ N := by
2380 rw [← pow_mul, ← pow_mul, Nat.mul_comm]
2381 rw [zpow_natCast]
2382 simpa [hpoweq] using hdPow
2384 exact hdTargetNat
2385 have hcommQ : ⁅(x ^ N) ^ n, d⁆ = 1 := by
2386 exact
2387 commutatorElement_eq_one_iff_mul_comm.2
2388 ((mem_centralizerOf_iff.mp hdCentN).symm)
2389 have hqcommF : q ⁅((X i) ^ N) ^ n, a⁆ = 1 := by
2390 have hqa' : q a = d := by simpa using hqa
2391 rw [map_commutatorElement, map_zpow]
2392 change ⁅(q ((X i) ^ N)) ^ n, q a⁆ = 1
2393 have hqXiN : q ((X i) ^ N) = q (X i) ^ N := by simp only [map_pow]
2394 rw [hqXiN]
2395 change ⁅(q (X i) ^ N) ^ n, q a⁆ = 1
2396 rw [hqa']
2397 simpa [x] using hcommQ
2398 have hcommF_der :
2399 ⁅((X i) ^ N) ^ n, a⁆ ∈ topDerivedTop F m :=
2401 (G := F) (m := m) (x := ⁅((X i) ^ N) ^ n, a⁆)).1 hqcommF
2402 have hcommH_der :
2403 ⁅xN_H ^ n, aH⁆ ∈ topDerivedTop ↥(Hpre : Subgroup F) (m - 1) := by
2404 have hcomm_map := hFm_le_Hpre hcommF_der
2405 rcases hcomm_map with ⟨w, hw, hwval⟩
2406 have hw_eq : w = ⁅xN_H ^ n, aH⁆ := by
2407 apply Subtype.ext
2408 simpa [xN_H, XU, aH, commutatorElement_def] using hwval
2409 rwa [← hw_eq]
2410 let qpre : ↥(Hpre : Subgroup F) →ₜ*
2411 MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1) :=
2412 continuousToMaxSolvQuot ↥(Hpre : Subgroup F) (m - 1)
2413 have hqpre_comm :
2414 qpre ⁅xN_H ^ n, aH⁆ = 1 :=
2416 (G := ↥(Hpre : Subgroup F)) (m := m - 1)
2417 (x := ⁅xN_H ^ n, aH⁆)).2 hcommH_der
2418 have hcommQuot :
2419 ⁅qpre (xN_H ^ n), qpre aH⁆ = 1 := by
2420 simpa [map_commutatorElement] using hqpre_comm
2421 have haH_cent :
2422 qpre aH ∈ centralizerOf (qpre (xN_H ^ n)) := by
2424 exact (commutatorElement_eq_one_iff_mul_comm.1 hcommQuot).symm
2425 have hcent_formula :=
2426 ih Y hFreeY j0 n hn
2427 have haH_cyc :
2428 qpre aH ∈
2429 (closedSubgroupGenerated ({qpre (Y j0)} : Set _) :
2430 Subgroup (MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1))) := by
2431 rw [← hcent_formula]
2432 simpa [qpre, hYj0, map_zpow] using haH_cent
2433 have haHq_der :
2434 qpre aH ∈
2435 topDerivedTop (MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1)) 1 := by
2436 exact topDerived_map_le (f := qpre) (m := 1) ⟨aH, haH_der_one, rfl⟩
2437 have hcycInf :
2438 (closedSubgroupGenerated ({qpre (Y j0)} : Set _) :
2439 Subgroup (MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1))) ⊓
2440 topDerivedTop (MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1)) 1 = ⊥ := by
2441 simpa [qpre] using
2443 (C := SigmaGroup[sigma]) (F := ↥(Hpre : Subgroup F))
2444 Y hFreeY j0 (m - 1)
2445 have hqpre_a_bot :
2446 qpre aH ∈
2447 (⊥ : Subgroup (MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1))) := by
2448 have hinf :
2449 qpre aH ∈
2450 (closedSubgroupGenerated ({qpre (Y j0)} : Set _) :
2451 Subgroup (MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1))) ⊓
2452 topDerivedTop (MaxSolvQuot ↥(Hpre : Subgroup F) (m - 1)) 1 :=
2453 ⟨haH_cyc, haHq_der⟩
2454 rw [← hcycInf]
2455 exact hinf
2456 have hqpre_a_one : qpre aH = 1 :=
2457 Subgroup.mem_bot.mp hqpre_a_bot
2458 exact
2460 (G := ↥(Hpre : Subgroup F)) (m := m - 1) (x := aH)).1
2461 hqpre_a_one
2462 have hqH_der :
2463 qH aH ∈ topDerivedTop ↥(H : Subgroup Q) (m - 1) := by
2464 exact topDerived_map_le (f := qH) (m := m - 1) ⟨aH, haH_last, rfl⟩
2465 refine ⟨qH aH, hqH_der, ?_⟩
2466 change (qH aH : Q) = d
2467 simpa [qH, aH, hqa])
2468 have hg_eq_c : g = c := by
2469 calc
2470 g = c * d := hcd.symm
2471 _ = c := by rw [hd_eq_one, mul_one]
2472 rw [hg_eq_c]
2473 simpa only [Cx] using hc
2474 · simpa [map_zpow] using
2476 (G := MaxSolvQuot F m) (continuousToMaxSolvQuot F m (X i)) n)
2478/-- The pro-`Σ` finite-rank case, reduced to the metabelian base case and the induction step. -/
2480 {sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p)
2481 {r : ℕ} (X : Fin r → F)
2482 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2484 (Fin r) F X)
2485 (i : Fin r) (m : ℕ) (hm : 2 ≤ m) (n : ℤ) (hn : n ≠ 0) :
2488 cases r with
2489 | zero =>
2490 exact Fin.elim0 i
2491 | succ r =>
2492 have hmain :
2493 ∀ m : ℕ, 2 ≤ m →
2494 ∀ {r' : ℕ} {F' : Type u}
2495 [TopologicalSpace F'] [Group F'] [IsTopologicalGroup F'],
2496 ∀ Y : Fin r' → F',
2497 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2499 (Fin r') F' Y →
2500 ∀ i : Fin r', ∀ n : ℤ, n ≠ 0 →
2503 intro m
2504 refine Nat.strong_induction_on m ?_
2505 intro m ih hm r' F' _ _ _ Y hFreeY i n hn
2506 cases r' with
2507 | zero =>
2508 exact Fin.elim0 i
2509 | succ r' =>
2510 cases r' with
2511 | zero =>
2512 have hi0 : i = 0 := by
2513 fin_cases i
2514 rfl
2515 simpa [hi0] using
2517 (C := SigmaGroup[sigma]) (F := F') Y hFreeY m n
2518 | succ r' =>
2519 by_cases hm2 : m = 2
2520 · subst hm2
2521 exact
2523 (F := F') hsigma Y hFreeY i n hn
2524 · have hlt : 2 < m := lt_of_le_of_ne hm (Ne.symm hm2)
2525 have hm3 : 3 ≤ m := Nat.succ_le_of_lt hlt
2526 refine
2528 (F := F') hsigma Y hFreeY hm3 ?_ i n hn
2529 intro F'' _ _ _ r'' Z hFreeZ j z hz
2530 exact
2531 ih (m - 1)
2532 (Nat.sub_lt (show 0 < m by exact lt_trans (by decide) hlt) (by decide))
2533 (Nat.le_sub_of_add_le hm3) Z hFreeZ j z hz
2534 exact hmain m hm (F' := F) X hFree i n hn
2536/-- Theorem 1.5 for a finite pro-`Σ` basis family. -/
2538 {sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p)
2539 {ι : Type v} [Finite ι] (X : ι → F)
2540 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2541 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate (SigmaGroup[sigma])) ι F X)
2542 (i : ι) (m : ℕ) (hm : 2 ≤ m) (n : ℤ) (hn : n ≠ 0) :
2545 classical
2546 letI : Fintype ι := Fintype.ofFinite ι
2547 let r : ℕ := Fintype.card ι
2548 let e : ι ≃ Fin r := Fintype.equivFin ι
2549 let Xfin : Fin r → F := fun k => X (e.symm k)
2550 have hFreeFin : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2552 (Fin r) F Xfin :=
2553 finiteFamily_to_finiteRank (C := SigmaGroup[sigma]) X hFree
2554 have hcore :
2555 centralizerOf (continuousToMaxSolvQuot F m ((Xfin (e i)) ^ n)) =
2556 closedSubgroupGenerated ({continuousToMaxSolvQuot F m (Xfin (e i))} : Set _) :=
2557 thm_center_free_freegroup_finiteRank hsigma Xfin hFreeFin (e i) m hm n hn
2558 simpa [Xfin, e] using hcore
2560/-- The centralizer formula for maximal solvable quotients of free pro-`Σ` groups. -/
2562 {sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p)
2563 {ι : Type v} (X : ι → F)
2564 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2565 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate (SigmaGroup[sigma])) ι F X)
2566 (i : ι) (m : ℕ) (hm : 2 ≤ m) (n : ℤ) (hn : n ≠ 0) :
2569 classical
2570 let Q : Type u := MaxSolvQuot F m
2571 let π : F →ₜ* Q := continuousToMaxSolvQuot F m
2572 let x : Q := π (X i)
2575 (G := F)
2577 (SigmaGroup[sigma]) hFree.isProC)
2578 (N := topDerivedTop F m) (by infer_instance)
2579 letI : CompactSpace Q := hQprof.compactSpace
2580 letI : T2Space Q := hQprof.t2Space
2581 letI : TotallyDisconnectedSpace Q := hQprof.totallyDisconnectedSpace
2582 apply le_antisymm
2583 · intro g hg
2584 by_contra hgcyc
2585 let Cyc : ClosedSubgroup Q :=
2587 obtain ⟨U, hC_le_U, hgU⟩ :=
2589 (G := Q) hQprof Cyc hgcyc
2590 let k : ℕ := Nat.card (Q ⧸ ((U : OpenSubgroup Q) : Subgroup Q))
2591 let hUfinite : Finite (Q ⧸ ((U : OpenSubgroup Q) : Subgroup Q)) :=
2593 let ψ : Q →ₜ* Equiv.Perm (Fin k) :=
2594 ProCGroups.FiniteGeneration.openSubgroupIndexContinuousHom
2595 (G := Q) (H := (U : Subgroup Q)) U.isOpen' hUfinite (n := k) rfl
2596 let b : Fin k :=
2597 ProCGroups.FiniteGeneration.openSubgroupIndexBasepoint
2598 (G := Q) (H := (U : Subgroup Q)) hUfinite (n := k) rfl
2599 have hψg_move : ψ g b ≠ b := by
2600 intro hfix
2601 have hgU' : g ∈ (U : Subgroup Q) := by
2602 rw [ProCGroups.FiniteGeneration.mem_openSubgroup_iff_indexAction_fix_basepoint
2603 (G := Q) (H := (U : Subgroup Q)) hUfinite (n := k) rfl (g := g)]
2604 simpa [ψ, b, k] using hfix
2605 exact hgU hgU'
2606 have hψ_not_image :
2607 ψ g ∉ ψ '' ((closedSubgroupGenerated ({x} : Set Q) : Subgroup Q) : Set Q) := by
2608 rintro ⟨c, hc, hcg⟩
2609 have hcfix :
2610 ψ c b = b := by
2611 have hcU : c ∈ (U : Subgroup Q) := hC_le_U hc
2612 rw [ProCGroups.FiniteGeneration.mem_openSubgroup_iff_indexAction_fix_basepoint
2613 (G := Q) (H := (U : Subgroup Q)) hUfinite (n := k) rfl (g := c)] at hcU
2614 simpa [ψ, b, k] using hcU
2615 have hgfix : ψ g b = b := by simpa [hcg] using hcfix
2616 exact hψg_move hgfix
2617 let Supp : Set ι := {j | ψ (π (X j)) ≠ 1}
2618 let oneU : OpenSubgroup (Equiv.Perm (Fin k)) :=
2619 { toSubgroup := ⊥
2620 isOpen' := by
2621 exact
2622 isOpen_discrete
2623 (s := (((⊥ : Subgroup (Equiv.Perm (Fin k))) :
2624 Set (Equiv.Perm (Fin k))))) }
2625 have hSuppFinite : Supp.Finite := by
2626 have hconvψ :
2627 ProCGroups.FreeProC.FamilyConvergesToOne (G := Equiv.Perm (Fin k))
2628 (fun j => ψ (π (X j))) :=
2629 ProCGroups.FreeProC.FamilyConvergesToOne.comp (G := F) (H := Equiv.Perm (Fin k))
2630 (μ := X) hFree.convergesToOne (ψ.comp π)
2631 simpa [Supp, oneU] using hconvψ oneU
2632 let S : Finset ι := insert i hSuppFinite.toFinset
2633 have hiS : i ∈ S := by simp only [Finset.mem_insert, Set.Finite.mem_toFinset, true_or, S]
2634 have hψOutside : ∀ j, j ∉ S → ψ (π (X j)) = 1 := by
2635 intro j hj
2636 by_contra hj1
2637 exact hj (by simp only [ne_eq, Finset.mem_insert, Set.Finite.mem_toFinset, Set.mem_setOf_eq, hj1, not_false_eq_true,
2638 or_true, S, Supp])
2639 let R : Type u := hFree.FinsetSupportRetract S
2640 let B : S → R := hFree.finsetSupportBasis S
2641 let ρQ : Q →ₜ* MaxSolvQuot R m := finsetSupportRangeQuot X hFree S m
2642 let ιQ : MaxSolvQuot R m →ₜ* Q := finsetSupportInclusionQuot X hFree S m
2643 let iS : S := ⟨i, hiS⟩
2644 let xR : MaxSolvQuot R m := continuousToMaxSolvQuot R m (B iS)
2645 have hxR : ρQ x = xR := by
2646 have hxRange : hFree.collapseToFinsetRange S (X i) = B iS := by
2647 apply Subtype.ext
2648 change (hFree.collapseToFinset S (X i) : F) = X i
2649 simpa [B, ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet.collapseToFinsetRange,
2650 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet.finsetSupportBasis] using
2651 hFree.collapseToFinset_apply_mem (S := S) hiS
2652 change
2656 exact congrArg (continuousToMaxSolvQuot R m) hxRange
2657 have hιxR : ιQ xR = x := by
2658 change
2663 rfl
2664 have hgRcent : ρQ g ∈ centralizerOf (xR ^ n) := by
2666 have hcomm :
2667 g * (continuousToMaxSolvQuot F m (X i)) ^ n =
2668 (continuousToMaxSolvQuot F m (X i)) ^ n * g := by
2669 have hg' :
2670 g ∈ centralizerOf ((continuousToMaxSolvQuot F m (X i)) ^ n) := by
2671 simpa [map_zpow] using hg
2672 exact mem_centralizerOf_iff.mp hg'
2673 have hxR' : ρQ (continuousToMaxSolvQuot F m (X i)) = xR := by
2674 simpa [x, π] using hxR
2675 have hxRn :
2676 ρQ ((continuousToMaxSolvQuot F m (X i)) ^ n) = xR ^ n := by
2677 calc
2678 ρQ ((continuousToMaxSolvQuot F m (X i)) ^ n)
2679 = (ρQ (continuousToMaxSolvQuot F m (X i))) ^ n := by simp only [map_zpow]
2680 _ = xR ^ n := by rw [hxR']
2681 simpa [map_mul, hxRn] using congrArg ρQ hcomm
2682 have hFreeR :
2683 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2684 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate (SigmaGroup[sigma])) S R B :=
2685 hFree.isFreeProCGroupOnConvergingSet_finsetSupportBasis S
2686 have hcentR :
2690 (F := R) hsigma B hFreeR iS m hm n hn
2691 have hgRcyc : ρQ g ∈
2693 Subgroup (MaxSolvQuot R m)) := by
2694 rw [← hcentR]
2695 simpa [xR, map_zpow] using hgRcent
2696 have hcollapsedC :
2697 collapseToFinsetQuot X hFree S m g ∈
2698 (closedSubgroupGenerated ({x} : Set Q) : Subgroup Q) := by
2699 have hmap :
2700 ιQ (ρQ g) ∈
2701 (closedSubgroupGenerated ({ιQ xR} : Set Q) : Subgroup Q) :=
2703 have hcompg :
2704 ιQ (ρQ g) = collapseToFinsetQuot X hFree S m g := by
2705 obtain ⟨x, rfl⟩ := continuousToMaxSolvQuot_surjective (G := F) m g
2706 have hcomp :
2707 (hFree.collapseToFinsetInclusion S).comp (hFree.collapseToFinsetRange S) =
2708 hFree.collapseToFinset S := by
2709 ext x
2710 rfl
2711 change
2716 exact congrArg
2717 (fun y : F => continuousToMaxSolvQuot F m y)
2718 (congrArg (fun f : F →ₜ* F => f x) hcomp)
2719 exact hcompg ▸ (by simpa [hιxR] using hmap)
2720 have hψfactor :
2721 ψ.comp (collapseToFinsetQuot X hFree S m) = ψ :=
2722 comp_collapseToFinsetQuot_eq_of_eq_one_outside (X := X) hFree S m ψ hψOutside
2723 have hψcollapsed : ψ (collapseToFinsetQuot X hFree S m g) = ψ g := by
2724 exact congrArg (fun f : Q →ₜ* Equiv.Perm (Fin k) => f g) hψfactor
2725 have hψimg : ψ g ∈
2726 ψ '' ((closedSubgroupGenerated ({x} : Set Q) : Subgroup Q) : Set Q) := by
2727 have : ψ (collapseToFinsetQuot X hFree S m g) ∈
2728 ψ '' ((closedSubgroupGenerated ({x} : Set Q) : Subgroup Q) : Set Q) :=
2729 ⟨collapseToFinsetQuot X hFree S m g, hcollapsedC, rfl⟩
2730 simpa [hψcollapsed] using this
2731 exact hψ_not_image hψimg
2732 · have hcyc :
2735 ((continuousToMaxSolvQuot F m (X i)) ^ n) :=
2738 simpa [map_zpow] using hcyc
2740/-- A group is slim if two elements satisfy the centralizer formula and their closed cyclic
2741subgroups have trivial intersection. -/
2743 [CompactSpace G]
2744 (x x' : G)
2745 (hcentx : ∀ n : ℕ, 0 < n → centralizerOf (x ^ n) =
2746 (closedSubgroupGenerated ({x} : Set G) : Subgroup G))
2747 (hcentx' : ∀ n : ℕ, 0 < n → centralizerOf (x' ^ n) =
2748 (closedSubgroupGenerated ({x'} : Set G) : Subgroup G))
2749 (htriv : (closedSubgroupGenerated ({x} : Set G) : Subgroup G) ⊓
2750 (closedSubgroupGenerated ({x'} : Set G) : Subgroup G) = ⊥) :
2751 IsSlim G := by
2753 intro H
2754 rw [Subgroup.eq_bot_iff_forall]
2755 intro z hz
2756 obtain ⟨n, hn, hxn⟩ := ProCGroups.exists_pos_pow_mem_openSubgroup (G := G) H x
2757 obtain ⟨n', hn', hx'n'⟩ := ProCGroups.exists_pos_pow_mem_openSubgroup (G := G) H x'
2758 have hzcentx : (z : G) ∈ centralizerOf (x ^ n) := by
2760 exact (congrArg Subtype.val ((Subgroup.mem_center_iff.mp hz) ⟨x ^ n, hxn⟩)).symm
2761 have hzcentx' : (z : G) ∈ centralizerOf (x' ^ n') := by
2763 exact (congrArg Subtype.val ((Subgroup.mem_center_iff.mp hz) ⟨x' ^ n', hx'n'⟩)).symm
2764 have hzx : (z : G) ∈ (closedSubgroupGenerated ({x} : Set G) : Subgroup G) := by
2765 rw [← hcentx n hn]
2766 exact hzcentx
2767 have hzx' : (z : G) ∈ (closedSubgroupGenerated ({x'} : Set G) : Subgroup G) := by
2768 rw [← hcentx' n' hn']
2769 exact hzcentx'
2770 have hzbot : (z : G) ∈ (⊥ : Subgroup G) := by
2771 have hzinf : (z : G) ∈ (closedSubgroupGenerated ({x} : Set G) : Subgroup G) ⊓
2772 (closedSubgroupGenerated ({x'} : Set G) : Subgroup G) :=
2773 ⟨hzx, hzx'⟩
2774 simpa [htriv] using hzinf
2775 exact Subtype.ext (by simpa using hzbot)
2777/-- Slimness of maximal solvable quotients of free pro-`Σ` groups of rank not equal to one. -/
2779 {sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p)
2780 {ι : Type v} (X : ι → F)
2781 (hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2782 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate (SigmaGroup[sigma])) ι F X)
2783 (hrank : ¬ Nonempty (Unique ι))
2784 (m : ℕ) (hm : 2 ≤ m) :
2785 IsSlim (MaxSolvQuot F m) := by
2786 classical
2789 (SigmaGroup[sigma]) hFree.isProC)
2790 letI : CompactSpace F := hFprof.compactSpace
2791 letI : T2Space F := hFprof.t2Space
2792 letI : TotallyDisconnectedSpace F := hFprof.totallyDisconnectedSpace
2793 by_cases hEmpty : IsEmpty ι
2794 · have hRangeEmpty : Set.range X = (∅ : Set F) := by
2795 ext y
2796 constructor
2797 · rintro ⟨i, rfl⟩
2798 exact (hEmpty.false i).elim
2799 · simp only [Set.mem_empty_iff_false, Set.mem_range, IsEmpty.exists_iff, imp_self]
2800 have hclosureEmpty : Subgroup.closure (∅ : Set F) = (⊥ : Subgroup F) := by
2801 ext y
2802 simp only [Subgroup.closure_empty, Subgroup.mem_bot]
2803 have hbotClosed : IsClosed (((⊥ : Subgroup F) : Set F)) := by
2804 exact isClosed_singleton
2805 have hbotClosure : (⊥ : Subgroup F).topologicalClosure = ⊥ := by
2806 apply le_antisymm
2807 · exact Subgroup.topologicalClosure_minimal _ le_rfl hbotClosed
2808 · exact Subgroup.le_topologicalClosure (s := (⊥ : Subgroup F))
2809 have hgen :
2810 ((⊥ : Subgroup F).topologicalClosure : Subgroup F) = ⊤ := by
2811 have htopGen := hFree.generates_range
2813 simpa [hRangeEmpty, hclosureEmpty] using htopGen
2814 have htopbot : (⊤ : Subgroup F) = ⊥ := by
2815 rw [hbotClosure] at hgen
2816 exact hgen.symm
2817 have hFtriv : ∀ g : F, g = 1 := by
2818 intro g
2819 have hgTop : g ∈ (⊤ : Subgroup F) := by simp only [Subgroup.mem_top]
2820 have hgBot : g ∈ (⊥ : Subgroup F) := by simpa [htopbot] using hgTop
2821 simpa using hgBot
2822 have hQtriv : ∀ q : MaxSolvQuot F m, q = 1 := by
2823 intro q
2824 rcases continuousToMaxSolvQuot_surjective (G := F) m q with ⟨g, rfl⟩
2825 simp only [hFtriv g, map_one]
2826 intro H
2827 ext q
2828 constructor
2829 · intro hq
2830 have hq1 : (q : MaxSolvQuot F m) = 1 := hQtriv q
2831 simp only [hq1, one_mem]
2832 · intro hq
2833 have hq1 : (q : MaxSolvQuot F m) = 1 := hQtriv q
2834 simp only [hq1, one_mem]
2835 have hNotSubsingleton : ¬ Subsingleton ι := by
2836 intro hSub
2837 rcases not_isEmpty_iff.mp hEmpty with ⟨i0⟩
2838 exact hrank ⟨
2839 { default := i0
2840 uniq := fun i => @Subsingleton.elim _ hSub i i0 }⟩
2841 letI : Nontrivial ι := not_subsingleton_iff_nontrivial.mp hNotSubsingleton
2842 obtain ⟨i, j, hij⟩ := exists_pair_ne ι
2843 let x : MaxSolvQuot F m := continuousToMaxSolvQuot F m (X i)
2844 let x' : MaxSolvQuot F m := continuousToMaxSolvQuot F m (X j)
2845 have hcentx :
2846 ∀ n : ℕ, 0 < n → centralizerOf (x ^ n) =
2848 Subgroup (MaxSolvQuot F m)) := by
2849 intro n hn
2850 have hnz : (n : ℤ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn)
2851 simpa [x, zpow_natCast] using
2852 (theorem_1_5_center_free_freegroup (F := F) hsigma X hFree i m hm (n : ℤ) hnz)
2853 have hcentx' :
2854 ∀ n : ℕ, 0 < n → centralizerOf (x' ^ n) =
2856 Subgroup (MaxSolvQuot F m)) := by
2857 intro n hn
2858 have hnz : (n : ℤ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn)
2859 simpa [x', zpow_natCast] using
2860 (theorem_1_5_center_free_freegroup (F := F) hsigma X hFree j m hm (n : ℤ) hnz)
2861 have htriv :
2863 Subgroup (MaxSolvQuot F m)) ⊓
2865 Subgroup (MaxSolvQuot F m)) = ⊥ := by
2866 simpa [x, x'] using
2868 (C := SigmaGroup[sigma]) (F := F) X hFree hij m
2871/-! ## Subsection 2.1: Ab-torsion-freeness and ab-faithfulness -/
2873-- Local notation used only in this file to keep statements readable.
2875/-- The preimage of an open subgroup above the last derived term has the same
2876maximal abelian quotient. -/
2878 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2879 [CompactSpace G]
2880 {m : ℕ} (hm : 2 ≤ m)
2881 (P : OpenSubgroup (Qm G m))
2882 (hP : lastDerivedSubgroup (G := G) m ≤ (P : Subgroup (Qm G m))) :
2883 Nonempty
2885 ↥((preimageOpenSubgroup (continuousToMaxSolvQuot G m) P : OpenSubgroup G) :
2886 Subgroup G) 1 ≃*
2887 MaxSolvQuot ↥(P : Subgroup (Qm G m)) 1) := by
2888 let Q : Type u := Qm G m
2889 let π : G →ₜ* Q := continuousToMaxSolvQuot G m
2890 have hπsurj : Function.Surjective π := by
2891 simpa [π, Q] using continuousToMaxSolvQuot_surjective (G := G) m
2892 have hpre :
2893 topDerivedTop G (m - 1) ≤ ((P : Subgroup Q).comap (π : G →* Q)) := by
2894 intro x hx
2895 exact hP ((topDerivedTop_le_comap (f := π) (m := m - 1)) hx)
2896 have hm1 : 1 ≤ m := le_trans (by decide) hm
2897 have hker :
2898 (π : G →* Q).ker ≤
2900 ↥((preimageOpenSubgroup π P : OpenSubgroup G) : Subgroup G) 1).map
2901 (Subgroup.subtype
2902 ((preimageOpenSubgroup π P : OpenSubgroup G) : Subgroup G)) := by
2903 simpa [π, Q] using
2905 (G := G) (m := m) hm1 P hpre
2906 have hclosed :
2907 IsClosedMap (π.restrictPreimage (P : Subgroup Q)) := by
2908 exact
2910 (π := π) (Q₁ := (P : Subgroup Q))
2911 ((continuousToMaxSolvQuot G m).continuous_toFun.isClosedMap)
2912 (Subgroup.isClosed_of_isOpen (P : Subgroup Q) P.isOpen')
2913 simpa [π, Q] using
2915 (G := G) (Q := Q) π hπsurj P hclosed 1 hker
2917/-- Open subgroups above the last derived term have torsion-free abelianization. -/
2919 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2920 [CompactSpace G]
2922 {m : ℕ} (hm : 2 ≤ m)
2923 (H : OpenSubgroup (Qm G m))
2924 (hH : aboveLastDerived (G := G) m H) :
2925 IsMulTorsionFree
2926 (AbTop ↥(H : Subgroup (Qm G m))) :=
2928 (G := G) hG hm H hH
2930/-- Open normal subgroups above the last derived term inherit faithful
2931conjugation action. -/
2933 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2934 [CompactSpace G] [TotallyDisconnectedSpace G]
2936 {m : ℕ} (hm : 2 ≤ m)
2937 (H : OpenSubgroup (Qm G m))
2938 (N : OpenNormalSubgroup ↥(H : Subgroup (Qm G m)))
2939 (hContain : containsLastDerived (G := G) m H N) :
2940 Function.Injective
2942 (G := ↥(H : Subgroup (Qm G m)))
2943 (N := (N : Subgroup ↥(H : Subgroup (Qm G m))))) :=
2945 (G := G) hG hm H N hContain
2947/-- Ab-torsion-freeness passes to closed subgroups. -/
2949 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2950 [CompactSpace G] [TotallyDisconnectedSpace G]
2952 {K : Subgroup G} (hKClosed : IsClosed (K : Set G)) :
2956/-- An ab-torsion-free profinite group is torsion-free. -/
2958 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2959 [CompactSpace G] [TotallyDisconnectedSpace G]
2961 IsTorsionFreeGroup G :=
2964/-- Maximal finite-step solvable quotients are torsion-free. -/
2966 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2967 [CompactSpace G] [TotallyDisconnectedSpace G]
2969 {m : ℕ} (hm : 1 ≤ m) :
2970 IsTorsionFreeGroup (Qm G m) :=
2973/-- Closed normal subgroups inside the first derived subgroup have no nontrivial
2974fixed points on abelianization. -/
2976 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2977 [CompactSpace G] [TotallyDisconnectedSpace G]
2978 {K : Subgroup G} (hKClosed : IsClosed (K : Set G))
2979 (hKNormal : K.Normal) (hK : K ≤ topDerivedTop G 1)
2981 let _ : K.Normal := hKNormal
2984 noFixedPoints_of_isAbTorsionFree (G := G) hKClosed hKNormal hK hG
2986/-- An ab-faithful profinite group is center-free. -/
2988 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2989 [CompactSpace G] [TotallyDisconnectedSpace G]
2990 (hG : IsAbFaithful G) :
2991 Subgroup.center G = ⊥ :=
2994/-- In maximal solvable quotients, the center is contained in the last derived
2995subgroup. -/
2997 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
2998 [CompactSpace G] [TotallyDisconnectedSpace G]
3000 {m : ℕ} (hm : 1 ≤ m) :
3001 Subgroup.center (Qm G m) ≤ lastDerivedSubgroup (G := G) m :=
3004/-- Maximal solvable quotients are torsion-free and center-free under ab-torsion-freeness and
3005ab-faithfulness. -/
3007 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
3008 [CompactSpace G] [TotallyDisconnectedSpace G]
3009 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
3010 {m : ℕ} (hm : 2 ≤ m) :
3011 IsTorsionFreeGroup (Qm G m) ∧
3012 Subgroup.center (Qm G m) = ⊥ := by
3013 exact
3015 (G := G) hTorsion (le_trans (by decide) hm),
3017 (G := G) hTorsion hFaithful hm⟩
3019/-- The centralizer of an open subgroup lies in the last derived subgroup under ab-torsion-freeness
3020and ab-faithfulness. -/
3022 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
3023 [CompactSpace G] [TotallyDisconnectedSpace G]
3024 (hTorsion : IsAbTorsionFree G) (hFaithful : IsAbFaithful G)
3025 {m : ℕ} (hm : 1 ≤ m)
3026 (H : OpenSubgroup (Qm G m)) :
3027 Subgroup.centralizer (H : Set (Qm G m))
3028 ≤ lastDerivedSubgroup (G := G) m :=
3029 centralizer_openSubgroup_le_lastDerived_of_abTorsionFree_faithful
3030 (G := G) hTorsion hFaithful hm H
3032end CenterFreenessFiniteStepSolvable