ProCGroups/ProC/OpenNormalSubgroups/ClosedAndCosets.lean
1import ProCGroups.Profinite.OpenSubgroups
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/ClosedAndCosets.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C groups and open normal quotients
14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
15-/
17namespace ProCGroups.ProC
19universe u v
21section
23variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25/-- A closed subgroup of a profinite group is the intersection of all
26open subgroups containing it.
28The proof uses Mathlib's clopen-neighborhood machinery for compact totally disconnected groups;
29this theorem is the unbundled subgroup form used by the pro-`C` API.
30-/
31theorem closedSubgroup_eq_sInf_open [CompactSpace G] [TotallyDisconnectedSpace G]
32 (H : ClosedSubgroup G) :
33 (H : Subgroup G) = sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N} := by
34 ext x
35 constructor
36 · intro hx
37 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
38 intro N hN
39 exact hN.2 hx
40 · intro hx
41 by_contra hxH
42 let W : Set G := { y : G | x * y⁻¹ ∉ (H : Set G) }
43 have hW : IsOpen W := by
44 change IsOpen ((fun y : G => x * y⁻¹) ⁻¹' ((H : Set G)ᶜ))
45 exact H.isClosed'.isOpen_compl.preimage (continuous_const.mul continuous_inv)
46 have h1W : (1 : G) ∈ W := by
47 simpa [W] using hxH
48 rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
49 (G := G) hW h1W with ⟨N, hNW⟩
50 let K : OpenSubgroup G :=
51 ⟨(H : Subgroup G) ⊔ (N : Subgroup G),
52 Subgroup.isOpen_of_openSubgroup ((H : Subgroup G) ⊔ (N : Subgroup G))
53 (show (N : Subgroup G) ≤ (H : Subgroup G) ⊔ (N : Subgroup G) from le_sup_right)⟩
54 have hHK : (H : Subgroup G) ≤ (K : Subgroup G) := by
55 intro y hy
56 exact Subgroup.mem_sup_left hy
57 have hxK : x ∈ (K : Subgroup G) := by
58 have hxall : ∀ N : Subgroup G, IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N → x ∈ N := by
59 simpa only [Subgroup.mem_sInf, Set.mem_setOf_eq] using hx
60 exact hxall (K : Subgroup G) ⟨openSubgroup_isOpen (G := G) K, hHK⟩
61 rcases
62 (Subgroup.mem_sup_of_normal_right (s := (H : Subgroup G)) (t := (N : Subgroup G))).1
63 hxK with
64 ⟨h, hhH, n, hnN, hxn⟩
65 have hnW : n ∈ W := hNW hnN
66 have : h ∉ (H : Set G) := by
67 simpa [W, hxn.symm, mul_assoc] using hnW
68 exact this hhH
70end
72section
74variable {G : Type u} [Group G]
76/-- If the intersection of a family of subgroups is trivial, every nonidentity element is omitted
78theorem exists_not_mem_of_iInf_eq_bot {ι : Type v} (U : ι → Subgroup G)
79 (hU : iInf U = (⊥ : Subgroup G)) {x : G} (hx : x ≠ 1) :
80 ∃ i : ι, x ∉ U i := by
81 by_contra h
82 have hxall : ∀ i : ι, x ∈ U i := by
83 intro i
84 by_contra hxi
85 exact h ⟨i, hxi⟩
86 have hxinf : x ∈ iInf U := by
87 simpa [Subgroup.mem_iInf] using hxall
88 have hxbot : x ∈ (⊥ : Subgroup G) := by
89 simpa [hU] using hxinf
90 exact hx (by simpa using hxbot)
92/-- Distinct left cosets of a subgroup are disjoint. -/
93theorem disjoint_leftCoset_of_not_mem (U : Subgroup G) {x y : G} (hxy : x⁻¹ * y ∉ U) :
94 Disjoint {g : G | x⁻¹ * g ∈ U} {g : G | y⁻¹ * g ∈ U} := by
95 refine Set.disjoint_left.2 ?_
96 intro g hx hg
97 apply hxy
98 have hmul : (x⁻¹ * g) * (y⁻¹ * g)⁻¹ ∈ U := U.mul_mem hx (U.inv_mem hg)
99 simpa [mul_assoc] using hmul
101variable [TopologicalSpace G] [IsTopologicalGroup G]
103/-- The left coset of an open subgroup is clopen. -/
104theorem isClopen_leftCoset_openSubgroup (U : OpenSubgroup G) (x : G) :
105 IsClopen {g : G | x⁻¹ * g ∈ (U : Subgroup G)} := by
106 let f : G → G := fun g => x⁻¹ * g
107 have hf : Continuous f := continuous_const.mul continuous_id
108 refine ⟨?_, ?_⟩
109 · simpa [f] using (openSubgroup_isClosed (G := G) U).preimage hf
110 · simpa [f] using (openSubgroup_isOpen (G := G) U).preimage hf
112end
114end ProCGroups.ProC