Source: ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
1import Mathlib.Topology.Algebra.ClopenNhdofOne
3/-!
4# Open-normal neighborhood bases at the identity
6Every identity neighborhood in a profinite group contains an open normal subgroup. This file
7packages that refinement result for later basis, separation, and inverse-limit arguments.
8-/
10namespace ProCGroups.ProC
12universe u v
14section
16variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
18/--
19In a compact totally disconnected topological group, any open neighborhood of \(1\) contains an
20open normal subgroup.
21-/
22theorem exists_openNormalSubgroup_sub_open_nhds_of_one [CompactSpace G]
23 [TotallyDisconnectedSpace G] {W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
24 ∃ U : OpenNormalSubgroup G, ((U : Subgroup G) : Set G) ⊆ W := by
25 obtain ⟨U, hU⟩ :=
26 ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one hW h1W
27 exact ⟨U, fun _ hx ↦ hU hx⟩
29end
31end ProCGroups.ProC