Source: ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
1import Mathlib.Topology.Algebra.ContinuousMonoidHom
2import Mathlib.Topology.Algebra.Group.Quotient
3import Mathlib.GroupTheory.Commutator.Basic
4import ProCGroups.Topologies.QuotientMaps
6/-!
7# Topologically characteristic subgroups
9This file studies subgroups invariant under continuous automorphisms. It proves invariance of the
10closed commutator subgroup, gives equivalent map and comap formulations, and establishes closure
11of topologically characteristic subgroups under lattice operations and topological closure.
12-/
14universe u
16namespace TopologicalGroup
18/-- Identify the image of a subgroup with its Subgroup.map. -/
19lemma image_subtype_eq_map
20 {G : Type u} [Group G]
21 {H : Type _} [Group H]
22 (f : G →* H) (K : Subgroup G) :
23 (fun x : G => f x) '' (K : Set G) = ((K.map f : Subgroup H) : Set H) := by
24 ext y
25 constructor
26 · rintro ⟨x, hx, rfl⟩
27 exact ⟨x, hx, rfl⟩
28 · rintro ⟨x, hx, rfl⟩
29 exact ⟨x, hx, rfl⟩
31/--
32Mapping a subgroup by the inverse of an automorphism agrees with comapping along the
33automorphism itself.
34-/
35lemma map_symm_toMonoidHom_eq_comap
36 {G : Type u} [Group G] (K : Subgroup G) (e : G ≃* G) :
37 K.map e.symm.toMonoidHom = K.comap e.toMonoidHom := by
38 ext x
39 constructor
40 · rintro ⟨y, hy, rfl⟩
41 change e (e.symm y) ∈ K
42 simpa using hy
43 · intro hx
44 have hx' : e x ∈ K := by
45 simpa [Subgroup.mem_comap] using hx
46 exact ⟨e x, hx', by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe,
47 MulEquiv.symm_apply_apply]⟩
49end TopologicalGroup
51namespace Subgroup
53variable {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
54variable {H K : Subgroup G}
56/--
57Continuous maps send the topological closure of a subgroup into a closed subgroup whenever they
58send the subgroup itself into that closed subgroup.
59-/
60theorem map_topologicalClosure_le_of_map_le
61 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
62 [TopologicalSpace H] [Group H]
63 {A : Subgroup G} {B : Subgroup H} {f : G →* H}
64 (hf : Continuous f) (hAB : A.map f ≤ B) (hB : IsClosed (B : Set H)) :
65 A.topologicalClosure.map f ≤ B := by
66 have hMapsTo : Set.MapsTo (fun x : G => f x) (A : Set G) (B : Set H) := by
67 intro x hx
68 exact hAB ⟨x, hx, rfl⟩
69 have hMapsTo_cl :
70 Set.MapsTo (fun x : G => f x) (_root_.closure (A : Set G)) (B : Set H) :=
71 Set.MapsTo.closure_left hMapsTo hf hB
72 rintro y ⟨x, hx, rfl⟩
73 exact hMapsTo_cl hx
75/-- Homeomorphic group equivalences commute with topological closure of subgroups. -/
76theorem map_topologicalClosure_eq_of_continuousMulEquiv
77 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
78 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
79 (e : G ≃ₜ* H) (A : Subgroup G) :
80 A.topologicalClosure.map e.toMulEquiv.toMonoidHom =
81 (A.map e.toMulEquiv.toMonoidHom).topologicalClosure := by
82 apply SetLike.coe_injective
83 calc
84 ((A.topologicalClosure.map e.toMulEquiv.toMonoidHom : Subgroup H) : Set H) =
85 e.toHomeomorph '' ((A.topologicalClosure : Subgroup G) : Set G) := by
86 symm
88 (f := e.toMulEquiv.toMonoidHom) (K := A.topologicalClosure)
89 _ = e.toHomeomorph '' (_root_.closure ((A : Subgroup G) : Set G)) := by
90 rw [show ((A.topologicalClosure : Subgroup G) : Set G) =
91 _root_.closure ((A : Set G)) by
92 exact topologicalClosure_coe]
93 _ = _root_.closure (e.toHomeomorph '' ((A : Subgroup G) : Set G)) := by
94 exact e.toHomeomorph.image_closure ((A : Subgroup G) : Set G)
95 _ = _root_.closure (((A.map e.toMulEquiv.toMonoidHom : Subgroup H) : Set H)) := by
96 exact congrArg _root_.closure
98 (f := e.toMulEquiv.toMonoidHom) (K := A))
99 _ = (((A.map e.toMulEquiv.toMonoidHom).topologicalClosure : Subgroup H) : Set H) := by
100 symm
101 exact topologicalClosure_coe
103/-- The closed commutator subgroup of a topological group. -/
104abbrev closedCommutator (G : Type*) [TopologicalSpace G] [Group G]
105 [IsTopologicalGroup G] : Subgroup G :=
106 (_root_.commutator G).topologicalClosure
108/-- The closed commutator subgroup is closed. -/
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)
114/-- The abstract commutator subgroup is contained in the closed commutator subgroup. -/
115theorem commutator_le_closedCommutator
116 (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
117 _root_.commutator G ≤ closedCommutator G :=
118 le_topologicalClosure (_root_.commutator G)
120/--
121In a discrete topological group, the topological closure of a subgroup is the subgroup itself.
122-/
123@[simp] theorem topologicalClosure_eq_self_of_discrete
124 (H : Subgroup G) [DiscreteTopology G] :
125 H.topologicalClosure = H := by
126 apply SetLike.coe_injective
127 rw [topologicalClosure_coe, closure_discrete]
129/--
130For a discrete group, the closed commutator subgroup agrees with the ordinary commutator
131subgroup.
132-/
133@[simp] theorem closedCommutator_eq_commutator_of_discrete
134 (G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
135 [DiscreteTopology G] :
136 closedCommutator G = _root_.commutator G := by
137 simp only [closedCommutator, topologicalClosure_eq_self_of_discrete]
139/-- Continuous homomorphisms send closed commutator subgroups into closed commutator subgroups. -/
140theorem closedCommutator_map_le
141 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
142 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
143 (f : G →ₜ* H) :
144 (closedCommutator G).map f.toMonoidHom ≤ closedCommutator H := by
145 have hcomm : (_root_.commutator G).map f.toMonoidHom ≤ closedCommutator H := by
146 have hmap : (_root_.commutator G).map f.toMonoidHom ≤ _root_.commutator H := by
147 rw [_root_.map_commutator_eq]
148 exact Subgroup.commutator_mono le_top le_top
149 exact hmap.trans (commutator_le_closedCommutator H)
150 exact map_topologicalClosure_le_of_map_le
151 (f := f.toMonoidHom) f.continuous_toFun hcomm (isClosed_closedCommutator H)
153/--
154Continuous group equivalences map the closed commutator subgroup onto the closed commutator
155subgroup.
156-/
157theorem closedCommutator_map_eq_of_equiv
158 {G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
159 [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
160 (e : G ≃ₜ* H) :
161 (closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator H := by
162 apply le_antisymm
163 · exact closedCommutator_map_le
164 { toMonoidHom := e.toMulEquiv.toMonoidHom
165 continuous_toFun := e.continuous_toFun }
166 · intro y hy
167 have hy' :
168 e.symm y ∈
169 (closedCommutator H).map e.symm.toMulEquiv.toMonoidHom := ⟨y, hy, rfl⟩
170 exact
171 ⟨e.symm y,
172 closedCommutator_map_le
173 { toMonoidHom := e.symm.toMulEquiv.toMonoidHom
174 continuous_toFun := e.symm.continuous_toFun } hy',
175 e.apply_symm_apply y⟩
177/-- The closed commutator subgroup is invariant under continuous automorphisms. -/
178theorem closedCommutator_characteristic
179 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
180 ∀ e : G ≃ₜ* G,
181 (closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator G :=
182 fun e => closedCommutator_map_eq_of_equiv e
184/-- A subgroup is topologically characteristic if every continuous automorphism preserves it. -/
185structure TopologicallyCharacteristic
186 (H : Subgroup G) : Prop where
187 /-- Pulling back \(H\) along any continuous automorphism of \(G\) leaves \(H\) unchanged. -/
188 comap_eq : ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = H
190attribute [class] TopologicallyCharacteristic
192/-- Every abstractly characteristic subgroup is invariant under continuous automorphisms. -/
193instance topologicallyCharacteristic_of_characteristic
194 [H.Characteristic] :
195 H.TopologicallyCharacteristic := by
196 refine ⟨?_⟩
197 intro e
198 simpa using
199 (Subgroup.characteristic_iff_comap_eq.mp (show H.Characteristic by infer_instance)
200 e.toMulEquiv)
202omit [IsTopologicalGroup G] in
203/--
204Topological characteristicity is equivalent to invariance under comap by every continuous
205automorphism.
206-/
207theorem topologicallyCharacteristic_iff_comap_eq :
208 H.TopologicallyCharacteristic ↔
209 ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = H :=
210 ⟨TopologicallyCharacteristic.comap_eq, TopologicallyCharacteristic.mk⟩
212omit [IsTopologicalGroup G] in
213/--
214A subgroup is topologically characteristic exactly when every automorphism comap is contained in
215it.
216-/
217theorem topologicallyCharacteristic_iff_comap_le :
218 H.TopologicallyCharacteristic ↔
219 ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom ≤ H :=
220 topologicallyCharacteristic_iff_comap_eq.trans
221 ⟨fun h e => le_of_eq (h e), fun h e =>
222 le_antisymm (h e) fun g hg =>
223 h e.symm ((congrArg (fun x => x ∈ H) (e.symm_apply_apply g)).mpr hg)⟩
225omit [IsTopologicalGroup G] in
226/--
227A subgroup is topologically characteristic exactly when it is contained in every automorphism
228comap.
229-/
230theorem topologicallyCharacteristic_iff_le_comap :
231 H.TopologicallyCharacteristic ↔
232 ∀ e : G ≃ₜ* G, H ≤ H.comap e.toMulEquiv.toMonoidHom :=
233 topologicallyCharacteristic_iff_comap_eq.trans
234 ⟨fun h e => ge_of_eq (h e), fun h e =>
235 le_antisymm
236 (fun g hg =>
237 (congrArg (fun x => x ∈ H) (e.symm_apply_apply g)).mp (h e.symm hg))
238 (h e)⟩
240omit [IsTopologicalGroup G] in
241/--
242Topological characteristicity is equivalent to invariance under image by every continuous
243automorphism.
244-/
245theorem topologicallyCharacteristic_iff_map_eq :
246 H.TopologicallyCharacteristic ↔
247 ∀ e : G ≃ₜ* G, H.map e.toMulEquiv.toMonoidHom = H := by
248 simp_rw [map_equiv_eq_comap_symm']
249 exact topologicallyCharacteristic_iff_comap_eq.trans
250 ⟨fun h e => h e.symm, fun h e => h e.symm⟩
252/-- The closed commutator subgroup is topologically characteristic. -/
253theorem closedCommutator_topologicallyCharacteristic
254 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
255 (closedCommutator G).TopologicallyCharacteristic := by
256 rw [topologicallyCharacteristic_iff_map_eq]
257 exact closedCommutator_characteristic
259omit [IsTopologicalGroup G] in
260/--
261A subgroup is topologically characteristic exactly when it is contained in every automorphism
262image.
263-/
264theorem topologicallyCharacteristic_iff_le_map :
265 H.TopologicallyCharacteristic ↔
266 ∀ e : G ≃ₜ* G, H ≤ H.map e.toMulEquiv.toMonoidHom := by
267 simp_rw [map_equiv_eq_comap_symm']
268 exact topologicallyCharacteristic_iff_le_comap.trans
269 ⟨fun h e => h e.symm, fun h e => h e.symm⟩
271namespace TopologicallyCharacteristic
273omit [IsTopologicalGroup G] in
274/--
275A topologically characteristic subgroup is fixed by the image of every continuous automorphism.
276-/
277lemma map_eq
278 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
279 H.map (e.toMulEquiv.toMonoidHom) = H := by
280 calc
281 H.map (e.toMulEquiv.toMonoidHom)
282 = H.comap (e.symm.toMulEquiv.toMonoidHom) := by
283 ext x
284 constructor
285 · rintro ⟨y, hy, rfl⟩
286 change e.symm (e y) ∈ H
287 simpa using hy
288 · intro hx
289 change e.symm x ∈ H at hx
290 exact ⟨e.symm x, hx, e.apply_symm_apply x⟩
291 _ = H := hH.comap_eq e.symm
293omit [IsTopologicalGroup G] in
294/--
295Membership in a topologically characteristic subgroup is invariant under applying a continuous
296automorphism.
297-/
298lemma apply_mem_iff
299 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) {g : G} :
300 e g ∈ H ↔ g ∈ H := by
301 change g ∈ H.comap e.toMulEquiv.toMonoidHom ↔ g ∈ H
302 rw [hH.comap_eq e]
304omit [IsTopologicalGroup G] in
305/-- Intersections of topologically characteristic subgroups are topologically characteristic. -/
306theorem inf
307 (hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
308 (H ⊓ K).TopologicallyCharacteristic := by
309 rw [topologicallyCharacteristic_iff_comap_eq]
310 intro e
311 calc
312 (H ⊓ K).comap e.toMulEquiv.toMonoidHom =
313 H.comap e.toMulEquiv.toMonoidHom ⊓ K.comap e.toMulEquiv.toMonoidHom := by
314 simpa using Subgroup.comap_inf H K e.toMulEquiv.toMonoidHom
315 _ = H ⊓ K := by rw [hH.comap_eq e, hK.comap_eq e]
317omit [IsTopologicalGroup G] in
318/-- Supremums of topologically characteristic subgroups are topologically characteristic. -/
319theorem sup
320 (hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
321 (H ⊔ K).TopologicallyCharacteristic := by
322 rw [topologicallyCharacteristic_iff_map_eq]
323 intro e
324 calc
325 (H ⊔ K).map e.toMulEquiv.toMonoidHom = H.map e.toMulEquiv.toMonoidHom ⊔
326 K.map e.toMulEquiv.toMonoidHom := by
327 simpa using Subgroup.map_sup H K e.toMulEquiv.toMonoidHom
328 _ = H ⊔ K := by rw [map_eq hH e, map_eq hK e]
330omit [IsTopologicalGroup G] in
331/--
332Arbitrary intersections of topologically characteristic subgroups are topologically
333characteristic.
334-/
335theorem sInf
336 {S : Set (Subgroup G)}
337 (hS : ∀ L ∈ S, L.TopologicallyCharacteristic) :
338 (sInf S).TopologicallyCharacteristic := by
339 rw [topologicallyCharacteristic_iff_comap_eq]
340 intro e
341 ext g
342 rw [Subgroup.mem_comap, Subgroup.mem_sInf, Subgroup.mem_sInf]
343 constructor
344 · intro hg L hL
345 exact (apply_mem_iff (hS L hL) e (g := g)).1 (hg L hL)
346 · intro hg L hL
347 exact (apply_mem_iff (hS L hL) e (g := g)).2 (hg L hL)
349omit [IsTopologicalGroup G] in
350/--
351Indexed intersections of topologically characteristic subgroups are topologically
352characteristic.
353-/
354theorem iInf
355 {ι : Sort*} {S : ι → Subgroup G}
356 (hS : ∀ i, (S i).TopologicallyCharacteristic) :
357 (⨅ i, S i).TopologicallyCharacteristic := by
358 rw [topologicallyCharacteristic_iff_comap_eq]
359 intro e
360 ext g
361 rw [Subgroup.mem_comap, Subgroup.mem_iInf, Subgroup.mem_iInf]
362 constructor
363 · intro hg i
364 exact (apply_mem_iff (hS i) e (g := g)).1 (hg i)
365 · intro hg i
366 exact (apply_mem_iff (hS i) e (g := g)).2 (hg i)
368omit [IsTopologicalGroup G] in
369/-- Indexed supremums of topologically characteristic subgroups are topologically characteristic. -/
370theorem iSup
371 {ι : Sort*} {S : ι → Subgroup G}
372 (hS : ∀ i, (S i).TopologicallyCharacteristic) :
373 (⨆ i, S i).TopologicallyCharacteristic := by
374 rw [topologicallyCharacteristic_iff_map_eq]
375 intro e
376 calc
377 (⨆ i, S i).map e.toMulEquiv.toMonoidHom = ⨆ i, (S i).map e.toMulEquiv.toMonoidHom := by
378 simpa using Subgroup.map_iSup e.toMulEquiv.toMonoidHom S
379 _ = ⨆ i, S i := by
380 simpa using iSup_congr (fun i => map_eq (hS i) e)
382/--
383The topological closure of a topologically characteristic subgroup is topologically
384characteristic.
385-/
386theorem topologicalClosure
387 (hH : H.TopologicallyCharacteristic) :
388 H.topologicalClosure.TopologicallyCharacteristic := by
389 rw [topologicallyCharacteristic_iff_map_eq]
390 intro e
391 apply SetLike.coe_injective
392 calc
393 (((H.topologicalClosure).map e.toMulEquiv.toMonoidHom : Subgroup G) : Set G) =
394 e.toHomeomorph '' ((H.topologicalClosure : Subgroup G) : Set G) := by
395 symm
397 (f := e.toMulEquiv.toMonoidHom) (K := H.topologicalClosure)
398 _ = e.toHomeomorph '' (_root_.closure ((H : Subgroup G) : Set G)) := by
399 rw [show (((H.topologicalClosure : Subgroup G) : Set G)) = _root_.closure ((H : Set G)) by
400 exact Subgroup.topologicalClosure_coe]
401 _ = _root_.closure (e.toHomeomorph '' ((H : Subgroup G) : Set G)) := by
402 exact e.toHomeomorph.image_closure ((H : Subgroup G) : Set G)
403 _ = _root_.closure (((H.map e.toMulEquiv.toMonoidHom : Subgroup G) : Set G)) := by
404 exact congrArg _root_.closure
406 (f := e.toMulEquiv.toMonoidHom) (K := H))
407 _ = _root_.closure ((H : Subgroup G) : Set G) := by
408 simpa using congrArg _root_.closure
409 (congrArg (fun L : Subgroup G => (L : Set G)) (map_eq hH e))
410 _ = ((H.topologicalClosure : Subgroup G) : Set G) := by
411 symm
412 exact Subgroup.topologicalClosure_coe
414end TopologicallyCharacteristic
416/-- The bottom subgroup is topologically characteristic. -/
417instance botTopologicallyCharacteristic :
418 (⊥ : Subgroup G).TopologicallyCharacteristic := inferInstance
420/-- The top subgroup is topologically characteristic. -/
421instance topTopologicallyCharacteristic :
422 (⊤ : Subgroup G).TopologicallyCharacteristic := inferInstance
424/-- Commutators of topologically characteristic subgroups are topologically characteristic. -/
425instance commutatorTopologicallyCharacteristic
426 [H.TopologicallyCharacteristic] [K.TopologicallyCharacteristic] :
427 (⁅H, K⁆).TopologicallyCharacteristic := by
428 refine topologicallyCharacteristic_iff_le_map.mpr ?_
429 intro e
430 have hHle :
431 H ≤ H.map e.toMulEquiv.toMonoidHom :=
432 topologicallyCharacteristic_iff_le_map.mp
433 (show H.TopologicallyCharacteristic by infer_instance) e
434 have hKle :
435 K ≤ K.map e.toMulEquiv.toMonoidHom :=
436 topologicallyCharacteristic_iff_le_map.mp
437 (show K.TopologicallyCharacteristic by infer_instance) e
438 exact Subgroup.commutator_le_map_commutator
439 hHle hKle
441/-- The center is topologically characteristic. -/
442instance centerTopologicallyCharacteristic :
443 (center G).TopologicallyCharacteristic := inferInstance
445/--
446The centralizer of a topologically characteristic subgroup is again topologically
447characteristic.
448-/
449instance topologicallyCharacteristic_centralizerInst
450 [hH : H.TopologicallyCharacteristic] :
451 (centralizer (H : Set G)).TopologicallyCharacteristic := by
452 refine topologicallyCharacteristic_iff_comap_le.mpr ?_
453 intro e g hg
454 have hg' : e g ∈ centralizer (H : Set G) := hg
455 rw [Subgroup.mem_centralizer_iff]
456 intro h hh
457 apply e.toMulEquiv.injective
458 rw [e.toMulEquiv.map_mul, e.toMulEquiv.map_mul]
459 exact
460 hg' (e h) ((TopologicallyCharacteristic.apply_mem_iff (hH := inferInstance) e (g := h)).2 hh)
462/-- Topologically characteristic subgroups are normal. -/
463instance topologicallyCharacteristic_normalInst
464 [H.TopologicallyCharacteristic] :
465 H.Normal := by
466 refine ⟨?_⟩
467 intro x hx g
468 let e : G ≃ₜ* G :=
469 { toMulEquiv := MulAut.conj g
470 continuous_toFun := by
471 dsimp [MulAut.conj_apply]
472 exact IsTopologicalGroup.continuous_conj (G := G) g
473 continuous_invFun := by
474 change Continuous fun h : G => g⁻¹ * h * g
475 simpa only [inv_inv] using
476 (IsTopologicalGroup.continuous_conj (G := G) (g := g⁻¹)) }
477 have hmap : H.map (e.toMulEquiv.toMonoidHom) = H :=
478 TopologicallyCharacteristic.map_eq (hH := inferInstance) e
479 have hxmap : e x ∈ H.map (e.toMulEquiv.toMonoidHom) := ⟨x, hx, rfl⟩
480 rw [hmap] at hxmap
481 simpa [e, MulAut.conj_apply] using hxmap
483namespace TopologicallyCharacteristic
485/--
486A continuous automorphism descends to the quotient by a topologically characteristic subgroup.
487-/
488noncomputable def quotientMulEquiv
489 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
490 G ⧸ H ≃* G ⧸ H := by
491 letI : H.Normal := by infer_instance
492 exact QuotientGroup.congr H H e.toMulEquiv (map_eq hH e)
494/--
495The quotient equivalence induced by a topologically characteristic subgroup sends
496representatives to representatives.
497-/
498@[simp] theorem quotientMulEquiv_mk
499 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
500 hH.quotientMulEquiv e (QuotientGroup.mk' H g) =
501 QuotientGroup.mk' H (e g) := by
502 rfl
504/--
505A topologically characteristic subgroup induces the corresponding continuous multiplicative
506equivalence on quotients.
507-/
508noncomputable def quotientContinuousMulEquiv
509 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
510 G ⧸ H ≃ₜ* G ⧸ H := by
511 letI : H.Normal := by infer_instance
512 exact ProCGroups.QuotientGroup.congrₜ H H e (map_eq hH e)
514/--
515The continuous quotient equivalence induced by a topologically characteristic subgroup sends
516representatives to representatives.
517-/
518@[simp] theorem quotientContinuousMulEquiv_mk
519 (hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
520 hH.quotientContinuousMulEquiv e (QuotientGroup.mk' H g) =
521 QuotientGroup.mk' H (e g) := by
522 rfl
524end TopologicallyCharacteristic
526end Subgroup