Yamaguchi Lean 4 Library
Source: ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
ProCGroups/ProC/OpenNormalSubgroups/ProCGroup/Source

Source: ProCGroups.ProC.OpenNormalSubgroups.ProCGroup

1import ProCGroups.FiniteGroups.AllFinite
2import ProCGroups.InverseSystems.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.Basic
4import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
6/-!
7# Open-normal quotient bases in a finite-group class
9`HasOpenNormalBasisInClass C G` says exactly that the identity neighborhoods of `G` have a basis
10of open normal subgroups whose quotients lie in `C`. It does not assert compactness, Hausdorffness,
11total disconnectedness, or even the topological-group laws.
13For an ambient `ProfiniteGrp`, this is precisely the additional property used to define the bundled
14category `ProCGrp C`.
16The module also packages the class-indexed open normal subgroups, their quotient projections and
17transition maps, and the separation consequences of a Hausdorff open-normal basis.
18-/
20namespace ProCGroups.ProC
22universe u v
24section
26variable {C : FiniteGroupClass.{u}}
27variable {G : Type u} [Group G] [TopologicalSpace G]
29/-- The identity-neighborhood basis property for open normal subgroups with quotient in \(C\).
31This predicate deliberately carries no profiniteness assumptions. A bundled pro-\(C\) object is an
32ambient `ProfiniteGrp` satisfying this additional property, as expressed by `ProCGrp C`. -/
33def HasOpenNormalBasisInClass (C : FiniteGroupClass.{u})
34 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
35 ∀ W : Set G, IsOpen W → (1 : G) ∈ W →
36 ∃ U : OpenNormalSubgroup G,
37 ((U : Subgroup G) : Set G) ⊆ W ∧ C (G ⧸ (U : Subgroup G))
39/-- Universe-independent open-normal basis membership. Quotients are tested up to multiplicative
40equivalence with a finite group represented in the carrier universe of `C`. -/
41def HasOpenNormalBasisInClassAcrossUniverses (C : FiniteGroupClass.{u})
42 (G : Type v) [Group G] [TopologicalSpace G] : Prop :=
43 ∀ W : Set G, IsOpen W → (1 : G) ∈ W →
44 ∃ U : OpenNormalSubgroup G,
45 ((U : Subgroup G) : Set G) ⊆ W ∧ C.MemAcrossUniverses (G ⧸ (U : Subgroup G))
47/-- In the native universe of `C`, the universe-independent and original basis predicates agree. -/
48theorem hasOpenNormalBasisInClassAcrossUniverses_iff
49 {C : FiniteGroupClass.{u}} {G : Type u} [Group G] [TopologicalSpace G] :
50 HasOpenNormalBasisInClassAcrossUniverses C G ↔ HasOpenNormalBasisInClass C G := by
51 constructor
52 · intro h W hW h1W
53 rcases h W hW h1W with ⟨U, hUW, hCU⟩
54 exact ⟨U, hUW, (C.memAcrossUniverses_iff).1 hCU⟩
55 · intro h W hW h1W
56 rcases h W hW h1W with ⟨U, hUW, hCU⟩
57 exact ⟨U, hUW, (C.memAcrossUniverses_iff).2 hCU⟩
59namespace HasOpenNormalBasisInClass
61/--
62The existence of an open-normal basis in a class is monotone under enlarging the finite-group
63class.
64-/
65theorem mono {C D : FiniteGroupClass.{u}} {G : Type u} [Group G] [TopologicalSpace G]
66 (hbasis : HasOpenNormalBasisInClass C G)
67 (hmono : ∀ {Q : Type u} [Group Q], C Q → D Q) :
68 HasOpenNormalBasisInClass D G := by
69 intro W hW h1W
70 rcases hbasis W hW h1W with ⟨U, hUW, hCU⟩
71 exact ⟨U, hUW, hmono hCU⟩
73end HasOpenNormalBasisInClass
75/--
76Open normal subgroups whose quotient lies in the chosen class \(C\). This packages the specified
77family as an actual type so later inverse-limit and basis constructions can quantify over it
78directly.
79-/
80abbrev OpenNormalSubgroupInClass (C : FiniteGroupClass.{u})
81 (G : Type u) [Group G] [TopologicalSpace G] :=
82 {U : OpenNormalSubgroup G // C (G ⧸ (U : Subgroup G))}
84namespace OpenNormalSubgroupInClass
86variable {C : FiniteGroupClass.{u}}
87variable {G : Type u} [Group G] [TopologicalSpace G]
89/--
90Repackage an open normal subgroup together with a certificate that its quotient lies in \(C\).
91-/
92def ofOpenNormal (U : OpenNormalSubgroup G) (hU : C (G ⧸ (U : Subgroup G))) :
93 OpenNormalSubgroupInClass C G :=
94 ⟨U, hU⟩
96/-- The quotient attached to a normal subgroup in the finite-quotient index family lies in \(C\). -/
97theorem quotient_mem (U : OpenNormalSubgroupInClass C G) :
98 C (G ⧸ (U.1 : Subgroup G)) :=
99 U.2
101/-- Move an open-normal-in-class subgroup along an inclusion of finite-group classes. -/
102def of_mono {D : FiniteGroupClass.{u}}
103 (hmono : ∀ {Q : Type u} [Group Q], C Q → D Q)
104 (U : OpenNormalSubgroupInClass C G) :
105 OpenNormalSubgroupInClass D G :=
106 ⟨U.1, hmono U.2⟩
108/-- The top subgroup belongs to any finite-group class containing trivial quotients. -/
109def top [FiniteGroupClass.ContainsTrivialQuotients C] :
110 OpenNormalSubgroupInClass C G :=
111 ⟨⊤, by
112 have hsub : Subsingleton (G ⧸ (⊤ : Subgroup G)) := by
113 constructor
114 intro x y
115 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) x with ⟨a, rfl⟩
116 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) y with ⟨b, rfl⟩
117 exact QuotientGroup.eq.2 (by simp only [Subgroup.mem_top])
118 exact FiniteGroupClass.ContainsTrivialQuotients.of_subsingleton hsub⟩
120/-- There is an open-normal-in-class subgroup whenever the class contains trivial quotients. -/
121theorem nonempty_of_containsTrivialQuotients [FiniteGroupClass.ContainsTrivialQuotients C] :
122 Nonempty (OpenNormalSubgroupInClass C G) :=
123 ⟨top (C := C) (G := G)⟩
125/-- Every open normal quotient of a compact group lies in the all-finite class. -/
126def of_allFinite [ContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) :
127 OpenNormalSubgroupInClass FiniteGroupClass.allFinite G :=
128 ⟨U, openNormalSubgroup_finiteQuotient (G := G) U⟩
130/--
131Pull back an open-normal-in-class subgroup along a continuous homomorphism, when the class is
132hereditary.
133-/
134noncomputable def comap {H : Type u} [Group H] [TopologicalSpace H]
135 (hHer : FiniteGroupClass.Hereditary C) (f : G →ₜ* H)
136 (U : OpenNormalSubgroupInClass C H) : OpenNormalSubgroupInClass C G :=
137 let N : OpenNormalSubgroup G :=
138 OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun U.1
139 ⟨N, by
140 let qmap : G ⧸ (N : Subgroup G) →* H ⧸ (U.1 : Subgroup H) :=
141 QuotientGroup.map (N := (N : Subgroup G)) (M := (U.1 : Subgroup H))
142 f.toMonoidHom (by
143 intro x hx
144 exact hx)
145 have hqmap_inj : Function.Injective qmap := by
146 rw [← MonoidHom.ker_eq_bot_iff qmap]
147 ext z
148 constructor
149 · intro hz
150 rcases QuotientGroup.mk'_surjective (N : Subgroup G) z with ⟨x, rfl⟩
151 have hxU : f x ∈ (U.1 : Subgroup H) := by
152 apply (QuotientGroup.eq_one_iff (N := (U.1 : Subgroup H)) (f x)).1
153 simpa [qmap, MonoidHom.mem_ker] using hz
154 exact (QuotientGroup.eq_one_iff (N := (N : Subgroup G)) x).2 hxU
155 · intro hz
156 subst z
157 simp only [one_mem]
158 exact hHer.of_injective U.2 qmap hqmap_inj⟩
160/--
161An open surjective continuous homomorphism sends an open-normal-in-class subgroup to an open
162normal subgroup when target quotient membership is supplied explicitly. This is the lightweight
163bridge; stronger automatic versions can be derived from class closure hypotheses as needed.
164-/
165def mapOpenNormal {H : Type u} [Group H] [TopologicalSpace H]
166 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
167 (U : OpenNormalSubgroupInClass C G)
168 (hC : C (H ⧸ ((OpenNormalSubgroup.map f hfopen hfsurj U.1 : OpenNormalSubgroup H) :
169 Subgroup H))) :
170 OpenNormalSubgroupInClass C H :=
171 ⟨OpenNormalSubgroup.map f hfopen hfsurj U.1, hC⟩
173/--
174An open surjective continuous homomorphism sends an in-class open normal subgroup to an in-class
175open normal subgroup. Formation closure supplies the target quotient membership.
176-/
177def mapOpenNormal_of_formation {H : Type u} [Group H] [TopologicalSpace H]
178 (hForm : FiniteGroupClass.Formation C)
179 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
180 (U : OpenNormalSubgroupInClass C G) :
181 OpenNormalSubgroupInClass C H :=
182 mapOpenNormal (C := C) (G := G) f hfopen hfsurj U (by
183 let M : OpenNormalSubgroup H := OpenNormalSubgroup.map f hfopen hfsurj U.1
184 let qmap : G ⧸ (U.1 : Subgroup G) →* H ⧸ (M : Subgroup H) :=
185 QuotientGroup.map (N := (U.1 : Subgroup G)) (M := (M : Subgroup H))
186 f.toMonoidHom (by
187 intro x hx
188 exact ⟨x, hx, rfl⟩)
189 have hqmap_surj : Function.Surjective qmap :=
190 QuotientGroup.map_surjective_of_surjective
191 (N := (U.1 : Subgroup G)) (M : Subgroup H) f.toMonoidHom (by
192 intro y
193 rcases QuotientGroup.mk'_surjective (M : Subgroup H) y with ⟨h, rfl⟩
194 rcases hfsurj h with ⟨g, rfl⟩
195 exact ⟨g, rfl⟩) (by
196 intro x hx
197 exact ⟨x, hx, rfl⟩)
198 have hquot :
199 C ((G ⧸ (U.1 : Subgroup G)) ⧸ qmap.ker) :=
200 hForm.quotientClosed qmap.ker U.2
201 let e :
202 (G ⧸ (U.1 : Subgroup G)) ⧸ qmap.ker ≃*
203 H ⧸ (M : Subgroup H) :=
204 QuotientGroup.quotientKerEquivOfSurjective qmap hqmap_surj
205 exact hForm.isomClosed ⟨e⟩ hquot)
207/-- Finite intersections stay in class for a formation. -/
208def inf (hForm : FiniteGroupClass.Formation C)
209 (U V : OpenNormalSubgroupInClass C G) : OpenNormalSubgroupInClass C G :=
210 ⟨U.1 ⊓ V.1,
211 FiniteGroupClass.Formation.quotient_inf_mem
212 (C := C) (G := G) hForm U.1 V.1 U.2 V.2⟩
214/-- The quotient projection attached to an open-normal-in-class subgroup. -/
215def quotientProj (U : OpenNormalSubgroupInClass C G) :
216 G →ₜ* G ⧸ (U.1 : Subgroup G) :=
217 OpenNormalSubgroup.quotientProj U.1
219/-- The quotient projection evaluates to the quotient class of the element. -/
220@[simp]
221theorem quotientProj_apply (U : OpenNormalSubgroupInClass C G) (x : G) :
222 quotientProj (C := C) U x = QuotientGroup.mk' (U.1 : Subgroup G) x :=
223 rfl
225/-- The quotient projection attached to an open-normal-in-class subgroup is surjective. -/
226@[simp]
227theorem quotientProj_surjective (U : OpenNormalSubgroupInClass C G) :
228 Function.Surjective (quotientProj (C := C) U) :=
229 OpenNormalSubgroup.quotientProj_surjective U.1
231/-- The kernel predicate of the quotient projection is membership in the subgroup. -/
232@[simp]
233theorem quotientProj_eq_one_iff {U : OpenNormalSubgroupInClass C G} {x : G} :
234 quotientProj (C := C) U x = 1 ↔ x ∈ (U.1 : Subgroup G) :=
235 OpenNormalSubgroup.quotientProj_eq_one_iff (U := U.1)
237/-- Equality in the quotient attached to an open-normal-in-class subgroup. -/
238theorem quotientProj_eq_quotientProj_iff {U : OpenNormalSubgroupInClass C G} {x y : G} :
239 quotientProj (C := C) U x = quotientProj (C := C) U y ↔
240 x / y ∈ (U.1 : Subgroup G) :=
241 OpenNormalSubgroup.quotientProj_eq_quotientProj_iff (U := U.1)
243/-- Kernel membership for the quotient projection attached to an open-normal-in-class subgroup. -/
244@[simp]
245theorem mem_ker_quotientProj [ContinuousMul G] {U : OpenNormalSubgroupInClass C G} {x : G} :
246 x ∈ OpenNormalSubgroup.ker (quotientProj (C := C) U) ↔
247 x ∈ (U.1 : Subgroup G) :=
248 OpenNormalSubgroup.mem_ker_quotientProj (U := U.1)
250/-- The open-normal kernel of the quotient projection is the original subgroup. -/
251@[simp]
252theorem ker_quotientProj [ContinuousMul G] (U : OpenNormalSubgroupInClass C G) :
253 ((OpenNormalSubgroup.ker (quotientProj (C := C) U) : OpenNormalSubgroup G) :
254 Subgroup G) = (U.1 : Subgroup G) :=
255 OpenNormalSubgroup.ker_quotientProj U.1
257/--
258The canonical transition map between quotients attached to nested open normal subgroups in the
259class-indexing family.
260-/
261def map {U V : OpenNormalSubgroupInClass C G}
262 (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
263 G ⧸ (V.1 : Subgroup G) →* G ⧸ (U.1 : Subgroup G) :=
264 QuotientGroup.map _ _ (MonoidHom.id G) hUV
266/-- These transition maps are the natural quotient epimorphisms. -/
267theorem map_surjective {U V : OpenNormalSubgroupInClass C G}
268 (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
269 Function.Surjective (map (C := C) (G := G) hUV) := by
270 intro x
271 rcases QuotientGroup.mk'_surjective (U.1 : Subgroup G) x with ⟨g, rfl⟩
272 exact ⟨QuotientGroup.mk' (V.1 : Subgroup G) g, rfl⟩
274/-- The identity transition map is the identity monoid homomorphism. -/
275theorem map_id (U : OpenNormalSubgroupInClass C G) :
276 map (C := C) (G := G) (le_rfl : (U.1 : Subgroup G) ≤ (U.1 : Subgroup G)) = MonoidHom.id _ := by
277 simp only [map, QuotientGroup.map_id]
279/-- Maps induced on topological abelianizations compose as expected. -/
280theorem map_comp {U V W : OpenNormalSubgroupInClass C G}
281 (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G))
282 (hVW : (W.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
283 (map (C := C) (G := G) hUV).comp (map (C := C) (G := G) hVW) =
284 map (C := C) (G := G) (hVW.trans hUV) := by
285 simpa [map] using QuotientGroup.map_comp_map
286 (N := (W.1 : Subgroup G)) (M := (V.1 : Subgroup G)) (O := (U.1 : Subgroup G))
287 (f := MonoidHom.id G) (g := MonoidHom.id G) hVW hUV
289/--
290The continuous transition map between quotients attached to nested open-normal-in-class
291subgroups.
292-/
293def transition {U V : OpenNormalSubgroupInClass C G}
294 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
295 G ⧸ (U.1 : Subgroup G) →ₜ* G ⧸ (V.1 : Subgroup G) :=
296 OpenNormalSubgroup.transition (G := G) (U := U.1) (V := V.1) hUV
298/-- Transition maps send quotient classes to the corresponding quotient classes. -/
299@[simp]
300theorem transition_mk {U V : OpenNormalSubgroupInClass C G}
301 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) (x : G) :
302 transition (C := C) (G := G) hUV (QuotientGroup.mk' (U.1 : Subgroup G) x) =
303 QuotientGroup.mk' (V.1 : Subgroup G) x :=
304 OpenNormalSubgroup.transition_mk (G := G) (U := U.1) (V := V.1) hUV x
306/--
307Composing the transition map with the smaller quotient projection gives the larger quotient
308projection.
309-/
310@[simp]
311theorem transition_comp_quotientProj {U V : OpenNormalSubgroupInClass C G}
312 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
313 (transition (C := C) (G := G) hUV).comp (quotientProj (C := C) U) =
314 quotientProj (C := C) V :=
315 OpenNormalSubgroup.transition_comp_quotientProj (G := G) (U := U.1) (V := V.1) hUV
317/-- Transition maps between quotients by nested open-normal-in-class subgroups are surjective. -/
318theorem transition_surjective {U V : OpenNormalSubgroupInClass C G}
319 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
320 Function.Surjective (transition (C := C) (G := G) hUV) :=
321 OpenNormalSubgroup.transition_surjective (G := G) (U := U.1) (V := V.1) hUV
323end OpenNormalSubgroupInClass
325section
327variable {C : FiniteGroupClass.{u}}
328variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
330/--
331The inverse system of quotient groups indexed by open normal subgroups whose quotients lie in
332\(C\), ordered by reverse inclusion.
333-/
334def openNormalSubgroupInClassSystem (C : FiniteGroupClass.{u})
335 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
336 InverseSystems.InverseSystem (I := OrderDual (OpenNormalSubgroupInClass C G)) where
337 X := fun U => G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
338 topologicalSpace := fun _ => inferInstance
339 map := fun {U V} hUV =>
340 OpenNormalSubgroupInClass.map (C := C) (G := G)
341 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV
342 continuous_map := by
343 intro U V hUV
344 letI : DiscreteTopology
345 (G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) :=
346 QuotientGroup.discreteTopology
347 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
348 exact continuous_of_discreteTopology
349 map_id := by
350 intro U
351 funext x
352 exact congrFun
353 (congrArg DFunLike.coe
354 (OpenNormalSubgroupInClass.map_id
355 (C := C) (G := G) (U := OrderDual.ofDual U))) x
356 map_comp := by
357 intro U V W hUV hVW
358 funext x
359 rcases QuotientGroup.mk'_surjective
360 ((((OrderDual.ofDual W).1 : OpenNormalSubgroup G) : Subgroup G)) x with ⟨g, rfl⟩
361 rfl
363/-- Every coordinate of the open-normal-in-class inverse system is a quotient group. -/
364instance instGroupOpenNormalSubgroupInClassSystemX
365 (U : OrderDual (OpenNormalSubgroupInClass C G)) :
366 Group ((openNormalSubgroupInClassSystem C G).X U) :=
367 QuotientGroup.Quotient.group
368 (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
370/--
371The canonical quotient homomorphisms from \(G\) into the open-normal-subgroup inverse system
372whose quotients lie in \(C\).
373-/
374def openNormalSubgroupInClassProj
375 (U : OrderDual (OpenNormalSubgroupInClass C G)) :
376 G →* G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) :=
377 QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
379/-- The canonical quotient homomorphisms are compatible with the transition maps. -/
380theorem openNormalSubgroupInClassProj_compatible :
381 (openNormalSubgroupInClassSystem C G).CompatibleMaps
382 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
383 openNormalSubgroupInClassProj (C := C) (G := G) U) := by
384 intro U V hUV
385 funext g
386 rfl
388/-- The quotient system attached to open normal subgroups in \(C\) is group-valued. -/
389instance instIsGroupSystemOpenNormalSubgroupInClassSystem :
390 InverseSystems.IsGroupSystem (openNormalSubgroupInClassSystem C G) where
391 map_one := by
392 intro i j hij
393 change
394 OpenNormalSubgroupInClass.map
395 (C := C) (G := G)
396 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij 1 = 1
397 exact
398 (OpenNormalSubgroupInClass.map
399 (C := C) (G := G)
400 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_one
401 map_mul := by
402 intro i j hij x y
403 change
404 OpenNormalSubgroupInClass.map
405 (C := C) (G := G)
406 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij (x * y) =
407 OpenNormalSubgroupInClass.map
408 (C := C) (G := G)
409 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x *
410 OpenNormalSubgroupInClass.map
411 (C := C) (G := G)
412 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij y
413 exact
414 (OpenNormalSubgroupInClass.map
415 (C := C) (G := G)
416 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_mul x y
417 map_inv := by
418 intro i j hij x
419 change
420 OpenNormalSubgroupInClass.map
421 (C := C) (G := G)
422 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x⁻¹ =
423 (OpenNormalSubgroupInClass.map
424 (C := C) (G := G)
425 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x)⁻¹
426 exact
427 (OpenNormalSubgroupInClass.map
428 (C := C) (G := G)
429 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_inv x
431omit [IsTopologicalGroup G] in
432/-- Each projection from \(G\) to an open-normal-in-class quotient is surjective. -/
433theorem openNormalSubgroupInClassProj_surjective
434 (U : OrderDual (OpenNormalSubgroupInClass C G)) :
435 Function.Surjective (openNormalSubgroupInClassProj (C := C) (G := G) U) :=
436 QuotientGroup.mk'_surjective _
438omit [IsTopologicalGroup G] in
439/-- The open-normal-in-class index family is directed under reverse inclusion. -/
440theorem directed_openNormalSubgroupInClass
441 (hForm : FiniteGroupClass.Formation C) :
442 Directed (α := OrderDual (OpenNormalSubgroupInClass C G)) (· ≤ ·) fun U => U := by
443 intro U V
444 let W : OpenNormalSubgroupInClass C G :=
445 ⟨U.1 ⊓ V.1,
446 FiniteGroupClass.Formation.quotient_inf_mem
447 (C := C) (G := G) hForm U.1 V.1 U.2 V.2⟩
448 refine ⟨OrderDual.toDual W, ?_, ?_⟩
449 · change ((W.1 : Subgroup G) ≤ (U.1 : Subgroup G))
450 exact inf_le_left
451 · change ((W.1 : Subgroup G) ≤ (V.1 : Subgroup G))
452 exact inf_le_right
454end
458variable {C : FiniteGroupClass.{u}}
459variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
461namespace HasOpenNormalBasisInClass
463omit [IsTopologicalGroup G] in
464/-- The open-normal quotient-basis property is preserved by continuous multiplicative
465equivalences. -/
466theorem ofContinuousMulEquiv
467 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
468 (hG : HasOpenNormalBasisInClass C G) (e : G ≃ₜ* H) :
469 HasOpenNormalBasisInClass C H := by
470 intro W hW h1W
471 have hpreOpen : IsOpen (e ⁻¹' W) := hW.preimage e.continuous
472 have hpreOne : (1 : G) ∈ e ⁻¹' W := by
473 simpa using h1W
474 rcases hG (e ⁻¹' W) hpreOpen hpreOne with ⟨U, hUW, hCU⟩
475 let V : OpenNormalSubgroup H :=
476 OpenNormalSubgroup.map (ContinuousMonoidHom.toContinuousMonoidHom e)
477 (Homeomorph.isOpenMap e.toHomeomorph) e.surjective U
478 refine ⟨V, ?_, ?_⟩
479 · intro h hh
480 change h ∈ (U : Subgroup G).map (ContinuousMonoidHom.toContinuousMonoidHom e).toMonoidHom at hh
481 rcases hh with ⟨g, hg, rfl⟩
482 exact hUW hg
483 · simpa [V] using
484 C.mem_of_mulEquiv
485 (OpenNormalSubgroup.quotientMapContinuousMulEquiv e U) hCU
487omit [IsTopologicalGroup G] in
488/-- With isomorphism and quotient closure, the basis property implies that every open-normal
489quotient lies in the class. -/
490theorem hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
491 (hIso : FiniteGroupClass.IsomClosed C)
492 (hQuot : FiniteGroupClass.QuotientClosed C)
493 (hG : HasOpenNormalBasisInClass C G) :
494 ∀ U : OpenNormalSubgroup G, C (G ⧸ (U : Subgroup G)) := by
495 intro U
496 rcases hG (((U : Subgroup G) : Set G))
497 (openNormalSubgroup_isOpen (G := G) U) U.one_mem' with
498 ⟨V, hVU, hCV⟩
499 let q : G ⧸ (V : Subgroup G) →ₜ* G ⧸ (U : Subgroup G) :=
500 OpenNormalSubgroup.transition (G := G) hVU
501 have hqsurj : Function.Surjective q := OpenNormalSubgroup.transition_surjective (G := G) hVU
502 have hQuot :
503 C ((G ⧸ (V : Subgroup G)) ⧸ q.toMonoidHom.ker) :=
504 hQuot (N := q.toMonoidHom.ker) hCV
505 exact hIso ⟨QuotientGroup.quotientKerEquivOfSurjective q.toMonoidHom hqsurj⟩ hQuot
507omit [IsTopologicalGroup G] in
508/-- For a group with an open-normal \(C\)-basis, every open-normal quotient lies in `C` when `C`
509is a formation. -/
510theorem quotient_mem (hForm : FiniteGroupClass.Formation C)
511 (hG : HasOpenNormalBasisInClass C G) (U : OpenNormalSubgroup G) :
512 C (G ⧸ (U : Subgroup G)) :=
513 hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
514 hForm.isomClosed hForm.quotientClosed hG U
516omit [IsTopologicalGroup G] in
517/-- Every open neighborhood of `1` contains an indexed open normal subgroup whose quotient lies
518in `C`. -/
519theorem exists_openNormalSubgroupInClass_sub_open_nhds_of_one (hG : HasOpenNormalBasisInClass C G)
520 {W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
521 ∃ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G)) ⊆ W := by
522 rcases hG W hW h1W with ⟨U, hUW, hCU⟩
523 exact ⟨⟨U, hCU⟩, hUW⟩
525section DiscreteCoset
527omit [IsTopologicalGroup G] in
528/-- A continuous map to a discrete target is locally fixed on a sufficiently small right coset,
529with the small subgroup chosen from the open normal subgroups whose quotients lie in `C`. -/
530theorem exists_openNormalSubgroupInClass_eq_on_right_coset_of_continuous_discrete
531 (hG : HasOpenNormalBasisInClass C G)
532 [ContinuousMul G]
533 {A : Type v} [TopologicalSpace A] [DiscreteTopology A]
534 (f : G → A) (hf : Continuous f) (g₀ : G) :
535 ∃ U : OpenNormalSubgroupInClass C G,
536 ∀ g : G, g * g₀⁻¹ ∈ (U.1 : Subgroup G) → f g = f g₀ := by
537 let W : Set G := {x | f (x * g₀) = f g₀}
538 have hW : IsOpen W := by
539 change IsOpen ((fun x : G => f (x * g₀)) ⁻¹' ({f g₀} : Set A))
540 exact isOpen_discrete _ |>.preimage (hf.comp (continuous_id.mul continuous_const))
541 have h1W : (1 : G) ∈ W := by
542 simp only [Set.mem_setOf_eq, one_mul, W]
543 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
544 refine ⟨U, ?_⟩
545 intro g hg
546 have hmem : g * g₀⁻¹ ∈ W := hUW hg
547 have hrewrite : (g * g₀⁻¹) * g₀ = g := by
548 simp only [mul_assoc, inv_mul_cancel, mul_one]
549 simpa [W, hrewrite] using hmem
551end DiscreteCoset
553section Hausdorff
555variable [T2Space G]
557omit [IsTopologicalGroup G] in
558/-- In a Hausdorff group with an open-normal \(C\)-basis, the open normal subgroups whose quotients
559lie in `C` have trivial total intersection. -/
560theorem iInf_openNormalSubgroupInClass_eq_bot (hG : HasOpenNormalBasisInClass C G) :
561 iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) = (⊥ : Subgroup G) := by
562 apply le_antisymm
563 · intro x hx
564 change x = 1
565 by_contra hxne
566 let W : Set G := ({x} : Set G)ᶜ
567 have hW : IsOpen W := by
568 simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
569 have h1W : (1 : G) ∈ W := by
570 have hx1 : (1 : G) ≠ x := by
571 intro h1x
572 exact hxne h1x.symm
573 simpa [W] using hx1
574 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
575 have hxall : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G) := by
576 simpa [Subgroup.mem_iInf] using hx
577 have hxU : x ∈ (U.1 : Subgroup G) := hxall U
578 have hxW : x ∈ W := hUW hxU
579 exact hxW (by simp only [Set.mem_singleton_iff])
580 · exact bot_le
582omit [IsTopologicalGroup G] in
583/-- Set-theoretic form of the trivial-intersection statement. -/
584theorem iInter_openNormalSubgroupInClass_eq_singleton (hG : HasOpenNormalBasisInClass C G) :
585 (⋂ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G))) = ({1} : Set G) := by
586 ext x
587 constructor
588 · intro hx
589 have hx' : x ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
590 simpa [Subgroup.mem_iInf, Set.mem_iInter] using hx
591 have hxbot : x ∈ (⊥ : Subgroup G) := by
592 simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hx'
593 simpa using hxbot
594 · rintro rfl
595 simp only [OpenSubgroup.coe_toSubgroup, Set.mem_iInter, SetLike.mem_coe, one_mem, implies_true]
597omit [IsTopologicalGroup G] in
598/-- Explicit family form of the open-normal basis and trivial-intersection package. -/
599theorem exists_openNormalBasisInClassFamily (hG : HasOpenNormalBasisInClass C G) :
600 ∃ ι : Type u, ∃ U : ι → OpenNormalSubgroup G,
601 (∀ i, C (G ⧸ (U i : Subgroup G))) ∧
602 (∀ W : Set G, IsOpen W → (1 : G) ∈ W →
603 ∃ i, (((U i : Subgroup G) : Set G)) ⊆ W) ∧
604 iInf (fun i => (U i : Subgroup G)) = (⊥ : Subgroup G) := by
605 refine ⟨OpenNormalSubgroupInClass C G, fun i => i.1, ?_, ?_, ?_⟩
606 · intro i
607 exact i.2
608 · intro W hW h1W
609 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
610 exact ⟨U, hUW⟩
611 · simpa using hG.iInf_openNormalSubgroupInClass_eq_bot
613omit [IsTopologicalGroup G] in
614/-- Membership in every open-normal-in-class subgroup forces an element to be trivial. -/
615theorem eq_one_of_mem_all_openNormalSubgroupInClass (hG : HasOpenNormalBasisInClass C G) {x : G}
616 (hx : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G)) :
617 x = 1 := by
618 have hx' : x ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
619 simpa [Subgroup.mem_iInf] using hx
620 have hxbot : x ∈ (⊥ : Subgroup G) := by
621 simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hx'
622 simpa using hxbot
624omit [IsTopologicalGroup G] in
625/-- If `x ≠ 1`, then some open normal subgroup in the class-family omits `x`. -/
626theorem exists_openNormalSubgroupInClass_not_mem (hG : HasOpenNormalBasisInClass C G) {x : G}
627 (hx : x ≠ 1) :
628 ∃ U : OpenNormalSubgroupInClass C G, x ∉ (U.1 : Subgroup G) := by
629 by_contra h
630 apply hx
631 apply hG.eq_one_of_mem_all_openNormalSubgroupInClass
632 intro U
633 by_contra hxU
634 exact h ⟨U, hxU⟩
636omit [IsTopologicalGroup G] in
637/-- In a Hausdorff group with an open-normal \(C\)-basis, two elements are equal once they agree in
638every quotient by an open normal subgroup whose quotient lies in `C`. -/
639theorem eq_of_forall_openNormalSubgroupInClass_quotient_eq (hG : HasOpenNormalBasisInClass C G)
640 {x y : G}
641 (hxy : ∀ U : OpenNormalSubgroupInClass C G,
642 QuotientGroup.mk' (U.1 : Subgroup G) x = QuotientGroup.mk' (U.1 : Subgroup G) y) :
643 x = y := by
644 have hxy' : x⁻¹ * y = 1 := by
645 apply hG.eq_one_of_mem_all_openNormalSubgroupInClass
646 intro U
647 exact QuotientGroup.eq.1 (hxy U)
648 calc
649 x = x * 1 := by simp only [mul_one]
650 _ = x * (x⁻¹ * y) := by rw [hxy']
651 _ = y := by simp only [mul_inv_cancel_left]
653omit [IsTopologicalGroup G] in
654/-- In a Hausdorff group with an open-normal \(C\)-basis, coordinatewise equality in the canonical
655inverse-system projections forces equality in the ambient group. -/
656theorem eq_of_forall_openNormalSubgroupInClassProj_eq (hG : HasOpenNormalBasisInClass C G) {x y : G}
657 (hxy : ∀ U : OrderDual (OpenNormalSubgroupInClass C G),
658 openNormalSubgroupInClassProj (C := C) (G := G) U x =
659 openNormalSubgroupInClassProj (C := C) (G := G) U y) :
660 x = y := by
661 apply hG.eq_of_forall_openNormalSubgroupInClass_quotient_eq
662 intro U
663 have hU := hxy (OrderDual.toDual U)
664 change
665 QuotientGroup.mk' (U.1 : Subgroup G) x =
666 QuotientGroup.mk' (U.1 : Subgroup G) y at hU
667 exact hU
669end Hausdorff
671/-- For a profinite group, the stronger all-open-normal-quotient condition supplies an open-normal
672\(C\)-basis. -/
673theorem of_allOpenNormalQuotients [CompactSpace G] [T2Space G]
674 [TotallyDisconnectedSpace G]
675 (hquot : ∀ U : OpenNormalSubgroup G, C (G ⧸ (U : Subgroup G))) :
676 HasOpenNormalBasisInClass C G := by
677 intro W hW h1W
678 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
679 exact ⟨U, hUW, hquot U⟩
681omit [IsTopologicalGroup G] in
682/-- An open-normal \(C\)-basis contains at least one subgroup. -/
683theorem openNormalSubgroupInClass_nonempty (hG : HasOpenNormalBasisInClass C G) :
684 Nonempty (OpenNormalSubgroupInClass C G) := by
685 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one
686 (W := Set.univ) isOpen_univ (by simp only [Set.mem_univ]) with ⟨U, _⟩
687 exact ⟨U⟩
689end HasOpenNormalBasisInClass
691end
693end ProCGroups.ProC