Source: ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
1import ProCGroups.Topologies.OpenSubgroup
2import ProCGroups.Topologies.Conjugation
3import ProCGroups.TopologicalGroups
4import ProCGroups.Abelian.TopologicalAbelianization
6/-!
7# Functorial topological abelianization
9Topological abelianization defines a functor from topological groups to
10commutative topological groups. Its universal property is expressed directly
11as an equivalence of morphism types for \(T_1\) targets.
12-/
14open CategoryTheory
15open scoped Topology commutatorElement
17namespace ProCGroups.Abelian
19universe u
21/--
22Topological abelianization as a functor from topological groups to commutative topological
23groups.
24-/
25noncomputable def topologicalAbelianizationFunctor : TopGrp.{u} ⥤ CommTopGrp.{u} where
26 obj G := CommTopGrp.of (TopologicalAbelianization G)
27 map {G H} f := CommTopGrp.ofHom (TopologicalAbelianization.map f.hom)
28 map_id G := by
29 apply CommTopGrp.hom_ext
30 exact TopologicalAbelianization.map_id G
31 map_comp f g := by
32 apply CommTopGrp.hom_ext
33 exact TopologicalAbelianization.map_comp g.hom f.hom
35/--
36The induced map on topological abelianizations sends a representative class to the class of its
37image.
38-/
39@[simp] theorem topologicalAbelianizationFunctor_map_apply_mk
40 {G H : TopGrp.{u}} (f : G ⟶ H) (x : G) :
41 topologicalAbelianizationFunctor.map f (TopologicalAbelianization.mk G x) =
42 TopologicalAbelianization.mk H (f x) :=
43 rfl
45/--
46Category-level Hom equivalence expressing the universal property of topological abelianization
47for commutative \(T_1\) targets.
48-/
49noncomputable def topologicalAbelianizationHomEquiv
50 (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A] :
51 (topologicalAbelianizationFunctor.obj G ⟶ A) ≃
52 (G ⟶ commTopGrpForgetToTopGrp.obj A) where
53 toFun φ := TopGrp.ofHom (φ.hom.comp (TopologicalAbelianization.mkₜ G))
54 invFun f := CommTopGrp.ofHom (TopologicalAbelianization.lift f.hom)
55 left_inv φ := by
56 apply CommTopGrp.hom_ext
57 apply TopologicalAbelianization.hom_ext
58 intro x
59 rfl
60 right_inv f := by
61 apply TopGrp.hom_ext
62 ext x
63 rfl
65/--
66The topological-abelianization hom equivalence evaluates a homomorphism by its induced map on
67representatives.
68-/
69@[simp] theorem topologicalAbelianizationHomEquiv_apply_hom
70 (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
71 (φ : topologicalAbelianizationFunctor.obj G ⟶ A) :
72 (topologicalAbelianizationHomEquiv G A φ).hom =
73 φ.hom.comp (TopologicalAbelianization.mkₜ G) :=
74 rfl
76/--
77The inverse topological-abelianization hom equivalence sends a coset representative to the
78corresponding homomorphism value.
79-/
80@[simp] theorem topologicalAbelianizationHomEquiv_symm_apply_mk
81 (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
82 (f : G ⟶ commTopGrpForgetToTopGrp.obj A) (x : G) :
83 (topologicalAbelianizationHomEquiv G A).symm f
84 (TopologicalAbelianization.mk G x) = f x :=
85 rfl
87/--
88The topological abelianization of the \(\top\) open subgroup is canonically the same as the
89topological abelianization of the ambient group.
90-/
91noncomputable def topologicalAbelianizationTopMulEquiv
92 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
93 TopologicalAbelianization ↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ*
94 TopologicalAbelianization G :=
95 TopologicalAbelianization.congr
96 (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
97 (H := G)
98 (OpenSubgroup.topContinuousMulEquiv G)
100/--
101The abelianization equivalence for a topological group equivalence sends representatives to
102representatives.
103-/
104@[simp] theorem topologicalAbelianizationTopMulEquiv_apply_mk
105 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
106 (x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :
107 topologicalAbelianizationTopMulEquiv
108 (G := G) (TopologicalAbelianization.mk ↥((⊤ : OpenSubgroup G) : Subgroup G) x) =
109 TopologicalAbelianization.mk G x.1 := by
110 calc
111 topologicalAbelianizationTopMulEquiv
112 (G := G) (TopologicalAbelianization.mk ↥((⊤ : OpenSubgroup G) : Subgroup G) x) =
113 TopologicalAbelianization.mk G ((OpenSubgroup.topContinuousMulEquiv G) x) :=
114 TopologicalAbelianization.congr_apply_mk
115 (OpenSubgroup.topContinuousMulEquiv G) x
116 _ = TopologicalAbelianization.mk G x.1 := rfl
118/-- The quotient G/N acts on the topological abelianization of N by conjugation. -/
119noncomputable def quotientConjugationTopologicalAbelianizationMap
120 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
121 (N : Subgroup G) [N.Normal] :
122 (G ⧸ N) →* MulAut (TopologicalAbelianization N) := by
123 let K : Subgroup N := Subgroup.closedCommutator N
124 have hKchar : K.TopologicallyCharacteristic :=
127 (G := G) N K
128 (fun n x => by
129 have hcomm :
130 ⁅n, x⁆ ∈ Subgroup.closedCommutator N :=
132 (Subgroup.commutator_mem_commutator (Subgroup.mem_top n) (Subgroup.mem_top x))
133 have hconj : (MulAut.conjNormal (n : G)) x = n * x * n⁻¹ := by
134 ext
135 simp only [MulAut.conjNormal_apply, Subgroup.coe_mul, InvMemClass.coe_inv]
136 rw [hconj]
137 simpa [K, commutatorElement_def, mul_assoc] using hcomm)
139/--
140The continuous self-equivalence of topological abelianization induced by conjugation by a
141representative.
142-/
143noncomputable def conjugationTopologicalAbelianizationContinuousAut
144 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
145 (N : Subgroup G) [N.Normal] (g : G) :
146 TopologicalAbelianization N ≃ₜ* TopologicalAbelianization N :=
147 TopologicalAbelianization.congr (Subgroup.conjNormalContinuousMulEquiv (G := G) N g)
149/--
150The representative-wise continuous automorphism has the same underlying algebraic action as
151quotientConjugationTopologicalAbelianizationMap.
152-/
153@[simp] theorem conjugationTopologicalAbelianizationContinuousAut_toMulAut_apply_mk
154 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
155 (N : Subgroup G) [N.Normal] (g : G) (n : N) :
156 conjugationTopologicalAbelianizationContinuousAut (G := G) N g
157 (TopologicalAbelianization.mk N n) =
158 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
159 (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n) := by
160 rfl
162/--
163The conjugation action on a quotient induces the expected map on topological abelianization
164representatives.
165-/
166@[simp] theorem quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
167 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
168 (N : Subgroup G) [N.Normal] (g : G) (n : N) :
169 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
170 (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n) =
171 TopologicalAbelianization.mk N ((MulAut.conjNormal g) n) := by
172 dsimp [quotientConjugationTopologicalAbelianizationMap, TopologicalAbelianization.mk,
173 TopologicalAbelianization.mkₜ]
174 rfl
176/--
177If every commutator correction lies in the closed commutator subgroup, the induced conjugation
178action on the topological abelianization is trivial.
179-/
180theorem quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure
181 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
182 (N : Subgroup G) [N.Normal] {x : G}
183 (hx :
184 ∀ n : N,
185 (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N) :
186 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
187 (QuotientGroup.mk' N x) = 1 := by
188 ext a
189 obtain ⟨n, rfl⟩ := QuotientGroup.mk'_surjective (Subgroup.closedCommutator N) a
190 exact
191 (QuotientGroup.eq_iff_div_mem (N := Subgroup.closedCommutator N)
192 (x := (MulAut.conjNormal x) n) (y := n)).2 (by
193 simpa [div_eq_mul_inv] using hx n)
195/--
196The conjugation action fixes a representative exactly when the correction term lies in the
197closed commutator subgroup.
198-/
199theorem quotientConjugationTopologicalAbelianizationMap_mk_apply_mk_eq_iff
200 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
201 {N : Subgroup G} [N.Normal] {x : G} {n : N} :
202 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
203 (QuotientGroup.mk' N x) (TopologicalAbelianization.mk N n) =
204 TopologicalAbelianization.mk N n ↔
205 (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N := by
206 rw [quotientConjugationTopologicalAbelianizationMap_mk_apply_mk]
207 change
208 QuotientGroup.mk' (Subgroup.closedCommutator N) ((MulAut.conjNormal x) n) =
209 QuotientGroup.mk' (Subgroup.closedCommutator N) n ↔
210 (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈
212 rw [show
213 QuotientGroup.mk' (Subgroup.closedCommutator N) ((MulAut.conjNormal x) n) =
214 ((MulAut.conjNormal x) n : TopologicalAbelianization N) by rfl,
215 show
216 QuotientGroup.mk' (Subgroup.closedCommutator N) n =
217 (n : TopologicalAbelianization N) by rfl,
218 QuotientGroup.eq_iff_div_mem, div_eq_mul_inv]
220/--
221The induced conjugation action is trivial exactly when every correction term lies in the closed
222commutator subgroup.
223-/
224theorem quotientConjugationTopologicalAbelianizationMap_mk_eq_one_iff
225 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
226 {N : Subgroup G} [N.Normal] {x : G} :
227 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
228 (QuotientGroup.mk' N x) = 1 ↔
229 ∀ n : N,
230 (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N := by
231 constructor
232 · intro h n
233 have hpoint :=
234 congrArg
235 (fun φ : MulAut (TopologicalAbelianization N) => φ (TopologicalAbelianization.mk N n))
236 h
237 exact
238 (quotientConjugationTopologicalAbelianizationMap_mk_apply_mk_eq_iff
239 (G := G) (N := N) (x := x) (n := n)).1 (by simpa using hpoint)
240 · intro hx
241 exact quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure
242 (G := G) (N := N) (x := x) hx
244/-- Central elements act trivially on the topological abelianization of a normal subgroup. -/
245theorem quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_mem_center
246 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
247 (N : Subgroup G) [N.Normal] {x : G} (hx : x ∈ Subgroup.center G) :
248 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
249 (QuotientGroup.mk' N x) = 1 := by
250 apply quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure
251 (G := G) (N := N)
252 intro n
253 have hxn : x * (n : G) = (n : G) * x := by
254 exact (Subgroup.mem_center_iff.mp hx (n : G)).symm
255 have hconj : MulAut.conjNormal x n = n := by
256 ext
257 rw [MulAut.conjNormal_apply]
258 simp only [hxn, mul_assoc, mul_inv_cancel, mul_one]
259 simp only [hconj, mul_inv_cancel, one_mem]
261/--
262If a representative commutes with an element of N, then the induced action fixes its class in
263the topological abelianization.
264-/
265theorem quotientConjAbMap_apply_mk_of_commute
266 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
267 (N : Subgroup G) [N.Normal] {g : G} {x : N}
268 (hgx : g * (x : G) = (x : G) * g) :
269 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
270 (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N x) =
271 TopologicalAbelianization.mk N x := by
272 have hconj : (MulAut.conjNormal g) x = x := by
273 ext
274 rw [MulAut.conjNormal_apply]
275 simp only [hgx, mul_assoc, mul_inv_cancel, mul_one]
276 rw [quotientConjugationTopologicalAbelianizationMap_mk_apply_mk, hconj]
278/-- The image of \(S\cap U\) in the topological abelianization of \(U\). -/
279noncomputable def subgroupImageInTopologicalAbelianization
280 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
281 (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
282 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q)) :=
283 (((S ⊓ (U : Subgroup Q)).subgroupOf (U : Subgroup Q)).map
284 (TopologicalAbelianization.mk ↥(U : Subgroup Q)))
286/--
287Membership in the subgroup image inside the topological abelianization is equivalent to the
288displayed coordinate condition.
289-/
290@[simp] theorem mem_subgroupImageInTopologicalAbelianization_iff
291 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
292 {S : Subgroup Q} {U : OpenNormalSubgroup Q}
293 {y : TopologicalAbelianization ↥(U : Subgroup Q)} :
294 y ∈ subgroupImageInTopologicalAbelianization (Q := Q) S U ↔
295 ∃ x : ↥(U : Subgroup Q), (x : Q) ∈ S ∧ TopologicalAbelianization.mk _ x = y := by
296 simp only [subgroupImageInTopologicalAbelianization, ContinuousMonoidHom.coe_toMonoidHom,
297 Subgroup.inf_subgroupOf_right, Subgroup.mem_map, Subgroup.mem_subgroupOf, MonoidHom.coe_coe,
298 Subtype.exists,
299 OpenSubgroup.mem_toSubgroup, exists_and_left]
301/-- Enlarging the ambient subgroup \(S\) enlarges its image in the abelianization of \(U\). -/
302theorem subgroupImageInTopologicalAbelianization_mono_left
303 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
304 {S T : Subgroup Q} (hST : S ≤ T) (U : OpenNormalSubgroup Q) :
305 subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
306 subgroupImageInTopologicalAbelianization (Q := Q) T U := by
307 intro y hy
308 rcases (mem_subgroupImageInTopologicalAbelianization_iff
309 (Q := Q) (S := S) (U := U) (y := y)).1 hy with
310 ⟨x, hxS, hxy⟩
311 exact (mem_subgroupImageInTopologicalAbelianization_iff
312 (Q := Q) (S := T) (U := U) (y := y)).2
313 ⟨x, hST hxS, hxy⟩
315/--
316An inclusion of open normal subgroups induces the corresponding map on topological
317abelianizations.
318-/
319noncomputable def topologicalAbelianizationMapOfOpenNormalSubgroupLe
320 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
321 {U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
322 TopologicalAbelianization ↥(U : Subgroup Q) →ₜ*
323 TopologicalAbelianization ↥(V : Subgroup Q) :=
324 TopologicalAbelianization.map
325 { toMonoidHom := Subgroup.inclusion hUV
326 continuous_toFun := by
327 apply Continuous.subtype_mk
328 exact continuous_subtype_val }
330/--
331The induced map on topological abelianizations sends a representative class to the class of its
332image.
333-/
334@[simp] theorem topologicalAbelianizationMapOfOpenNormalSubgroupLe_apply_mk
335 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
336 {U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q))
337 (x : ↥(U : Subgroup Q)) :
338 topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV
339 (TopologicalAbelianization.mk ↥(U : Subgroup Q) x) =
340 TopologicalAbelianization.mk ↥(V : Subgroup Q) ⟨x.1, hUV x.2⟩ :=
341 rfl
343/-- Under an inclusion U \(\leq\) V, the image from U maps into the image from V. -/
344theorem subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le
345 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
346 (S : Subgroup Q) {U V : OpenNormalSubgroup Q}
347 (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
348 (subgroupImageInTopologicalAbelianization (Q := Q) S U).map
349 (topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHom ≤
350 subgroupImageInTopologicalAbelianization (Q := Q) S V := by
351 intro y hy
352 rcases hy with ⟨x, hx, rfl⟩
353 rcases (mem_subgroupImageInTopologicalAbelianization_iff
354 (Q := Q) (S := S) (U := U) (y := x)).1 hx with
355 ⟨a, haS, hax⟩
356 rw [← hax]
357 exact (mem_subgroupImageInTopologicalAbelianization_iff
358 (Q := Q) (S := S) (U := V) (y := _)).2
359 ⟨⟨a.1, hUV a.2⟩, haS, rfl⟩
361/-- Comap form of subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le. -/
362theorem subgroupImageInTopologicalAbelianization_le_comap_of_openNormalSubgroup_le
363 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
364 (S : Subgroup Q) {U V : OpenNormalSubgroup Q}
365 (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
366 subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
367 (subgroupImageInTopologicalAbelianization (Q := Q) S V).comap
368 (topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHom :=
369 Subgroup.map_le_iff_le_comap.mp
370 (subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le
371 (Q := Q) S hUV)
373namespace OpenNormalAbelianizationImage
375/--
376The image of \(S\) has finite abstract index in the topological abelianization of every open
377normal supergroup of \(K\).
378-/
379def FiniteAbstractIndex
380 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
381 (S K : Subgroup Q) : Prop :=
382 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
383 Finite
384 ((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
385 subgroupImageInTopologicalAbelianization (Q := Q) S U)
387/--
388The topological closure of the image of \(S \cap U\) in the topological abelianization of \(U\).
389-/
390noncomputable def closedSubgroupImageInTopologicalAbelianization
391 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
392 (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
393 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q)) :=
394 (subgroupImageInTopologicalAbelianization (Q := Q) S U).topologicalClosure
396/--
397The image of a closed subgroup in the topological abelianization is the corresponding
398topological closure.
399-/
400@[simp] theorem closedSubgroupImageInTopologicalAbelianization_eq_topologicalClosure
401 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
402 (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
403 closedSubgroupImageInTopologicalAbelianization (Q := Q) S U =
404 (subgroupImageInTopologicalAbelianization (Q := Q) S U).topologicalClosure :=
405 rfl
407/-- The closed image of \(S\) is open in every open normal supergroup of \(K\). -/
408def OpenClosure
409 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
410 (S K : Subgroup Q) : Prop :=
411 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
412 IsOpen
413 ((closedSubgroupImageInTopologicalAbelianization (Q := Q) S U :
414 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) : Set
415 (TopologicalAbelianization ↥(U : Subgroup Q)))
417/--
418The image of \(S\) is closed and has finite quotient in every open normal supergroup of \(K\).
419-/
420def FiniteTopologicalIndex
421 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
422 (S K : Subgroup Q) : Prop :=
423 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
424 IsClosed
425 ((subgroupImageInTopologicalAbelianization (Q := Q) S U :
426 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) : Set
427 (TopologicalAbelianization ↥(U : Subgroup Q))) ∧
428 Finite
429 ((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
430 subgroupImageInTopologicalAbelianization (Q := Q) S U)
432/-- Finite topological index includes finite abstract index as its quotient-size component. -/
433theorem finiteAbstractIndex_of_finiteTopologicalIndex
434 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
435 {S K : Subgroup Q}
436 (h : FiniteTopologicalIndex (Q := Q) S K) :
437 FiniteAbstractIndex (Q := Q) S K :=
438 fun U hKU => (h U hKU).2
440end OpenNormalAbelianizationImage
442end ProCGroups.Abelian