ProCGroups/Abelian/TopologicalAbelianizationLimits.lean
1import ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
2import ProCGroups.InverseSystems.Quotients
3import ProCGroups.InverseSystems.StagewiseIso
4import ProCGroups.ProC.Quotients.ClosedNormal
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/Abelian/TopologicalAbelianizationLimits.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Topological abelianization and inverse limits
17Strong inverse-limit API for topological abelianization of profinite inverse systems.
18-/
20open scoped Topology
22namespace ProCGroups.Abelian
24universe u v
25/-- The stagewise inverse system obtained by applying topological abelianization. -/
26noncomputable def abelianizationInverseSystem
27 {I : Type u} [Preorder I]
28 (S : InverseSystems.InverseSystem (I := I))
29 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
30 [∀ i, IsTopologicalGroup (S.X i)] :
31 InverseSystems.InverseSystem (I := I) where
32 X := fun i => TopologicalAbelianization (S.X i)
33 topologicalSpace := fun i => inferInstance
34 map := fun {i j} hij =>
35 TopologicalAbelianization.map
36 { toMonoidHom :=
37 { toFun := S.map hij
38 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
39 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
40 continuous_toFun := S.continuous_map hij }
41 continuous_map := by
42 intro i j hij
43 exact (TopologicalAbelianization.map
44 { toMonoidHom :=
45 { toFun := S.map hij
46 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
47 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
48 continuous_toFun := S.continuous_map hij }).continuous_toFun
49 map_id := by
50 intro i
51 funext x
52 refine Quotient.inductionOn' x ?_
53 intro a
54 change
55 QuotientGroup.mk'
56 (Subgroup.topologicalClosure (commutator (S.X i)))
57 (S.map (le_rfl : i ≤ i) a) =
58 QuotientGroup.mk'
59 (Subgroup.topologicalClosure (commutator (S.X i)))
60 a
61 exact congrArg
62 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))
63 (S.map_id_apply i a)
64 map_comp := by
65 intro i j k hij hjk
66 funext x
67 refine Quotient.inductionOn' x ?_
68 intro a
69 change
70 QuotientGroup.mk'
71 (Subgroup.topologicalClosure (commutator (S.X i)))
72 (S.map hij (S.map hjk a)) =
73 QuotientGroup.mk'
74 (Subgroup.topologicalClosure (commutator (S.X i)))
75 (S.map (hij.trans hjk) a)
76 exact congrArg
77 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))
78 (S.map_comp_apply hij hjk a)
80/-- Each stage of the abelianization inverse system inherits its quotient group structure. -/
82 {I : Type u} [Preorder I]
83 (S : InverseSystems.InverseSystem (I := I))
84 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
85 [∀ i, IsTopologicalGroup (S.X i)] (i : I) :
86 Group ((abelianizationInverseSystem S).X i) := by
87 change Group (TopologicalAbelianization (S.X i))
88 infer_instance
90/-- The abelianization inverse system is a group-valued inverse system. -/
92 {I : Type u} [Preorder I]
93 (S : InverseSystems.InverseSystem (I := I))
94 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
95 [∀ i, IsTopologicalGroup (S.X i)] :
96 InverseSystems.IsGroupSystem (abelianizationInverseSystem S) where
98 intro i j hij
99 simp only [abelianizationInverseSystem, Lean.Elab.WF.paramLet, map_one]
101 intro i j hij x y
102 simp only [abelianizationInverseSystem, Lean.Elab.WF.paramLet, map_mul]
103 map_inv := by
104 intro i j hij x
105 exact (TopologicalAbelianization.map
106 { toMonoidHom :=
107 { toFun := S.map hij
108 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
109 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
110 continuous_toFun := S.continuous_map hij }).map_inv x
112/-- The stagewise quotient maps assemble into a morphism from an inverse system to its
113stagewise topological abelianization. -/
115 {I : Type u} [Preorder I]
116 (S : InverseSystems.InverseSystem (I := I))
117 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
118 [∀ i, IsTopologicalGroup (S.X i)] :
119 S.Morphism (abelianizationInverseSystem S) where
120 map := fun i => TopologicalAbelianization.mk (S.X i)
121 continuous_map := fun _ => continuous_quotient_mk'
122 comm := by
123 intro i j hij
124 funext x
125 rfl
127/-- The stagewise closed commutator subgroups form a compatible closed-normal family in any
128group-valued inverse system of topological groups. -/
129noncomputable def closedCommutatorCompatibleClosedNormalSubgroups
130 {I : Type u} [Preorder I]
131 (S : InverseSystems.InverseSystem (I := I))
132 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
133 [∀ i, IsTopologicalGroup (S.X i)] :
134 S.CompatibleClosedNormalSubgroups where
135 N := fun i => Subgroup.closedCommutator (S.X i)
136 normal := fun i => by infer_instance
137 closed := fun i => Subgroup.isClosed_closedCommutator (S.X i)
138 map_le := by
139 intro i j hij x hx
140 let f : S.X j →ₜ* S.X i :=
141 { toMonoidHom := S.transitionHom hij
142 continuous_toFun :=
143 InverseSystems.InverseSystem.continuous_transitionHom (S := S) hij }
144 have hxmap :
145 S.transitionHom hij x ∈
146 (Subgroup.closedCommutator (S.X j)).map f.toMonoidHom :=
147 Subgroup.mem_map_of_mem f.toMonoidHom hx
148 exact Subgroup.closedCommutator_map_le f hxmap
150/-- The canonical comparison map from the abelianization of an inverse limit to the inverse limit
151of the stagewise abelianizations. -/
152noncomputable def topologicalAbelianizationInverseLimitComparison
153 {I : Type u} [Preorder I]
154 (S : InverseSystems.InverseSystem (I := I))
155 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
156 [∀ i, IsTopologicalGroup (S.X i)] :
157 TopologicalAbelianization S.inverseLimit →ₜ*
158 (abelianizationInverseSystem S).inverseLimit := by
159 let T := abelianizationInverseSystem S
160 let ψ : ∀ i, TopologicalAbelianization S.inverseLimit →ₜ* T.X i := fun i =>
161 TopologicalAbelianization.map
162 { toMonoidHom :=
163 { toFun := S.projection i
164 map_one' := rfl
165 map_mul' := by intro x y; rfl }
166 continuous_toFun := S.continuous_projection i }
167 let ψFun : ∀ i, TopologicalAbelianization S.inverseLimit → T.X i := fun i => ψ i
168 have hψ : ∀ i, Continuous (ψFun i) := by
169 intro i
170 exact (ψ i).continuous_toFun
171 have hcompat : T.CompatibleMaps ψFun := by
172 intro i j hij
173 funext x
174 refine Quotient.inductionOn' x ?_
175 intro a
176 change
177 QuotientGroup.mk'
178 (Subgroup.topologicalClosure (commutator (S.X i)))
179 (S.map hij (S.projection j a)) =
180 QuotientGroup.mk'
181 (Subgroup.topologicalClosure (commutator (S.X i)))
182 (S.projection i a)
183 simpa using congrArg
184 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))
185 (S.projection_compatible a i j hij)
186 refine
187 { toMonoidHom :=
188 { toFun := T.inverseLimitLift ψFun hcompat
189 map_one' := by
190 apply T.ext
191 intro i
192 change ψFun i 1 = 1
194 map_mul' := by
195 intro x y
196 apply T.ext
197 intro i
198 change ψFun i (x * y) = ψFun i x * ψFun i y
200 continuous_toFun := T.continuous_inverseLimitLift ψFun hψ hcompat }
202/-- The `i`th projection of the canonical comparison map is the abelianization of the `i`th limit
203projection. -/
204@[simp 900] theorem π_topologicalAbelianizationInverseLimitComparison
205 {I : Type u} [Preorder I]
206 (S : InverseSystems.InverseSystem (I := I))
207 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
208 [∀ i, IsTopologicalGroup (S.X i)]
209 (i : I) :
210 (abelianizationInverseSystem S).projection i ∘
212 TopologicalAbelianization.map
213 { toMonoidHom :=
214 { toFun := S.projection i
215 map_one' := rfl
216 map_mul' := by intro x y; rfl }
217 continuous_toFun := S.continuous_projection i } := by
218 let T := abelianizationInverseSystem S
219 let ψ : ∀ i, TopologicalAbelianization S.inverseLimit →ₜ* T.X i := fun i =>
220 TopologicalAbelianization.map
221 { toMonoidHom :=
222 { toFun := S.projection i
223 map_one' := rfl
224 map_mul' := by intro x y; rfl }
225 continuous_toFun := S.continuous_projection i }
226 let ψFun : ∀ i, TopologicalAbelianization S.inverseLimit → T.X i := fun i => ψ i
227 have hcompat : T.CompatibleMaps ψFun := by
228 intro i j hij
229 funext x
230 refine Quotient.inductionOn' x ?_
231 intro a
232 change
233 QuotientGroup.mk'
234 (Subgroup.topologicalClosure (commutator (S.X i)))
235 (S.map hij (S.projection j a)) =
236 QuotientGroup.mk'
237 (Subgroup.topologicalClosure (commutator (S.X i)))
238 (S.projection i a)
239 simpa using congrArg
240 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))
241 (S.projection_compatible a i j hij)
242 funext x
243 change T.projection i (T.inverseLimitLift ψFun hcompat x) = ψFun i x
244 rfl
246/-- Evaluation of the canonical comparison map on a representative of the inverse limit. -/
247@[simp 900] theorem π_topologicalAbelianizationInverseLimitComparison_mk
248 {I : Type u} [Preorder I]
249 (S : InverseSystems.InverseSystem (I := I))
250 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
251 [∀ i, IsTopologicalGroup (S.X i)]
252 (i : I) (x : S.inverseLimit) :
253 (abelianizationInverseSystem S).projection i
255 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator S.inverseLimit)) x)) =
256 QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))) (S.projection i x) := by
257 simpa [Function.comp] using
258 congrFun (π_topologicalAbelianizationInverseLimitComparison (S := S) i)
259 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator S.inverseLimit)) x)
261/-- The induced map on inverse limits from the stagewise quotient morphism is the composite of the
262limit quotient map with the canonical comparison map. -/
263@[simp 900] theorem limMap_toAbelianizationInverseSystem_apply
264 {I : Type u} [Preorder I]
265 (S : InverseSystems.InverseSystem (I := I))
266 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
267 [∀ i, IsTopologicalGroup (S.X i)]
268 (x : S.inverseLimit) :
269 S.limMap (toAbelianizationInverseSystem S) x =
271 (TopologicalAbelianization.mk S.inverseLimit x) := by
272 apply (abelianizationInverseSystem S).ext
273 intro i
274 calc
275 (abelianizationInverseSystem S).projection i (S.limMap (toAbelianizationInverseSystem S) x)
276 = (toAbelianizationInverseSystem S).map i (S.projection i x) := by
277 simpa [Function.comp] using
278 congrFun
279 (InverseSystems.InverseSystem.π_comp_limMap
280 (S := S) (Θ := toAbelianizationInverseSystem S) i)
281 x
282 _ = QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))) (S.projection i x) := rfl
283 _ = (abelianizationInverseSystem S).projection i
285 (TopologicalAbelianization.mk S.inverseLimit x)) := by
286 symm
287 exact π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x
289/-- Proof-level injectivity of the canonical comparison map, used to build the continuous
290equivalence. The public API is `injective_topologicalAbelianizationInverseLimitComparison`. -/
292 {I : Type u} [Preorder I] [Nonempty I]
293 (S : InverseSystems.InverseSystem (I := I))
294 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
295 [∀ i, IsTopologicalGroup (S.X i)]
296 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
297 [∀ i, TotallyDisconnectedSpace (S.X i)]
298 (hdir : Directed (· ≤ ·) (id : I → I)) :
299 Function.Injective (topologicalAbelianizationInverseLimitComparison S) := by
301 letI : CompactSpace S.inverseLimit := inferInstance
302 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
303 letI : TotallyDisconnectedSpace S.inverseLimit := S.totallyDisconnectedSpace_inverseLimit
304 let hProfInv : IsProfiniteGroup S.inverseLimit :=
305 ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
306 let hProfAb : IsProfiniteGroup (TopologicalAbelianization S.inverseLimit) :=
308 (G := S.inverseLimit) hProfInv
309 (N := Subgroup.topologicalClosure (commutator S.inverseLimit))
310 (Subgroup.isClosed_topologicalClosure (s := commutator S.inverseLimit))
311 letI : CompactSpace (TopologicalAbelianization S.inverseLimit) :=
312 IsProfiniteGroup.compactSpace hProfAb
313 letI : T2Space (TopologicalAbelianization S.inverseLimit) :=
314 IsProfiniteGroup.t2Space hProfAb
315 letI : TotallyDisconnectedSpace (TopologicalAbelianization S.inverseLimit) :=
316 IsProfiniteGroup.totallyDisconnectedSpace hProfAb
317 have hkerbot : f.toMonoidHom.ker = ⊥ := by
318 ext a
319 constructor
320 · intro ha
321 by_contra hane
323 (G := TopologicalAbelianization S.inverseLimit) hProfAb (x := a) hane with ⟨U, haU⟩
324 let Q := TopologicalAbelianization S.inverseLimit ⧸
325 (U : Subgroup (TopologicalAbelianization S.inverseLimit))
326 letI : Finite Q := openNormalSubgroup_finiteQuotient
327 (G := TopologicalAbelianization S.inverseLimit) U
328 letI : DiscreteTopology Q :=
329 QuotientGroup.discreteTopology
330 (openNormalSubgroup_isOpen (G := TopologicalAbelianization S.inverseLimit) U)
331 let qInv : S.inverseLimit →ₜ* TopologicalAbelianization S.inverseLimit :=
332 { toMonoidHom := TopologicalAbelianization.mk S.inverseLimit
333 continuous_toFun := continuous_quotient_mk' }
334 let β : S.inverseLimit →ₜ* Q :=
335 { toMonoidHom :=
336 (QuotientGroup.mk' (U : Subgroup (TopologicalAbelianization S.inverseLimit))).comp
337 qInv.toMonoidHom
338 continuous_toFun := continuous_quotient_mk'.comp qInv.continuous_toFun
339 }
340 rcases InverseSystems.InverseSystem.factors_through_projection_finite_group_hom
341 (S := S) hdir β.toMonoidHom β.continuous_toFun with ⟨i, βi, hβi_continuous, hβfac⟩
342 let βiCont : S.X i →ₜ* Q :=
343 { toMonoidHom := βi
344 continuous_toFun := hβi_continuous }
345 have hq : QuotientGroup.mk' (U : Subgroup (TopologicalAbelianization S.inverseLimit)) a = 1 := by
346 rcases QuotientGroup.mk'_surjective
347 (Subgroup.topologicalClosure (commutator S.inverseLimit)) a with ⟨x, rfl⟩
348 calc
349 QuotientGroup.mk'
350 (U : Subgroup (TopologicalAbelianization S.inverseLimit))
351 (TopologicalAbelianization.mk S.inverseLimit x)
352 = β x := rfl
353 _ = βi (S.projection i x) := by
354 simpa [Function.comp] using
355 congrArg
356 (fun g : S.inverseLimit → Q => g x)
357 hβfac
358 _ = TopologicalAbelianization.lift βiCont
359 (TopologicalAbelianization.mk (S.X i) (S.projection i x)) := by
360 symm
361 exact TopologicalAbelianization.lift_apply_mk βiCont (S.projection i x)
362 _ = TopologicalAbelianization.lift βiCont
363 ((abelianizationInverseSystem S).projection i
365 (TopologicalAbelianization.mk S.inverseLimit x))) := by
366 simpa [TopologicalAbelianization.mk] using
367 congrArg (TopologicalAbelianization.lift βiCont)
368 (π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x).symm
369 _ = TopologicalAbelianization.lift βiCont
370 ((abelianizationInverseSystem S).projection i 1) := by
372 (TopologicalAbelianization.mk S.inverseLimit x) = 1 by
373 simpa [MonoidHom.mem_ker, f] using ha]
374 _ = TopologicalAbelianization.lift βiCont (1 : TopologicalAbelianization (S.X i)) := by
375 rfl
377 exact haU <| (QuotientGroup.eq_one_iff
378 (N := (U : Subgroup (TopologicalAbelianization S.inverseLimit))) a).1 hq
379 · intro hx
380 rw [Subgroup.mem_bot] at hx
381 rw [MonoidHom.mem_ker]
383 exact (MonoidHom.ker_eq_bot_iff (f := f.toMonoidHom)).mp hkerbot
385/-- Membership in the closed commutator subgroup of a profinite inverse limit is detected
386coordinatewise. -/
388 {I : Type u} [Preorder I] [Nonempty I]
389 (S : InverseSystems.InverseSystem (I := I))
390 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
391 [∀ i, IsTopologicalGroup (S.X i)]
392 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
393 [∀ i, TotallyDisconnectedSpace (S.X i)]
394 (hdir : Directed (· ≤ ·) (id : I → I)) {x : S.inverseLimit} :
395 x ∈ Subgroup.closedCommutator S.inverseLimit ↔
396 ∀ i, S.projection i x ∈ Subgroup.closedCommutator (S.X i) := by
397 constructor
398 · intro hx i
399 have hxmk :
400 TopologicalAbelianization.mk S.inverseLimit x = 1 :=
401 (TopologicalAbelianization.mk_eq_one_iff (G := S.inverseLimit) (x := x)).2 hx
402 have hcoord :=
403 π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x
404 have hcoord' :
405 (abelianizationInverseSystem S).projection i
407 (TopologicalAbelianization.mk S.inverseLimit x)) =
408 TopologicalAbelianization.mk (S.X i) (S.projection i x) := by
409 simpa [TopologicalAbelianization.mk] using hcoord
410 rw [hxmk] at hcoord'
411 have hmk :
412 TopologicalAbelianization.mk (S.X i) (S.projection i x) = 1 := by
413 simpa using hcoord'.symm
414 exact (TopologicalAbelianization.mk_eq_one_iff
415 (G := S.X i) (x := S.projection i x)).1 hmk
416 · intro hxcoord
418 have hf :
419 f (TopologicalAbelianization.mk S.inverseLimit x) = 1 := by
420 apply (abelianizationInverseSystem S).ext
421 intro i
422 have hmk :
423 TopologicalAbelianization.mk (S.X i) (S.projection i x) = 1 :=
424 (TopologicalAbelianization.mk_eq_one_iff
425 (G := S.X i) (x := S.projection i x)).2 (hxcoord i)
426 simpa [f, TopologicalAbelianization.mk] using
427 (π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x).trans hmk
428 have hxmk :
429 TopologicalAbelianization.mk S.inverseLimit x = 1 := by
430 apply inj_topologicalAbelianizationInverseLimitComparison_of_profinite_inverse_system (S := S) hdir
431 simpa [f] using hf
432 exact (TopologicalAbelianization.mk_eq_one_iff (G := S.inverseLimit) (x := x)).1 hxmk
434/-- The closed commutator subgroup of a profinite inverse limit is the infimum of the
435pullbacks of the stagewise closed commutator subgroups. -/
437 {I : Type u} [Preorder I] [Nonempty I]
438 (S : InverseSystems.InverseSystem (I := I))
439 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
440 [∀ i, IsTopologicalGroup (S.X i)]
441 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
442 [∀ i, TotallyDisconnectedSpace (S.X i)]
443 (hdir : Directed (· ≤ ·) (id : I → I)) :
444 Subgroup.closedCommutator S.inverseLimit =
445 ⨅ i, (Subgroup.closedCommutator (S.X i)).comap
446 ({ toFun := S.projection i
447 map_one' := rfl
448 map_mul' := by intro x y; rfl } : S.inverseLimit →* S.X i) := by
449 ext x
450 rw [mem_closedCommutator_inverseLimit_iff (S := S) hdir (x := x)]
451 simp only [InverseSystems.InverseSystem.projection_apply, Subgroup.mem_iInf, Subgroup.mem_comap,
452 MonoidHom.coe_mk, OneHom.coe_mk]
454/-- For the closed-commutator compatible family, the generic quotient-limit kernel is the closed
455commutator subgroup of the inverse limit. -/
457 {I : Type u} [Preorder I] [Nonempty I]
458 (S : InverseSystems.InverseSystem (I := I))
459 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
460 [∀ i, IsTopologicalGroup (S.X i)]
461 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
462 [∀ i, TotallyDisconnectedSpace (S.X i)]
463 (hdir : Directed (· ≤ ·) (id : I → I)) :
465 Subgroup.closedCommutator S.inverseLimit := by
466 symm
468 InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.inverseLimitKernel,
469 InverseSystems.projectionHom]
470 using closedCommutator_inverseLimit_eq_iInf_comap (S := S) hdir
472/-- The generic quotient inverse-limit theorem specialized to the closed commutator family. -/
473noncomputable def closedCommutatorQuotientInverseLimitContinuousMulEquiv
474 {I : Type u} [Preorder I] [Nonempty I]
475 (S : InverseSystems.InverseSystem (I := I))
476 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
477 [∀ i, IsTopologicalGroup (S.X i)]
478 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
479 [∀ i, TotallyDisconnectedSpace (S.X i)]
480 (hdir : Directed (· ≤ ·) (id : I → I)) :
481 TopologicalAbelianization S.inverseLimit ≃ₜ*
482 (closedCommutatorCompatibleClosedNormalSubgroups S).quotientInverseSystem.inverseLimit := by
484 have hkernel :
485 (Subgroup.closedCommutator S.inverseLimit).map
486 (ContinuousMulEquiv.refl S.inverseLimit).toMulEquiv.toMonoidHom =
487 Q.inverseLimitKernel := by
488 rw [closedCommutatorCompatibleClosedNormalSubgroups_inverseLimitKernel (S := S) hdir]
489 ext x
490 constructor
491 · intro hx
492 rcases hx with ⟨y, hy, hyx⟩
493 simpa using hyx ▸ hy
494 · intro hx
495 exact ⟨x, hx, rfl⟩
496 exact (QuotientGroup.congrₜ
497 (Subgroup.closedCommutator S.inverseLimit) Q.inverseLimitKernel
498 (ContinuousMulEquiv.refl S.inverseLimit) hkernel).trans
499 (Q.quotientInverseLimitContinuousMulEquiv hdir)
501@[simp 900] theorem projection_closedCommutatorQuotientInverseLimitContinuousMulEquiv_mk
502 {I : Type u} [Preorder I] [Nonempty I]
503 (S : InverseSystems.InverseSystem (I := I))
504 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
505 [∀ i, IsTopologicalGroup (S.X i)]
506 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
507 [∀ i, TotallyDisconnectedSpace (S.X i)]
508 (hdir : Directed (· ≤ ·) (id : I → I))
509 (i : I) (x : S.inverseLimit) :
510 (closedCommutatorCompatibleClosedNormalSubgroups S).quotientInverseSystem.projection i
511 (closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir
512 (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)) =
513 QuotientGroup.mk'
515 (S.projection i x) := by
518 dsimp
519 change Q.quotientInverseSystem.projection i
520 (Q.quotientInverseLimitContinuousMulEquiv hdir
521 (QuotientGroup.mk' Q.inverseLimitKernel x)) =
522 QuotientGroup.mk' (Q.N i) (S.projection i x)
523 unfold InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseLimitContinuousMulEquiv
524 change Q.quotientInverseSystem.projection i
525 (Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x)) =
526 QuotientGroup.mk' (Q.N i) (S.projection i x)
527 exact Q.projection_quotientInverseLimitComparison_mk i x
529/-- Topological abelianization commutes with profinite inverse limits as a topological-group
530isomorphism. -/
531noncomputable def topologicalAbelianizationInverseLimitContinuousMulEquiv
532 {I : Type u} [Preorder I] [Nonempty I]
533 (S : InverseSystems.InverseSystem (I := I))
534 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
535 [∀ i, IsTopologicalGroup (S.X i)]
536 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
537 [∀ i, TotallyDisconnectedSpace (S.X i)]
538 (hdir : Directed (· ≤ ·) (id : I → I)) :
539 TopologicalAbelianization S.inverseLimit ≃ₜ*
540 (abelianizationInverseSystem S).inverseLimit := by
542 let E : InverseSystems.InverseSystem.InverseSystemIso Q.quotientInverseSystem
543 (abelianizationInverseSystem S) :=
544 { stageEquiv := fun _ => ContinuousMulEquiv.refl _
545 comm := by intro i j hij x; rfl }
546 exact (closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir).trans
547 E.inverseLimitContinuousMulEquiv
549@[simp 900] theorem topologicalAbelianizationInverseLimitContinuousMulEquiv_apply
550 {I : Type u} [Preorder I] [Nonempty I]
551 (S : InverseSystems.InverseSystem (I := I))
552 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
553 [∀ i, IsTopologicalGroup (S.X i)]
554 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
555 [∀ i, TotallyDisconnectedSpace (S.X i)]
556 (hdir : Directed (· ≤ ·) (id : I → I))
557 (x : TopologicalAbelianization S.inverseLimit) :
558 topologicalAbelianizationInverseLimitContinuousMulEquiv (S := S) hdir x =
560 refine Quotient.inductionOn' x ?_
561 intro g
562 apply (abelianizationInverseSystem S).ext
563 intro i
565 let E : InverseSystems.InverseSystem.InverseSystemIso Q.quotientInverseSystem
566 (abelianizationInverseSystem S) :=
567 { stageEquiv := fun _ => ContinuousMulEquiv.refl _
568 comm := by intro i j hij x; rfl }
569 change (abelianizationInverseSystem S).projection i
570 (E.inverseLimitContinuousMulEquiv
571 ((closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir)
572 (QuotientGroup.mk'
573 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))) =
574 (abelianizationInverseSystem S).projection i
576 (QuotientGroup.mk'
577 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))
578 change (abelianizationInverseSystem S).projection i
579 (Q.quotientInverseSystem.limMap E.toMorphism
580 ((closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir)
581 (QuotientGroup.mk'
582 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))) =
583 (abelianizationInverseSystem S).projection i
585 (QuotientGroup.mk'
586 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))
587 rw [Q.quotientInverseSystem.π_limMap_apply E.toMorphism i]
588 change Q.quotientInverseSystem.projection i
589 ((closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir)
590 (QuotientGroup.mk'
591 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g)) =
592 (abelianizationInverseSystem S).projection i
594 (QuotientGroup.mk'
595 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))
598 rfl
600/-- The inverse-limit comparison is injective, as a corollary of the continuous equivalence. -/
602 {I : Type u} [Preorder I] [Nonempty I]
603 (S : InverseSystems.InverseSystem (I := I))
604 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
605 [∀ i, IsTopologicalGroup (S.X i)]
606 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
607 [∀ i, TotallyDisconnectedSpace (S.X i)]
608 (hdir : Directed (· ≤ ·) (id : I → I)) :
609 Function.Injective (topologicalAbelianizationInverseLimitComparison S) := by
610 let e := topologicalAbelianizationInverseLimitContinuousMulEquiv (S := S) hdir
611 intro x y hxy
612 apply e.injective
613 simpa [e] using hxy
615/-- The inverse-limit comparison is surjective, as a corollary of the continuous equivalence. -/
617 {I : Type u} [Preorder I] [Nonempty I]
618 (S : InverseSystems.InverseSystem (I := I))
619 [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
620 [∀ i, IsTopologicalGroup (S.X i)]
621 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
622 [∀ i, TotallyDisconnectedSpace (S.X i)]
623 (hdir : Directed (· ≤ ·) (id : I → I)) :
624 Function.Surjective (topologicalAbelianizationInverseLimitComparison S) := by
625 let e := topologicalAbelianizationInverseLimitContinuousMulEquiv (S := S) hdir
626 intro y
627 rcases e.surjective y with ⟨x, hx⟩
628 refine ⟨x, ?_⟩
629 simpa [e] using hx
631end ProCGroups.Abelian