Yamaguchi Lean 4 Library
ProCGroups/Abelian/TopologicalAbelianization.lean
ProCGroups/Abelian/TopologicalAbelianization/Source

ProCGroups/Abelian/TopologicalAbelianization.lean

1import Mathlib.Topology.Algebra.Group.TopologicalAbelianization
2import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Abelian/TopologicalAbelianization.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Topological abelianization
15Defines the canonical quotient by the closed commutator subgroup and records the universal property, representative formulas, functoriality, and the commutative T1 case.
16-/
18open scoped Topology
20namespace ProCGroups.Abelian
22universe u v
24namespace TopologicalAbelianization
26/-- The natural continuous quotient map to the topological abelianization. -/
28 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
29 G →ₜ* TopologicalAbelianization G :=
30 { toMonoidHom := QuotientGroup.mk' (Subgroup.closedCommutator G)
31 continuous_toFun := QuotientGroup.continuous_mk }
33/-- The natural quotient homomorphism to the topological abelianization. -/
34abbrev mk
35 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
36 G →* TopologicalAbelianization G :=
37 (mkₜ G).toMonoidHom
39/-- The kernel of the topological abelianization map is the closed commutator subgroup. -/
40theorem ker_mk
41 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
42 (mk G).ker =
44 exact QuotientGroup.ker_mk' _
46/-- A representative maps to `1` in the topological abelianization exactly when it lies in the closed commutator subgroup. -/
48 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
49 {x : G} :
50 mk G x = 1 ↔
52 exact QuotientGroup.eq_one_iff (N := Subgroup.closedCommutator G) x
54/-- In a commutative `T1` topological group, the closed commutator subgroup is trivial. -/
56 (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
58 have hcomm : commutator G = ⊥ := by
59 rw [commutator_eq_bot_iff_center_eq_top, CommGroup.center_eq_top]
61 ext x
62 change x ∈ closure ({(1 : G)} : Set G) ↔ x = 1
63 rw [closure_singleton]
64 simp only [Set.mem_singleton_iff]
66/-- The canonical map to the topological abelianization is surjective. -/
68 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
69 Function.Surjective (mk G) :=
70 QuotientGroup.mk'_surjective (Subgroup.closedCommutator G)
72/-- The quotient by the closed commutator subgroup is Hausdorff.
74This instance deliberately does not assume `T2Space G`: `TopologicalAbelianization G` is
76closed-subgroup hypothesis used by mathlib's `QuotientGroup.instT2Space`. -/
78 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
79 T2Space (TopologicalAbelianization G) := by
80 letI : IsClosed (((Subgroup.closedCommutator G : Subgroup G) : Set G)) :=
82 infer_instance
84/-- A continuous homomorphism to a commutative `T1` topological group factors through the
85topological abelianization. -/
86noncomputable def lift
87 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
88 {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
89 (f : G →ₜ* A) :
90 TopologicalAbelianization G →ₜ* A := by
91 have hclosedCommutator_le_ker :
92 Subgroup.closedCommutator G ≤ f.toMonoidHom.ker := by
93 have hcomm : commutator G ≤ f.toMonoidHom.ker := by
94 rw [commutator_eq_closure]
95 rw [Subgroup.closure_le]
96 rintro x ⟨g, h, rfl⟩
97 change f ⁅g, h⁆ = 1
98 simp only [commutatorElement_def, mul_assoc, map_mul, map_inv, mul_inv_cancel_comm_assoc, mul_inv_cancel]
99 have hkerClosed : IsClosed (((f.toMonoidHom.ker : Subgroup G) : Set G)) := by
100 change IsClosed (f ⁻¹' ({1} : Set A))
101 simpa using isClosed_singleton.preimage f.continuous_toFun
102 exact Subgroup.topologicalClosure_minimal
103 (s := commutator G) (t := f.toMonoidHom.ker) hcomm hkerClosed
104 exact QuotientGroup.liftₜ (Subgroup.closedCommutator G) f hclosedCommutator_le_ker
106/-- The lift from the topological abelianization evaluates on a quotient class by applying the original homomorphism. -/
107@[simp] theorem lift_apply_mk
108 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
109 {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
110 (f : G →ₜ* A) (x : G) :
111 lift f (mk G x) = f x := by
112 rfl
114/-- Continuous homomorphisms out of the topological abelianization are equal when they agree after the quotient map. -/
115@[ext] theorem hom_ext
116 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
117 {A : Type v} [TopologicalSpace A] [Group A]
118 (φ ψ : TopologicalAbelianization G →ₜ* A)
119 (h : ∀ x : G, φ (mk G x) = ψ (mk G x)) :
120 φ = ψ := by
121 apply ContinuousMonoidHom.toMonoidHom_injective
122 apply MonoidHom.ext
123 intro x
124 exact Quotient.inductionOn' x h
126/-- The lift from the topological abelianization is uniquely determined by its composition with the quotient map. -/
127theorem lift_unique
128 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
129 {A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
130 (f : G →ₜ* A)
131 (φ : TopologicalAbelianization G →ₜ* A)
132 (hφ : ∀ x : G, φ (mk G x) = f x) :
133 φ = lift f := by
134 apply hom_ext
135 intro x
136 simpa using hφ x
138/-- The universal property of topological abelianization as a Hom equivalence for commutative
139`T1` targets. -/
140noncomputable def homEquiv
141 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
142 (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A] :
143 (TopologicalAbelianization G →ₜ* A) ≃ (G →ₜ* A) where
144 toFun φ := φ.comp (mkₜ G)
145 invFun f := lift f
146 left_inv φ := by
147 apply hom_ext
148 intro x
149 rfl
150 right_inv f := by
151 ext x
152 rfl
154@[simp] theorem homEquiv_apply
155 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
156 (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
157 (φ : TopologicalAbelianization G →ₜ* A) :
158 homEquiv G A φ = φ.comp (mkₜ G) :=
159 rfl
162 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
163 (A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
164 (f : G →ₜ* A) (x : G) :
165 (homEquiv G A).symm f (mk G x) = f x :=
166 rfl
168/-- The map induced on topological abelianizations by a continuous homomorphism. -/
169noncomputable def map
170 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
171 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
172 (f : G →ₜ* H) :
173 TopologicalAbelianization G →ₜ* TopologicalAbelianization H :=
174 lift ((mkₜ H).comp f)
176/-- The map on topological abelianizations sends the class of an element to the class of its image. -/
177@[simp] theorem map_apply_mk
178 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
179 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
180 (f : G →ₜ* H) (x : G) :
181 map f (mk G x) =
182 mk H (f x) := by
183 rfl
185/-- Composing the abelianization map with the quotient map recovers the quotient map after applying the original homomorphism. -/
186@[simp] theorem map_comp_mk
187 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
188 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
189 (f : G →ₜ* H) :
190 (map f).toMonoidHom.comp (mk G) =
191 (mk H).comp f.toMonoidHom := by
192 ext x
193 rfl
195/-- The map induced on topological abelianizations by the identity homomorphism is the identity. -/
196@[simp] theorem map_id
197 (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
198 map
199 (ContinuousMonoidHom.id G) =
200 ContinuousMonoidHom.id (TopologicalAbelianization G) := by
201 apply hom_ext
202 intro g
203 rfl
205/-- Maps induced on topological abelianizations compose as expected. -/
206@[simp] theorem map_comp
207 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
208 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
209 {K : Type _} [TopologicalSpace K] [Group K] [IsTopologicalGroup K]
210 (g : H →ₜ* K) (f : G →ₜ* H) :
211 map (g.comp f) =
212 (map g).comp (map f) := by
213 apply hom_ext
214 intro a
215 rfl
217/-- A topological group isomorphism induces an isomorphism on topological abelianizations. -/
218noncomputable def congr
219 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
220 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
221 (e : G ≃ₜ* H) :
222 TopologicalAbelianization G ≃ₜ* TopologicalAbelianization H := by
223 let f := map e.toContinuousMonoidHom
224 let g := map e.symm.toContinuousMonoidHom
226 (by
227 intro x
228 refine Quotient.inductionOn' x ?_
229 intro a
230 change
231 map e.symm.toContinuousMonoidHom
232 (map e.toContinuousMonoidHom
233 (mk G a)) =
234 mk G a
236 simp only [ContinuousMonoidHom.coe_toMonoidHom, ContinuousMulEquiv.toContinuousMonoidHom_apply,
237 ContinuousMulEquiv.symm_apply_apply, MonoidHom.coe_coe])
238 (by
239 intro y
240 refine Quotient.inductionOn' y ?_
241 intro b
242 change
243 map e.toContinuousMonoidHom
244 (map e.symm.toContinuousMonoidHom
245 (mk H b)) =
246 mk H b
248 simp only [ContinuousMonoidHom.coe_toMonoidHom, ContinuousMulEquiv.toContinuousMonoidHom_apply,
249 ContinuousMulEquiv.apply_symm_apply, MonoidHom.coe_coe])
251/-- The abelianization congruence induced by a continuous equivalence sends representatives to representatives. -/
252@[simp] theorem congr_apply_mk
253 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
254 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
255 (e : G ≃ₜ* H) (x : G) :
256 congr e (mk G x) =
257 mk H (e x) := by
258 rfl
260/-- Surjective homomorphisms induce surjective maps on topological abelianizations. -/
262 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
263 {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
264 (f : G →ₜ* H) (hf : Function.Surjective f) :
265 Function.Surjective (map f) := by
266 intro y
267 refine Quotient.inductionOn' y ?_
268 intro h
269 rcases hf h with ⟨g, rfl⟩
270 exact ⟨QuotientGroup.mk' (Subgroup.closedCommutator G) g, rfl⟩
272/-- In a commutative `T1` topological group, the natural map to the topological abelianization is
273injective. -/
275 {G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
276 Function.Injective (mk G) := by
277 rw [← MonoidHom.ker_eq_bot_iff]
280/-- The canonical continuous equivalence for commutative `T1` groups. -/
282 (G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
283 _root_.TopologicalAbelianization G ≃ₜ* G := by
284 let e : G ≃* _root_.TopologicalAbelianization G :=
285 MulEquiv.ofBijective (mk G)
287 QuotientGroup.mk'_surjective (Subgroup.closedCommutator G)⟩
288 refine
289 { toMulEquiv := e.symm
290 continuous_toFun := ?_
291 continuous_invFun := ?_ }
292 · refine
293 (QuotientGroup.isQuotientMap_mk
294 (Subgroup.closedCommutator G)).continuous_iff.2 ?_
295 change Continuous fun x : G => e.symm (e x)
296 simpa using (continuous_id : Continuous fun x : G => x)
297 · change Continuous fun x : G => mk G x
298 exact QuotientGroup.continuous_mk
300end TopologicalAbelianization
302end ProCGroups.Abelian