ProCGroups/Abelian/TopologicalAbelianizationFunctoriality.lean
1import ProCGroups.Topologies.OpenSubgroup
2import ProCGroups.Topologies.Conjugation
3import ProCGroups.TopologicalGroups
4import ProCGroups.Abelian.TopologicalAbelianization
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/Abelian/TopologicalAbelianizationFunctoriality.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Functoriality of topological abelianization
17Develops the functorial and categorical universal property of topological abelianization, together with the conjugation action on the abelianization of an open normal subgroup.
18-/
20open CategoryTheory
21open scoped Topology
23namespace ProCGroups.Abelian
25universe u
27/-- Bundled commutative `T1` topological groups with continuous homomorphisms. -/
28@[pp_with_univ]
29structure T1CommTopGrp where
30 carrier : Type u
31 [commGroup : CommGroup carrier]
32 [topologicalSpace : TopologicalSpace carrier]
33 [isTopologicalGroup : IsTopologicalGroup carrier]
34 [t1Space : T1Space carrier]
36attribute [instance] T1CommTopGrp.commGroup T1CommTopGrp.topologicalSpace
37 T1CommTopGrp.isTopologicalGroup T1CommTopGrp.t1Space
39namespace T1CommTopGrp
41instance instCoeSort : CoeSort T1CommTopGrp (Type u) where
42 coe G := G.carrier
44/-- Bundle an unbundled commutative `T1` topological group. -/
45abbrev of (G : Type u) [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G]
46 [T1Space G] : T1CommTopGrp where
47 carrier := G
49/-- Morphisms of commutative `T1` topological groups are continuous homomorphisms. -/
50@[ext]
51structure Hom (G H : T1CommTopGrp.{u}) where
52 hom' : G →ₜ* H
54instance instCategory : Category T1CommTopGrp where
55 Hom G H := Hom G H
56 id G := ⟨ContinuousMonoidHom.id G⟩
57 comp f g := ⟨g.hom'.comp f.hom'⟩
59instance instConcreteCategory : ConcreteCategory T1CommTopGrp (fun G H => G →ₜ* H) where
60 hom f := f.hom'
61 ofHom f := ⟨f⟩
63/-- The underlying continuous homomorphism of a morphism. -/
64abbrev Hom.hom {G H : T1CommTopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
65 ConcreteCategory.hom (C := T1CommTopGrp) f
67instance instCoeFunHom {G H : T1CommTopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
68 coe f := f.hom
70@[simp] theorem hom_id {G : T1CommTopGrp.{u}} :
71 (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G :=
72 rfl
74@[simp] theorem hom_comp {G H K : T1CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
75 (f ≫ g).hom = g.hom.comp f.hom :=
76 rfl
78@[simp] theorem comp_apply {G H K : T1CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
79 (f ≫ g) x = g (f x) :=
80 rfl
82/-- Morphisms of commutative `T1` topological groups are extensional in their underlying continuous
83homomorphism. -/
84@[ext] theorem hom_ext {G H : T1CommTopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
85 f = g :=
86 Hom.ext h
88/-- Typecheck a continuous homomorphism as a bundled commutative `T1` topological-group morphism. -/
89abbrev ofHom {G H : Type u}
90 [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T1Space G]
91 [CommGroup H] [TopologicalSpace H] [IsTopologicalGroup H] [T1Space H]
92 (f : G →ₜ* H) : of G ⟶ of H :=
93 ConcreteCategory.ofHom f
95end T1CommTopGrp
97/-- Forget the `T1` and commutativity structure of a bundled commutative `T1` topological group. -/
98def t1CommTopGrpForgetToTopGrp : T1CommTopGrp.{u} ⥤ TopGrp.{u} where
100 map f := TopGrp.ofHom f.hom
101 map_id G := by
102 apply TopGrp.hom_ext
103 rfl
104 map_comp f g := by
105 apply TopGrp.hom_ext
106 rfl
108/-- Forget only the `T1` structure of a bundled commutative `T1` topological group. -/
109def t1CommTopGrpForgetToCommTopGrp : T1CommTopGrp.{u} ⥤ CommTopGrp.{u} where
110 obj G := CommTopGrp.of G
111 map f := CommTopGrp.ofHom f.hom
112 map_id G := by
113 apply CommTopGrp.hom_ext
114 rfl
115 map_comp f g := by
116 apply CommTopGrp.hom_ext
117 rfl
119/-- Topological abelianization as a functor from topological groups to commutative topological
120groups. -/
121noncomputable def topologicalAbelianizationFunctor : TopGrp.{u} ⥤ CommTopGrp.{u} where
122 obj G := CommTopGrp.of (TopologicalAbelianization G)
123 map {G H} f := CommTopGrp.ofHom (TopologicalAbelianization.map f.hom)
124 map_id G := by
125 apply CommTopGrp.hom_ext
126 exact TopologicalAbelianization.map_id G
127 map_comp f g := by
128 apply CommTopGrp.hom_ext
129 exact TopologicalAbelianization.map_comp g.hom f.hom
131@[simp] theorem topologicalAbelianizationFunctor_map_apply_mk
132 {G H : TopGrp.{u}} (f : G ⟶ H) (x : G) :
133 topologicalAbelianizationFunctor.map f (TopologicalAbelianization.mk G x) =
134 TopologicalAbelianization.mk H (f x) :=
135 rfl
137/-- Topological abelianization as a functor from topological groups to commutative `T1`
138topological groups. -/
139noncomputable def topologicalAbelianizationT1Functor : TopGrp.{u} ⥤ T1CommTopGrp.{u} where
140 obj G := T1CommTopGrp.of (TopologicalAbelianization G)
141 map {G H} f := T1CommTopGrp.ofHom (TopologicalAbelianization.map f.hom)
142 map_id G := by
143 apply T1CommTopGrp.hom_ext
144 exact TopologicalAbelianization.map_id G
145 map_comp f g := by
146 apply T1CommTopGrp.hom_ext
147 exact TopologicalAbelianization.map_comp g.hom f.hom
149@[simp] theorem topologicalAbelianizationT1Functor_map_apply_mk
150 {G H : TopGrp.{u}} (f : G ⟶ H) (x : G) :
151 topologicalAbelianizationT1Functor.map f (TopologicalAbelianization.mk G x) =
152 TopologicalAbelianization.mk H (f x) :=
153 rfl
155/-- Category-level Hom equivalence expressing the universal property of topological
156abelianization for commutative `T1` targets. -/
157noncomputable def topologicalAbelianizationHomEquiv
158 (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A] :
159 (topologicalAbelianizationFunctor.obj G ⟶ A) ≃
160 (G ⟶ commTopGrpForgetToTopGrp.obj A) where
161 toFun φ := TopGrp.ofHom (φ.hom.comp (TopologicalAbelianization.mkₜ G))
162 invFun f := CommTopGrp.ofHom (TopologicalAbelianization.lift f.hom)
163 left_inv φ := by
164 apply CommTopGrp.hom_ext
165 apply TopologicalAbelianization.hom_ext
166 intro x
167 rfl
168 right_inv f := by
169 apply TopGrp.hom_ext
170 ext x
171 rfl
173@[simp] theorem topologicalAbelianizationHomEquiv_apply_hom
174 (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
175 (φ : topologicalAbelianizationFunctor.obj G ⟶ A) :
176 (topologicalAbelianizationHomEquiv G A φ).hom =
177 φ.hom.comp (TopologicalAbelianization.mkₜ G) :=
178 rfl
180@[simp] theorem topologicalAbelianizationHomEquiv_symm_apply_mk
181 (G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
182 (f : G ⟶ commTopGrpForgetToTopGrp.obj A) (x : G) :
183 (topologicalAbelianizationHomEquiv G A).symm f
184 (TopologicalAbelianization.mk G x) = f x :=
185 rfl
187/-- The topological abelianization of the top open subgroup is canonically the same as the
188topological abelianization of the ambient group. -/
189noncomputable def topologicalAbelianizationTopMulEquiv
190 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
191 TopologicalAbelianization ↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ*
192 TopologicalAbelianization G :=
193 TopologicalAbelianization.congr
194 (G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
195 (H := G)
198/-- The abelianization equivalence for a topological group equivalence sends representatives to representatives. -/
199@[simp] theorem topologicalAbelianizationTopMulEquiv_apply_mk
200 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
201 (x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :
203 (G := G) (TopologicalAbelianization.mk ↥((⊤ : OpenSubgroup G) : Subgroup G) x) =
204 TopologicalAbelianization.mk G x.1 := by
205 simpa [topologicalAbelianizationTopMulEquiv] using
206 (TopologicalAbelianization.congr_apply_mk
209/-- The quotient `G/N` acts on the topological abelianization of `N` by conjugation. -/
210noncomputable def quotientConjugationTopologicalAbelianizationMap
211 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
212 (N : Subgroup G) [N.Normal] :
213 (G ⧸ N) →* MulAut (TopologicalAbelianization N) := by
214 let K : Subgroup N := Subgroup.closedCommutator N
215 have hKchar : K.TopologicallyCharacteristic :=
218 (G := G) N K
219 (fun n x => by
220 have hcomm :
221 ⁅n, x⁆ ∈ Subgroup.closedCommutator N :=
223 (Subgroup.commutator_mem_commutator (Subgroup.mem_top n) (Subgroup.mem_top x))
224 have hconj : (MulAut.conjNormal (n : G)) x = n * x * n⁻¹ := by
225 ext
226 simp only [MulAut.conjNormal_apply, Subgroup.coe_mul, InvMemClass.coe_inv]
227 rw [hconj]
228 simpa [K, commutatorElement_def, mul_assoc] using hcomm)
230/-- The continuous self-equivalence of topological abelianization induced by conjugation by a
231representative. -/
232noncomputable def conjugationTopologicalAbelianizationContinuousAut
233 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
234 (N : Subgroup G) [N.Normal] (g : G) :
235 TopologicalAbelianization N ≃ₜ* TopologicalAbelianization N :=
236 TopologicalAbelianization.congr (Subgroup.conjNormalContinuousMulEquiv (G := G) N g)
238/-- The representative-wise continuous automorphism has the same underlying algebraic action as
241 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
242 (N : Subgroup G) [N.Normal] (g : G) (n : N) :
243 conjugationTopologicalAbelianizationContinuousAut (G := G) N g
244 (TopologicalAbelianization.mk N n) =
245 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
246 (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n) := by
247 rfl
249/-- The conjugation action on a quotient induces the expected map on topological abelianization representatives. -/
250@[simp] theorem quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
251 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
252 (N : Subgroup G) [N.Normal] (g : G) (n : N) :
253 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
254 (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n) =
255 TopologicalAbelianization.mk N ((MulAut.conjNormal g) n) := by
256 dsimp [quotientConjugationTopologicalAbelianizationMap, TopologicalAbelianization.mk,
257 TopologicalAbelianization.mkₜ]
258 rfl
260/-- If every commutator correction lies in the closed commutator subgroup, the induced conjugation
261action on the topological abelianization is trivial. -/
263 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
264 (N : Subgroup G) [N.Normal] {x : G}
265 (hx :
266 ∀ n : N,
267 (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N) :
268 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
269 (QuotientGroup.mk' N x) = 1 := by
270 ext a
271 obtain ⟨n, rfl⟩ := QuotientGroup.mk'_surjective (Subgroup.closedCommutator N) a
272 exact
273 (QuotientGroup.eq_iff_div_mem (N := Subgroup.closedCommutator N)
274 (x := (MulAut.conjNormal x) n) (y := n)).2 (by
275 simpa [div_eq_mul_inv] using hx n)
277/-- The conjugation action fixes a representative exactly when the correction term lies in the
278closed commutator subgroup. -/
280 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
281 (N : Subgroup G) [N.Normal] {x : G} {n : N} :
282 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
283 (QuotientGroup.mk' N x) (TopologicalAbelianization.mk N n) =
284 TopologicalAbelianization.mk N n ↔
285 (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N := by
287 simpa [div_eq_mul_inv] using
288 (QuotientGroup.eq_iff_div_mem
289 (N := Subgroup.closedCommutator N)
290 (x := (MulAut.conjNormal x) n) (y := n))
292/-- The induced conjugation action is trivial exactly when every correction term lies in the
293closed commutator subgroup. -/
295 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
296 (N : Subgroup G) [N.Normal] {x : G} :
297 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
298 (QuotientGroup.mk' N x) = 1 ↔
299 ∀ n : N,
300 (((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N := by
301 constructor
302 · intro h n
303 have hpoint :=
304 congrArg
305 (fun φ : MulAut (TopologicalAbelianization N) => φ (TopologicalAbelianization.mk N n))
306 h
307 exact
309 (G := G) (N := N) (x := x) (n := n)).1 (by simpa using hpoint)
310 · intro hx
312 (G := G) (N := N) (x := x) hx
314/-- Central elements act trivially on the topological abelianization of a normal subgroup. -/
316 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
317 (N : Subgroup G) [N.Normal] {x : G} (hx : x ∈ Subgroup.center G) :
318 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
319 (QuotientGroup.mk' N x) = 1 := by
321 (G := G) (N := N)
322 intro n
323 have hxn : x * (n : G) = (n : G) * x := by
324 exact (Subgroup.mem_center_iff.mp hx (n : G)).symm
325 have hconj : MulAut.conjNormal x n = n := by
326 ext
327 rw [MulAut.conjNormal_apply]
328 simp only [hxn, mul_assoc, mul_inv_cancel, mul_one]
329 simp only [hconj, mul_inv_cancel, one_mem]
331/-- If a representative commutes with an element of `N`, then the induced action fixes its class in
332the topological abelianization. -/
334 {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
335 (N : Subgroup G) [N.Normal] {g : G} {x : N}
336 (hgx : g * (x : G) = (x : G) * g) :
337 quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
338 (QuotientGroup.mk' N g) (TopologicalAbelianization.mk N x) =
339 TopologicalAbelianization.mk N x := by
340 have hconj : (MulAut.conjNormal g) x = x := by
341 ext
342 rw [MulAut.conjNormal_apply]
343 simp only [hgx, mul_assoc, mul_inv_cancel, mul_one]
346/-- The image of `S ∩ U` in the topological abelianization of `U`. -/
347noncomputable def subgroupImageInTopologicalAbelianization
348 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
349 (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
350 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q)) :=
351 (((S ⊓ (U : Subgroup Q)).subgroupOf (U : Subgroup Q)).map
352 (TopologicalAbelianization.mk ↥(U : Subgroup Q)))
354@[simp] theorem mem_subgroupImageInTopologicalAbelianization_iff
355 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
356 (S : Subgroup Q) (U : OpenNormalSubgroup Q)
357 (y : TopologicalAbelianization ↥(U : Subgroup Q)) :
358 y ∈ subgroupImageInTopologicalAbelianization (Q := Q) S U ↔
359 ∃ x : ↥(U : Subgroup Q), (x : Q) ∈ S ∧ TopologicalAbelianization.mk _ x = y := by
360 simp only [subgroupImageInTopologicalAbelianization, ContinuousMonoidHom.coe_toMonoidHom,
361 Subgroup.inf_subgroupOf_right, Subgroup.mem_map, Subgroup.mem_subgroupOf, MonoidHom.coe_coe, Subtype.exists,
362 OpenSubgroup.mem_toSubgroup, exists_and_left]
364/-- Enlarging the ambient subgroup `S` enlarges its image in the abelianization of `U`. -/
366 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
367 {S T : Subgroup Q} (hST : S ≤ T) (U : OpenNormalSubgroup Q) :
368 subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
369 subgroupImageInTopologicalAbelianization (Q := Q) T U := by
370 intro y hy
371 rcases (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) S U y).1 hy with
372 ⟨x, hxS, hxy⟩
373 exact (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) T U y).2
374 ⟨x, hST hxS, hxy⟩
376/-- The map on abelianizations induced by an inclusion of open normal subgroups. -/
377noncomputable def topologicalAbelianizationMapOfOpenNormalSubgroupLe
378 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
379 {U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
380 TopologicalAbelianization ↥(U : Subgroup Q) →ₜ*
381 TopologicalAbelianization ↥(V : Subgroup Q) :=
382 TopologicalAbelianization.map
383 { toMonoidHom := Subgroup.inclusion hUV
384 continuous_toFun := by
385 apply Continuous.subtype_mk
386 exact continuous_subtype_val }
388@[simp] theorem topologicalAbelianizationMapOfOpenNormalSubgroupLe_apply_mk
389 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
390 {U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q))
391 (x : ↥(U : Subgroup Q)) :
392 topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV
393 (TopologicalAbelianization.mk ↥(U : Subgroup Q) x) =
394 TopologicalAbelianization.mk ↥(V : Subgroup Q) ⟨x.1, hUV x.2⟩ :=
395 rfl
397/-- Under an inclusion `U ≤ V`, the image from `U` maps into the image from `V`. -/
399 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
400 (S : Subgroup Q) {U V : OpenNormalSubgroup Q}
401 (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
402 (subgroupImageInTopologicalAbelianization (Q := Q) S U).map
403 (topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHom ≤
404 subgroupImageInTopologicalAbelianization (Q := Q) S V := by
405 intro y hy
406 rcases hy with ⟨x, hx, rfl⟩
407 rcases (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) S U x).1 hx with
408 ⟨a, haS, hax⟩
409 rw [← hax]
410 exact (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) S V _).2
411 ⟨⟨a.1, hUV a.2⟩, haS, rfl⟩
413/-- Comap form of `subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le`. -/
415 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
416 (S : Subgroup Q) {U V : OpenNormalSubgroup Q}
417 (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
418 subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
419 (subgroupImageInTopologicalAbelianization (Q := Q) S V).comap
420 (topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHom :=
421 Subgroup.map_le_iff_le_comap.mp
423 (Q := Q) S hUV)
425namespace OpenNormalAbelianizationImage
427/-- The image of `S` has finite abstract index in the topological abelianization of every open
428normal supergroup of `K`. -/
430 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
431 (S K : Subgroup Q) : Prop :=
432 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
433 Finite
434 ((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
435 subgroupImageInTopologicalAbelianization (Q := Q) S U)
437/-- The topological closure of the image of `S ∩ U` in the topological abelianization of `U`. -/
438noncomputable def closedSubgroupImageInTopologicalAbelianization
439 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
440 (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
441 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q)) :=
442 (subgroupImageInTopologicalAbelianization (Q := Q) S U).topologicalClosure
445 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
446 (S : Subgroup Q) (U : OpenNormalSubgroup Q) :
447 closedSubgroupImageInTopologicalAbelianization (Q := Q) S U =
448 (subgroupImageInTopologicalAbelianization (Q := Q) S U).topologicalClosure :=
449 rfl
451/-- The closed image of `S` is open in every open normal supergroup of `K`. -/
452def OpenClosure
453 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
454 (S K : Subgroup Q) : Prop :=
455 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
456 IsOpen
457 ((closedSubgroupImageInTopologicalAbelianization (Q := Q) S U :
458 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) : Set
459 (TopologicalAbelianization ↥(U : Subgroup Q)))
461/-- The image of `S` is closed and has finite quotient in every open normal supergroup of `K`. -/
463 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
464 (S K : Subgroup Q) : Prop :=
465 ∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
466 IsClosed
467 ((subgroupImageInTopologicalAbelianization (Q := Q) S U :
468 Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) : Set
469 (TopologicalAbelianization ↥(U : Subgroup Q))) ∧
470 Finite
471 ((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
472 subgroupImageInTopologicalAbelianization (Q := Q) S U)
474/-- Finite topological index includes finite abstract index as its quotient-size component. -/
476 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
477 {S K : Subgroup Q}
478 (h : FiniteTopologicalIndex (Q := Q) S K) :
479 FiniteAbstractIndex (Q := Q) S K :=
480 fun U hKU => (h U hKU).2
482end OpenNormalAbelianizationImage
484end ProCGroups.Abelian