Source: ProCGroups.Abelian.TopologicalAbelianization
1import Mathlib.Topology.Algebra.Group.TopologicalAbelianization
2import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
4/-!
5# Topological abelianization
7This module develops the canonical quotient by the closed commutator subgroup, its universal
8property for continuous maps to Hausdorff commutative groups, and the induced quotient topology.
9-/
11open scoped Topology commutatorElement
13namespace ProCGroups.Abelian
15universe u v
17namespace TopologicalAbelianization
19/-- The natural continuous quotient map to the topological abelianization. -/
20def mkₜ
21 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
22 G →ₜ* TopologicalAbelianization G :=
23 { toMonoidHom := QuotientGroup.mk' (Subgroup.closedCommutator G)
24 continuous_toFun := QuotientGroup.continuous_mk }
26/-- The natural quotient homomorphism to the topological abelianization. -/
27abbrev mk
28 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
29 G →* TopologicalAbelianization G :=
30 (mkₜ G).toMonoidHom
32/-- The kernel of the topological abelianization map is the closed commutator subgroup. -/
33theorem ker_mk
34 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
35 (mk G).ker =
36 Subgroup.closedCommutator G := by
37 exact QuotientGroup.ker_mk' _
39/--
40A representative maps to \(1\) in the topological abelianization exactly when it lies in the
41closed commutator subgroup.
42-/
43theorem mk_eq_one_iff
44 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
45 {x : G} :
46 mk G x = 1 ↔
47 x ∈ Subgroup.closedCommutator G := by
48 exact QuotientGroup.eq_one_iff (N := Subgroup.closedCommutator G) x
50/-- In a commutative \(T_1\) topological group, the closed commutator subgroup is trivial. -/
51@[simp] theorem closedCommutator_eq_bot_of_commGroup_t1
52 (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
53 Subgroup.closedCommutator G = ⊥ := by
54 have hcomm : commutator G = ⊥ := by
55 rw [commutator_eq_bot_iff_center_eq_top, CommGroup.center_eq_top]
56 rw [Subgroup.closedCommutator, hcomm]
57 ext x
58 change x ∈ closure ({(1 : G)} : Set G) ↔ x = 1
59 rw [closure_singleton]
60 simp only [Set.mem_singleton_iff]
62/-- The canonical map to the topological abelianization is surjective. -/
63theorem surjective_mk
64 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
65 Function.Surjective (mk G) :=
66 QuotientGroup.mk'_surjective (Subgroup.closedCommutator G)
68/--
69The topological abelianization is Hausdorff because it is a quotient by the closed commutator
70subgroup.
71-/
72instance instT2SpaceTopologicalAbelianization
73 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
74 T2Space (TopologicalAbelianization G) := by
75 letI : IsClosed (((Subgroup.closedCommutator G : Subgroup G) : Set G)) :=
77 infer_instance
79/--
80A continuous homomorphism to a commutative \(T_1\) topological group factors through the
81topological abelianization.
82-/
83noncomputable def lift
84 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
85 {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
86 (f : G →ₜ* A) :
87 TopologicalAbelianization G →ₜ* A := by
88 have hclosedCommutator_le_ker :
89 Subgroup.closedCommutator G ≤ f.toMonoidHom.ker := by
90 have hcomm : commutator G ≤ f.toMonoidHom.ker := by
91 rw [commutator_eq_closure]
92 rw [Subgroup.closure_le]
93 rintro x ⟨g, h, rfl⟩
94 change f ⁅g, h⁆ = 1
95 simp only [commutatorElement_def, mul_assoc, map_mul, map_inv, mul_inv_cancel_comm_assoc,
96 mul_inv_cancel]
97 have hkerClosed : IsClosed (((f.toMonoidHom.ker : Subgroup G) : Set G)) := by
98 change IsClosed (f ⁻¹' ({1} : Set A))
99 simpa using isClosed_singleton.preimage f.continuous_toFun
100 exact Subgroup.topologicalClosure_minimal
101 (s := commutator G) (t := f.toMonoidHom.ker) hcomm hkerClosed
102 exact QuotientGroup.liftₜ (Subgroup.closedCommutator G) f hclosedCommutator_le_ker
104/--
105The lift from the topological abelianization evaluates on a quotient class by applying the
106original homomorphism.
107-/
108@[simp] theorem lift_apply_mk
109 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
110 {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
111 (f : G →ₜ* A) (x : G) :
112 lift f (mk G x) = f x := by
113 rfl
115/--
116Continuous homomorphisms out of the topological abelianization are equal when they agree after
117the quotient map.
118-/
119@[ext] theorem hom_ext
120 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
121 {A : Type v} [TopologicalSpace A] [Group A]
122 (φ ψ : TopologicalAbelianization G →ₜ* A)
123 (h : ∀ x : G, φ (mk G x) = ψ (mk G x)) :
124 φ = ψ := by
125 apply ContinuousMonoidHom.toMonoidHom_injective
126 apply MonoidHom.ext
127 intro x
128 exact Quotient.inductionOn' x h
130/--
131The lift from the topological abelianization is uniquely determined by its composition with the
132quotient map.
133-/
134theorem lift_unique
135 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
136 {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
137 (f : G →ₜ* A)
138 (φ : TopologicalAbelianization G →ₜ* A)
139 (hφ : ∀ x : G, φ (mk G x) = f x) :
140 φ = lift f := by
141 apply hom_ext
142 intro x
143 calc
144 φ (mk G x) = f x := hφ x
145 _ = lift f (mk G x) := (lift_apply_mk f x).symm
147/--
148The universal property of topological abelianization as a Hom equivalence for commutative
149\(T_1\) targets.
150-/
151noncomputable def homEquiv
152 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
153 (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A] :
154 (TopologicalAbelianization G →ₜ* A) ≃ (G →ₜ* A) where
155 toFun φ := φ.comp (mkₜ G)
156 invFun f := lift f
157 left_inv φ := by
158 apply hom_ext
159 intro x
160 rfl
161 right_inv f := by
162 ext x
163 rfl
165/--
166The Hom-equivalence is evaluated by composing a map out of the topological abelianization with
167the quotient map from the original group.
168-/
169@[simp] theorem homEquiv_apply
170 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
171 (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
172 (φ : TopologicalAbelianization G →ₜ* A) :
173 homEquiv G A φ = φ.comp (mkₜ G) :=
174 rfl
176/--
177The inverse Hom equivalence evaluates on the abelianization class of \(x\) as the original
178continuous homomorphism evaluated at \(x\).
179-/
180@[simp] theorem homEquiv_symm_apply_mk
181 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
182 (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
183 (f : G →ₜ* A) (x : G) :
184 (homEquiv G A).symm f (mk G x) = f x :=
185 rfl
187/-- A continuous homomorphism induces a continuous homomorphism on topological abelianizations. -/
188noncomputable def map
189 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
190 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
191 (f : G →ₜ* H) :
192 TopologicalAbelianization G →ₜ* TopologicalAbelianization H :=
193 lift ((mkₜ H).comp f)
195/-- The induced map on topological abelianizations is evaluated on quotient representatives. -/
196@[simp] theorem map_apply_mk
197 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
198 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
199 (f : G →ₜ* H) (x : G) :
200 map f (mk G x) =
201 mk H (f x) := by
202 rfl
204/--
205Composing the abelianization map with the quotient map recovers the quotient map after applying
206the original homomorphism.
207-/
208@[simp] theorem map_comp_mk
209 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
210 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
211 (f : G →ₜ* H) :
212 (map f).toMonoidHom.comp (mk G) =
213 (mk H).comp f.toMonoidHom := by
214 ext x
215 rfl
217/--
218The map induced by the identity homomorphism is the identity on the topological abelianization.
219-/
220@[simp] theorem map_id
221 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
222 map
223 (ContinuousMonoidHom.id G) =
224 ContinuousMonoidHom.id (TopologicalAbelianization G) := by
225 apply hom_ext
226 intro g
227 rfl
229/-- Induced maps on topological abelianizations compose functorially. -/
230@[simp] theorem map_comp
231 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
232 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
233 {K : Type _} [TopologicalSpace K] [Group K] [IsTopologicalGroup K]
234 (g : H →ₜ* K) (f : G →ₜ* H) :
235 map (g.comp f) =
236 (map g).comp (map f) := by
237 apply hom_ext
238 intro a
239 rfl
241/-- A topological group isomorphism induces an isomorphism on topological abelianizations. -/
242noncomputable def congr
243 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
244 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
245 (e : G ≃ₜ* H) :
246 TopologicalAbelianization G ≃ₜ* TopologicalAbelianization H := by
247 let f := map (ContinuousMonoidHom.toContinuousMonoidHom e)
248 let g := map (ContinuousMonoidHom.toContinuousMonoidHom e.symm)
249 exact ContinuousMulEquiv.ofHomInv f g
250 (by
251 intro x
252 refine Quotient.inductionOn' x ?_
253 intro a
254 change
255 map (ContinuousMonoidHom.toContinuousMonoidHom e.symm)
256 (map (ContinuousMonoidHom.toContinuousMonoidHom e)
257 (mk G a)) =
258 mk G a
259 rw [map_apply_mk, map_apply_mk]
260 simp only [ContinuousMonoidHom.coe_toMonoidHom, ContinuousMonoidHom.coe_coe,
261 ContinuousMulEquiv.symm_apply_apply, MonoidHom.coe_coe])
262 (by
263 intro y
264 refine Quotient.inductionOn' y ?_
265 intro b
266 change
267 map (ContinuousMonoidHom.toContinuousMonoidHom e)
268 (map (ContinuousMonoidHom.toContinuousMonoidHom e.symm)
269 (mk H b)) =
270 mk H b
271 rw [map_apply_mk, map_apply_mk]
272 simp only [ContinuousMonoidHom.coe_toMonoidHom, ContinuousMonoidHom.coe_coe,
273 ContinuousMulEquiv.apply_symm_apply, MonoidHom.coe_coe])
275/--
276The abelianization congruence induced by a continuous equivalence sends representatives to
277representatives.
278-/
279@[simp] theorem congr_apply_mk
280 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
281 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
282 (e : G ≃ₜ* H) (x : G) :
283 congr e (mk G x) =
284 mk H (e x) := by
285 rfl
287/-- Surjective homomorphisms induce surjective maps on topological abelianizations. -/
288theorem surjective_map_of_surjective
289 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
290 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
291 (f : G →ₜ* H) (hf : Function.Surjective f) :
292 Function.Surjective (map f) := by
293 intro y
294 refine Quotient.inductionOn' y ?_
295 intro h
296 rcases hf h with ⟨g, rfl⟩
297 exact ⟨QuotientGroup.mk' (Subgroup.closedCommutator G) g, rfl⟩
299/--
300In a commutative \(T_1\) topological group, the natural map to the topological abelianization is
301injective.
302-/
303theorem injective_mk_of_commGroup
304 {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
305 Function.Injective (mk G) := by
306 rw [← MonoidHom.ker_eq_bot_iff]
307 rw [ker_mk, closedCommutator_eq_bot_of_commGroup_t1]
309/-- The canonical continuous equivalence for commutative \(T_1\) groups. -/
310noncomputable def continuousMulEquivOfCommGroup
311 (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
312 _root_.TopologicalAbelianization G ≃ₜ* G := by
313 let e : G ≃* _root_.TopologicalAbelianization G :=
314 MulEquiv.ofBijective (mk G)
315 ⟨injective_mk_of_commGroup (G := G),
316 QuotientGroup.mk'_surjective (Subgroup.closedCommutator G)⟩
317 refine
318 { toMulEquiv := e.symm
319 continuous_toFun := ?_
320 continuous_invFun := ?_ }
321 · refine
322 (QuotientGroup.isQuotientMap_mk
323 (Subgroup.closedCommutator G)).continuous_iff.2 ?_
324 change Continuous fun x : G => e.symm (e x)
325 have heq : (fun x : G => e.symm (e x)) = id := by
326 funext x
327 exact e.symm_apply_apply x
328 rw [heq]
329 exact continuous_id
330 · change Continuous fun x : G => mk G x
331 exact QuotientGroup.continuous_mk
333end TopologicalAbelianization
335end ProCGroups.Abelian