Source: ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods
1import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
2import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
3import ProCGroups.ProC.Quotients.LeftQuotientMaps
5/-!
6# Open-normal neighborhoods of closed subgroups
8Given an open neighborhood of a closed subgroup, this file finds an open normal subgroup whose
9intersection with the closed subgroup lies in that neighborhood, including a version whose finite
10quotient belongs to a prescribed class.
11-/
13open Set
14open scoped Topology Pointwise
16namespace ProCGroups.ProC
18universe u v
20open InverseSystems
22variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24/--
25Given an open subgroup of a closed subgroup of a profinite group, one can shrink it to the
26intersection with an ambient open normal subgroup.
27-/
28theorem exists_openNormalSubgroup_inter_closedSubgroup_le
29 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
30 (H : ClosedSubgroup G) (U : OpenSubgroup H) :
31 ∃ V : OpenNormalSubgroup G,
32 (OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V : Subgroup H) ≤
33 (U : Subgroup H) := by
34 have hU_nhds : (((U : Subgroup H) : Set H)) ∈ 𝓝 (1 : H) := by
35 exact U.isOpen'.mem_nhds U.one_mem'
36 rcases (mem_nhds_subtype (H : Set G) (1 : H) (((U : Subgroup H) : Set H))).1 hU_nhds with
37 ⟨W, hW_nhds, hWU⟩
38 rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
39 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW'open h1W' with ⟨V, hVW'⟩
40 refine ⟨V, ?_⟩
41 intro x hx
42 exact hWU <| by
43 change x.1 ∈ W
44 exact hW'W (hVW' hx)
46omit [IsTopologicalGroup G] in
47/--
48Class-restricted version of \(exists_openNormalSubgroup_inter_closedSubgroup_le\) for a closed
49subgroup of a pro-\(C\) group.
50-/
51theorem exists_openNormalSubgroupInClass_inter_closedSubgroup_le
52 {C : FiniteGroupClass.{u}} (hG : HasOpenNormalBasisInClass C G)
53 (H : ClosedSubgroup G) (U : OpenSubgroup H) :
54 ∃ V : OpenNormalSubgroupInClass C G,
55 (OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V.1 :
56 Subgroup H) ≤
57 (U : Subgroup H) := by
58 have hU_nhds : (((U : Subgroup H) : Set H)) ∈ 𝓝 (1 : H) := by
59 exact U.isOpen'.mem_nhds U.one_mem'
60 rcases (mem_nhds_subtype (H : Set G) (1 : H) (((U : Subgroup H) : Set H))).1
61 hU_nhds with
62 ⟨W, hW_nhds, hWU⟩
63 rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
64 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW'open h1W' with
65 ⟨V, hVW'⟩
66 refine ⟨V, ?_⟩
67 intro x hx
68 exact hWU <| by
69 change x.1 ∈ W
70 exact hW'W (hVW' hx)
72end ProCGroups.ProC