Existence of an open normal subgroup in any clopen neighborhood of the neutral element

This file proves the lemma IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one, which states that in a compact topological group, for any clopen neighborhood of 1, there exists an open normal subgroup contained within it.

We then apply this lemma to show ProfiniteGrp.closedSubgroup_eq_sInf_open: any closed subgroup of a profinite group is the intersection of the open subgroups containing it.

This file is split out from the file OpenSubgroup because it needs more imports.

theorem IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) : ∃ (H : OpenNormalSubgroup G), ↑H ⊆ W

theorem IsTopologicalAddGroup.exist_openNormalAddSubgroup_sub_clopen_nhds_of_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 0 ∈ W) : ∃ (H : OpenNormalAddSubgroup G), ↑H ⊆ W

theorem ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Set G} (UOpen : IsOpen U) (einU : 1 ∈ U) : ∃ (H : OpenNormalSubgroup G), ↑H ⊆ U

theorem ProfiniteGrp.exist_openNormalAddSubgroup_sub_open_nhds_of_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Set G} (UOpen : IsOpen U) (einU : 0 ∈ U) : ∃ (H : OpenNormalAddSubgroup G), ↑H ⊆ U

theorem ProfiniteGrp.closedSubgroup_eq_sInf_open {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : ClosedSubgroup G) : ↑H = sInf {N : Subgroup G | IsOpen ↑N ∧ ↑H ≤ N}

Any closed subgroup of a profinite group is the intersection of the open subgroups containing it. See https://math.stackexchange.com/questions/5023433/closed-subgroups-of-a-compact-topological-group.

theorem ProfiniteGrp.closedAddSubgroup_eq_sInf_open {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : ClosedAddSubgroup G) : ↑H = sInf {N : AddSubgroup G | IsOpen ↑N ∧ ↑H ≤ N}

Any closed subgroup of a profinite group is the intersection of the open subgroups containing it. See https://math.stackexchange.com/questions/5023433/closed-subgroups-of-a-compact-topological-group.