ProCGroups/ProC/Quotients/ClosedSubgroupNeighborhoods.lean
1import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
2import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
3import ProCGroups.ProC.Quotients.LeftQuotientMaps
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/Quotients/ClosedSubgroupNeighborhoods.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C groups and open normal quotients
16Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
17-/
19open Set
20open scoped Topology Pointwise
22namespace ProCGroups.ProC
24universe u v
26open InverseSystems
28variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30/-- Given an open subgroup of a closed subgroup of a profinite group, one can shrink it to the
31intersection with an ambient open normal subgroup. -/
33 (hG : IsProfiniteGroup G) (H : ClosedSubgroup G) (U : OpenSubgroup H) :
34 ∃ V : OpenNormalSubgroup G,
36 (U : Subgroup H) := by
37 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
38 letI : T2Space G := IsProfiniteGroup.t2Space hG
39 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
40 have hU_nhds : (((U : Subgroup H) : Set H)) ∈ 𝓝 (1 : H) := by
41 exact U.isOpen'.mem_nhds U.one_mem'
42 rcases (mem_nhds_subtype (H : Set G) (1 : H) (((U : Subgroup H) : Set H))).1 hU_nhds with
43 ⟨W, hW_nhds, hWU⟩
44 rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
45 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW'open h1W' with ⟨V, hVW'⟩
46 refine ⟨V, ?_⟩
47 intro x hx
48 exact hWU <| by
49 change x.1 ∈ W
50 exact hW'W (hVW' hx)
52omit [IsTopologicalGroup G] in
53/-- Class-restricted version of `exists_openNormalSubgroup_inter_closedSubgroup_le` for a
54closed subgroup of a pro-`C` group. -/
56 {C : FiniteGroupClass.{u}} (hG : IsProCGroup C G)
57 (H : ClosedSubgroup G) (U : OpenSubgroup H) :
58 ∃ V : OpenNormalSubgroupInClass C G,
60 Subgroup H) ≤
61 (U : Subgroup H) := by
62 letI : CompactSpace G := IsProCGroup.compactSpace hG
63 letI : T2Space G := IsProCGroup.t2Space hG
64 letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
65 have hU_nhds : (((U : Subgroup H) : Set H)) ∈ 𝓝 (1 : H) := by
66 exact U.isOpen'.mem_nhds U.one_mem'
67 rcases (mem_nhds_subtype (H : Set G) (1 : H) (((U : Subgroup H) : Set H))).1
68 hU_nhds with
69 ⟨W, hW_nhds, hWU⟩
70 rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
71 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW'open h1W' with
72 ⟨V, hVW'⟩
73 refine ⟨V, ?_⟩
74 intro x hx
75 exact hWU <| by
76 change x.1 ∈ W
77 exact hW'W (hVW' hx)
79end ProCGroups.ProC