ProCGroups/Topologies/TopologicallyCharacteristicSubgroups.lean
1import Mathlib.Topology.Algebra.ContinuousMonoidHom
2import Mathlib.Topology.Algebra.Group.Quotient
3import Mathlib.GroupTheory.Commutator.Basic
4import ProCGroups.Topologies.QuotientMaps
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/Topologies/TopologicallyCharacteristicSubgroups.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 group constructions
17Topological subgroup, quotient, continuous homomorphism, continuous equivalence, conjugation, and full-subgroup-topology lemmas.
18-/
20universe u
22namespace TopologicalGroup
24/-- Identify the image of a subgroup with its `Subgroup.map`. -/
25lemma image_subtype_eq_map
26 {G : Type u} [Group G]
27 {H : Type _} [Group H]
28 (f : G →* H) (K : Subgroup G) :
29 (fun x : G => f x) '' (K : Set G) = ((K.map f : Subgroup H) : Set H) := by
30 ext y
31 constructor
32 · rintro ⟨x, hx, rfl⟩
33 exact ⟨x, hx, rfl⟩
34 · rintro ⟨x, hx, rfl⟩
35 exact ⟨x, hx, rfl⟩
37/-- Mapping a subgroup by the inverse of an automorphism agrees with comapping along the
38automorphism itself. -/
40 {G : Type u} [Group G] (K : Subgroup G) (e : G ≃* G) :
41 K.map e.symm.toMonoidHom = K.comap e.toMonoidHom := by
42 ext x
43 constructor
44 · rintro ⟨y, hy, rfl⟩
45 change e (e.symm y) ∈ K
46 simpa using hy
47 · intro hx
48 have hx' : e x ∈ K := by
49 simpa [Subgroup.mem_comap] using hx
50 exact ⟨e x, hx', by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulEquiv.symm_apply_apply]⟩
52end TopologicalGroup
54namespace Subgroup
56variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
57variable {H K : Subgroup G}
59/-- Continuous maps send the topological closure of a subgroup into a closed subgroup whenever
60they send the subgroup itself into that closed subgroup. -/
62 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
63 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
64 {A : Subgroup G} {B : Subgroup H} {f : G →* H}
65 (hf : Continuous f) (hAB : A.map f ≤ B) (hB : IsClosed (B : Set H)) :
66 A.topologicalClosure.map f ≤ B := by
67 have hMapsTo : Set.MapsTo (fun x : G => f x) (A : Set G) (B : Set H) := by
68 intro x hx
69 exact hAB ⟨x, hx, rfl⟩
70 have hMapsTo_cl :
71 Set.MapsTo (fun x : G => f x) (_root_.closure (A : Set G)) (B : Set H) :=
72 Set.MapsTo.closure_left hMapsTo hf hB
73 rintro y ⟨x, hx, rfl⟩
74 exact hMapsTo_cl hx
76/-- Homeomorphic group equivalences commute with topological closure of subgroups. -/
78 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
79 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
80 (e : G ≃ₜ* H) (A : Subgroup G) :
81 A.topologicalClosure.map e.toMulEquiv.toMonoidHom =
82 (A.map e.toMulEquiv.toMonoidHom).topologicalClosure := by
83 apply SetLike.coe_injective
84 calc
85 ((A.topologicalClosure.map e.toMulEquiv.toMonoidHom : Subgroup H) : Set H) =
86 e.toHomeomorph '' ((A.topologicalClosure : Subgroup G) : Set G) := by
87 symm
89 (f := e.toMulEquiv.toMonoidHom) (K := A.topologicalClosure)
90 _ = e.toHomeomorph '' (_root_.closure ((A : Subgroup G) : Set G)) := by
91 rw [show ((A.topologicalClosure : Subgroup G) : Set G) =
92 _root_.closure ((A : Set G)) by
93 exact topologicalClosure_coe]
94 _ = _root_.closure (e.toHomeomorph '' ((A : Subgroup G) : Set G)) := by
95 exact e.toHomeomorph.image_closure ((A : Subgroup G) : Set G)
96 _ = _root_.closure (((A.map e.toMulEquiv.toMonoidHom : Subgroup H) : Set H)) := by
97 exact congrArg _root_.closure
99 (f := e.toMulEquiv.toMonoidHom) (K := A))
100 _ = (((A.map e.toMulEquiv.toMonoidHom).topologicalClosure : Subgroup H) : Set H) := by
101 symm
102 exact topologicalClosure_coe
104/-- The closed commutator subgroup of a topological group. -/
105abbrev closedCommutator (G : Type*) [TopologicalSpace G] [Group G]
106 [IsTopologicalGroup G] : Subgroup G :=
107 (_root_.commutator G).topologicalClosure
109@[simp] theorem isClosed_closedCommutator
110 (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
111 IsClosed (closedCommutator G : Set G) :=
112 isClosed_topologicalClosure (s := _root_.commutator G)
115 (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
116 _root_.commutator G ≤ closedCommutator G :=
117 le_topologicalClosure (_root_.commutator G)
119@[simp] theorem topologicalClosure_eq_self_of_discrete
120 (H : Subgroup G) [DiscreteTopology G] :
121 H.topologicalClosure = H := by
122 apply SetLike.coe_injective
123 rw [topologicalClosure_coe, closure_discrete]
125@[simp] theorem closedCommutator_eq_commutator_of_discrete
126 (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
127 [DiscreteTopology G] :
128 closedCommutator G = _root_.commutator G := by
129 simp only [closedCommutator, topologicalClosure_eq_self_of_discrete]
131/-- Continuous homomorphisms send closed commutator subgroups into closed commutator subgroups. -/
132theorem closedCommutator_map_le
133 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
134 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
135 (f : G →ₜ* H) :
136 (closedCommutator G).map f.toMonoidHom ≤ closedCommutator H := by
137 have hcomm : (_root_.commutator G).map f.toMonoidHom ≤ closedCommutator H := by
138 have hmap : (_root_.commutator G).map f.toMonoidHom ≤ _root_.commutator H := by
139 rw [_root_.map_commutator_eq]
140 exact Subgroup.commutator_mono le_top le_top
141 exact hmap.trans (commutator_le_closedCommutator H)
143 (f := f.toMonoidHom) f.continuous_toFun hcomm (isClosed_closedCommutator H)
145/-- Continuous group equivalences map the closed commutator subgroup onto the closed commutator
146subgroup. -/
148 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
149 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
150 (e : G ≃ₜ* H) :
151 (closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator H := by
152 apply le_antisymm
153 · exact closedCommutator_map_le
154 { toMonoidHom := e.toMulEquiv.toMonoidHom
155 continuous_toFun := e.continuous_toFun }
156 · intro y hy
157 have hy' :
158 e.symm y ∈
159 (closedCommutator H).map e.symm.toMulEquiv.toMonoidHom := ⟨y, hy, rfl⟩
160 exact
161 ⟨e.symm y,
163 { toMonoidHom := e.symm.toMulEquiv.toMonoidHom
164 continuous_toFun := e.symm.continuous_toFun } hy',
165 e.apply_symm_apply y⟩
167/-- The closed commutator subgroup is invariant under continuous automorphisms. -/
169 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
170 ∀ e : G ≃ₜ* G,
171 (closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator G :=
172 fun e => closedCommutator_map_eq_of_equiv e
174/-- A subgroup is topologically characteristic if every continuous automorphism preserves it. -/
175structure TopologicallyCharacteristic
176 (H : Subgroup G) : Prop where
177 comap_eq : ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = H
179attribute [class] TopologicallyCharacteristic
181/-- Every abstractly characteristic subgroup is invariant under continuous automorphisms. -/
183 [H.Characteristic] :
184 H.TopologicallyCharacteristic := by
185 refine ⟨?_⟩
186 intro e
187 simpa using
188 (Subgroup.characteristic_iff_comap_eq.mp (show H.Characteristic by infer_instance)
189 e.toMulEquiv)
191omit [IsTopologicalGroup G] in
192/-- A subgroup is topologically characteristic exactly when it is fixed by comap along every continuous automorphism. -/
194 H.TopologicallyCharacteristic ↔
195 ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = H :=
196 ⟨TopologicallyCharacteristic.comap_eq, TopologicallyCharacteristic.mk⟩
198omit [IsTopologicalGroup G] in
199/-- A subgroup is topologically characteristic exactly when every automorphism comap is contained in it. -/
201 H.TopologicallyCharacteristic ↔
202 ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom ≤ H :=
203 topologicallyCharacteristic_iff_comap_eq.trans
204 ⟨fun h e => le_of_eq (h e), fun h e =>
205 le_antisymm (h e) fun g hg =>
206 h e.symm ((congrArg (fun x => x ∈ H) (e.symm_apply_apply g)).mpr hg)⟩
208omit [IsTopologicalGroup G] in
209/-- A subgroup is topologically characteristic exactly when it is contained in every automorphism comap. -/
211 H.TopologicallyCharacteristic ↔
212 ∀ e : G ≃ₜ* G, H ≤ H.comap e.toMulEquiv.toMonoidHom :=
213 topologicallyCharacteristic_iff_comap_eq.trans
214 ⟨fun h e => ge_of_eq (h e), fun h e =>
215 le_antisymm
216 (fun g hg =>
217 (congrArg (fun x => x ∈ H) (e.symm_apply_apply g)).mp (h e.symm hg))
218 (h e)⟩
220omit [IsTopologicalGroup G] in
221/-- A subgroup is topologically characteristic exactly when it is fixed by map along every continuous automorphism. -/
223 H.TopologicallyCharacteristic ↔
224 ∀ e : G ≃ₜ* G, H.map e.toMulEquiv.toMonoidHom = H := by
225 simp_rw [map_equiv_eq_comap_symm']
226 exact topologicallyCharacteristic_iff_comap_eq.trans
227 ⟨fun h e => h e.symm, fun h e => h e.symm⟩
229/-- The closed commutator subgroup is topologically characteristic. -/
230theorem closedCommutator_topologicallyCharacteristic
231 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
232 (closedCommutator G).TopologicallyCharacteristic := by
236omit [IsTopologicalGroup G] in
237/-- A subgroup is topologically characteristic exactly when it is contained in every automorphism image. -/
239 H.TopologicallyCharacteristic ↔
240 ∀ e : G ≃ₜ* G, H ≤ H.map e.toMulEquiv.toMonoidHom := by
241 simp_rw [map_equiv_eq_comap_symm']
242 exact topologicallyCharacteristic_iff_le_comap.trans
243 ⟨fun h e => h e.symm, fun h e => h e.symm⟩
245namespace TopologicallyCharacteristic
247omit [IsTopologicalGroup G] in
248/-- Continuous automorphisms preserve topologically characteristic subgroups. -/
250 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
251 H.map (e.toMulEquiv.toMonoidHom) = H := by
252 calc
253 H.map (e.toMulEquiv.toMonoidHom)
254 = H.comap (e.symm.toMulEquiv.toMonoidHom) := by
255 simpa using
256 TopologicalGroup.map_symm_toMonoidHom_eq_comap (K := H) (e := e.symm.toMulEquiv)
257 _ = H := hH.comap_eq e.symm
259omit [IsTopologicalGroup G] in
260/-- Membership in a topologically characteristic subgroup is invariant under every continuous
261automorphism. -/
262lemma apply_mem_iff
263 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) {g : G} :
264 e g ∈ H ↔ g ∈ H := by
265 change g ∈ H.comap e.toMulEquiv.toMonoidHom ↔ g ∈ H
266 rw [hH.comap_eq e]
268omit [IsTopologicalGroup G] in
269/-- Intersections of topologically characteristic subgroups are topologically characteristic. -/
270theorem inf
271 (hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
272 (H ⊓ K).TopologicallyCharacteristic := by
274 intro e
275 calc
276 (H ⊓ K).comap e.toMulEquiv.toMonoidHom =
277 H.comap e.toMulEquiv.toMonoidHom ⊓ K.comap e.toMulEquiv.toMonoidHom := by
278 simpa using Subgroup.comap_inf H K e.toMulEquiv.toMonoidHom
279 _ = H ⊓ K := by rw [hH.comap_eq e, hK.comap_eq e]
281omit [IsTopologicalGroup G] in
282/-- Supremums of topologically characteristic subgroups are topologically characteristic. -/
284 (hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
285 (H ⊔ K).TopologicallyCharacteristic := by
287 intro e
288 calc
289 (H ⊔ K).map e.toMulEquiv.toMonoidHom = H.map e.toMulEquiv.toMonoidHom ⊔
290 K.map e.toMulEquiv.toMonoidHom := by
291 simpa using Subgroup.map_sup H K e.toMulEquiv.toMonoidHom
294omit [IsTopologicalGroup G] in
295/-- Arbitrary intersections of topologically characteristic subgroups are topologically
296characteristic. -/
297theorem sInf
298 {S : Set (Subgroup G)}
299 (hS : ∀ L ∈ S, L.TopologicallyCharacteristic) :
300 (sInf S).TopologicallyCharacteristic := by
302 intro e
303 ext g
304 rw [Subgroup.mem_comap, Subgroup.mem_sInf, Subgroup.mem_sInf]
305 constructor
306 · intro hg L hL
307 exact (apply_mem_iff (hS L hL) e (g := g)).1 (hg L hL)
308 · intro hg L hL
309 exact (apply_mem_iff (hS L hL) e (g := g)).2 (hg L hL)
311omit [IsTopologicalGroup G] in
312/-- Indexed intersections of topologically characteristic subgroups are topologically
313characteristic. -/
314theorem iInf
315 {ι : Sort*} {S : ι → Subgroup G}
316 (hS : ∀ i, (S i).TopologicallyCharacteristic) :
317 (⨅ i, S i).TopologicallyCharacteristic := by
319 intro e
320 ext g
321 rw [Subgroup.mem_comap, Subgroup.mem_iInf, Subgroup.mem_iInf]
322 constructor
323 · intro hg i
324 exact (apply_mem_iff (hS i) e (g := g)).1 (hg i)
325 · intro hg i
326 exact (apply_mem_iff (hS i) e (g := g)).2 (hg i)
328omit [IsTopologicalGroup G] in
329/-- Indexed supremums of topologically characteristic subgroups are topologically characteristic. -/
331 {ι : Sort*} {S : ι → Subgroup G}
332 (hS : ∀ i, (S i).TopologicallyCharacteristic) :
333 (⨆ i, S i).TopologicallyCharacteristic := by
335 intro e
336 calc
337 (⨆ i, S i).map e.toMulEquiv.toMonoidHom = ⨆ i, (S i).map e.toMulEquiv.toMonoidHom := by
338 simpa using Subgroup.map_iSup e.toMulEquiv.toMonoidHom S
339 _ = ⨆ i, S i := by
342/-- Topological closure preserves topological characteristicity. -/
343theorem topologicalClosure
344 (hH : H.TopologicallyCharacteristic) :
345 H.topologicalClosure.TopologicallyCharacteristic := by
347 intro e
348 apply SetLike.coe_injective
349 calc
350 (((H.topologicalClosure).map e.toMulEquiv.toMonoidHom : Subgroup G) : Set G) =
351 e.toHomeomorph '' ((H.topologicalClosure : Subgroup G) : Set G) := by
352 symm
354 (f := e.toMulEquiv.toMonoidHom) (K := H.topologicalClosure)
355 _ = e.toHomeomorph '' (_root_.closure ((H : Subgroup G) : Set G)) := by
356 rw [show (((H.topologicalClosure : Subgroup G) : Set G)) = _root_.closure ((H : Set G)) by
357 exact Subgroup.topologicalClosure_coe]
358 _ = _root_.closure (e.toHomeomorph '' ((H : Subgroup G) : Set G)) := by
359 exact e.toHomeomorph.image_closure ((H : Subgroup G) : Set G)
360 _ = _root_.closure (((H.map e.toMulEquiv.toMonoidHom : Subgroup G) : Set G)) := by
361 exact congrArg _root_.closure
363 (f := e.toMulEquiv.toMonoidHom) (K := H))
364 _ = _root_.closure ((H : Subgroup G) : Set G) := by
365 simpa using congrArg _root_.closure
367 _ = ((H.topologicalClosure : Subgroup G) : Set G) := by
368 symm
369 exact Subgroup.topologicalClosure_coe
373/-- The bottom subgroup is topologically characteristic. -/
374instance botTopologicallyCharacteristic :
375 (⊥ : Subgroup G).TopologicallyCharacteristic := inferInstance
377/-- The top subgroup is topologically characteristic. -/
378instance topTopologicallyCharacteristic :
379 (⊤ : Subgroup G).TopologicallyCharacteristic := inferInstance
381/-- Commutators of topologically characteristic subgroups are topologically characteristic. -/
383 [H.TopologicallyCharacteristic] [K.TopologicallyCharacteristic] :
384 (⁅H, K⁆).TopologicallyCharacteristic := by
385 refine topologicallyCharacteristic_iff_le_map.mpr ?_
386 intro e
387 have hHle :
388 H ≤ H.map e.toMulEquiv.toMonoidHom :=
389 topologicallyCharacteristic_iff_le_map.mp
390 (show H.TopologicallyCharacteristic by infer_instance) e
391 have hKle :
392 K ≤ K.map e.toMulEquiv.toMonoidHom :=
393 topologicallyCharacteristic_iff_le_map.mp
394 (show K.TopologicallyCharacteristic by infer_instance) e
395 exact Subgroup.commutator_le_map_commutator
396 hHle hKle
398/-- The center is topologically characteristic. -/
399instance centerTopologicallyCharacteristic :
400 (center G).TopologicallyCharacteristic := inferInstance
402/-- The centralizer of a topologically characteristic subgroup is again topologically
403characteristic. -/
405 [hH : H.TopologicallyCharacteristic] :
406 (centralizer (H : Set G)).TopologicallyCharacteristic := by
407 refine topologicallyCharacteristic_iff_comap_le.mpr ?_
408 intro e g hg
409 have hg' : e g ∈ centralizer (H : Set G) := hg
410 rw [Subgroup.mem_centralizer_iff]
411 intro h hh
412 apply e.toMulEquiv.injective
413 rw [e.toMulEquiv.map_mul, e.toMulEquiv.map_mul]
414 exact
415 hg' (e h) ((TopologicallyCharacteristic.apply_mem_iff (hH := inferInstance) e (g := h)).2 hh)
417/-- Topologically characteristic subgroups are normal. -/
419 [H.TopologicallyCharacteristic] :
420 H.Normal := by
421 refine ⟨?_⟩
422 intro x hx g
423 let e : G ≃ₜ* G :=
424 { toMulEquiv := MulAut.conj g
425 continuous_toFun := by
426 dsimp [MulAut.conj_apply]
427 exact IsTopologicalGroup.continuous_conj (G := G) g
428 continuous_invFun := by
429 simpa [MulAut.conj_inv_apply] using
430 (IsTopologicalGroup.continuous_conj (G := G) (g := g⁻¹)) }
431 have hmap : H.map (e.toMulEquiv.toMonoidHom) = H :=
432 TopologicallyCharacteristic.map_eq (hH := inferInstance) e
433 have hxmap : e x ∈ H.map (e.toMulEquiv.toMonoidHom) := ⟨x, hx, rfl⟩
434 rw [hmap] at hxmap
435 simpa [e, MulAut.conj_apply] using hxmap
437namespace TopologicallyCharacteristic
439/-- A continuous automorphism descends to the quotient by a topologically characteristic
440subgroup. -/
441noncomputable def quotientMulEquiv
442 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
443 G ⧸ H ≃* G ⧸ H := by
444 letI : H.Normal := by infer_instance
447/-- The quotient equivalence induced by a topologically characteristic subgroup sends representatives to representatives. -/
448@[simp] theorem quotientMulEquiv_mk
449 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
450 hH.quotientMulEquiv e (QuotientGroup.mk' H g) =
451 QuotientGroup.mk' H (e g) := by
452 rfl
454/-- Topological version of `quotientMulEquiv`. -/
455noncomputable def quotientContinuousMulEquiv
456 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
457 G ⧸ H ≃ₜ* G ⧸ H := by
458 letI : H.Normal := by infer_instance
461/-- The continuous quotient equivalence induced by a topologically characteristic subgroup sends representatives to representatives. -/
462@[simp] theorem quotientContinuousMulEquiv_mk
463 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
464 hH.quotientContinuousMulEquiv e (QuotientGroup.mk' H g) =
465 QuotientGroup.mk' H (e g) := by
466 rfl
470end Subgroup