ProCGroups/ProC/OpenNormalSubgroups/Separation.lean
1import ProCGroups.Categorical.QuotientPullbackEquivalences
2import ProCGroups.ProC.OpenNormalSubgroups.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
4import ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets
5import ProCGroups.GroupTheory.CentralizerNormalizerCommensurator
6import ProCGroups.Profinite.Basic
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/Separation.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Pro-C groups and open normal quotients
19Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
20-/
22open scoped Topology
24namespace ProCGroups
26namespace IsProfiniteGroup
28universe u
30/-- Membership in a closed subset of a profinite group can be tested on all open-normal
31quotients. -/
33 {G : Type u} [Group G] [TopologicalSpace G]
34 (hG : IsProfiniteGroup G) {S : Set G} (hSclosed : IsClosed S) {x : G} :
35 x ∈ S ↔
36 ∀ U : OpenNormalSubgroup G,
37 ∃ y ∈ S, QuotientGroup.mk' (U : Subgroup G) y =
38 QuotientGroup.mk' (U : Subgroup G) x := by
39 letI : IsTopologicalGroup G := hG.isTopologicalGroup
40 letI : CompactSpace G := hG.compactSpace
41 letI : T2Space G := hG.t2Space
42 letI : TotallyDisconnectedSpace G := hG.totallyDisconnectedSpace
43 constructor
44 · intro hx U
45 exact ⟨x, hx, rfl⟩
46 · intro hx
47 by_contra hxS
48 let A : Set G := (fun y : G => y⁻¹ * x) '' S
49 have hAclosed : IsClosed A := by
50 exact (hSclosed.isCompact.image (continuous_inv.mul continuous_const)).isClosed
51 have h1A : (1 : G) ∉ A := by
52 rintro ⟨y, hyS, hyx⟩
53 have hxy : x = y := by
54 have h := congrArg (fun z : G => y * z) hyx
55 simpa [mul_assoc] using h
56 exact hxS (by simpa [hxy] using hyS)
57 have hAcomplOpen : IsOpen (Aᶜ) := hAclosed.isOpen_compl
58 have h1Acompl : (1 : G) ∈ Aᶜ := h1A
59 rcases ProC.exists_openNormalSubgroup_sub_open_nhds_of_one
60 (G := G) hAcomplOpen h1Acompl with ⟨U, hUA⟩
61 rcases hx U with ⟨y, hyS, hyquot⟩
62 have hyU : y⁻¹ * x ∈ (U : Subgroup G) :=
63 QuotientGroup.eq.1 hyquot
64 have hyA : y⁻¹ * x ∈ A := ⟨y, hyS, rfl⟩
65 exact hUA hyU hyA
69end ProCGroups
71namespace ProCGroups.ProC
73universe u v
75variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
77namespace OpenNormalSubgroup
79/-- Open-normal finite quotient projections separate points in a profinite group. -/
80theorem eq_of_forall_quotientProj_eq (hG : IsProfiniteGroup G) {x y : G}
81 (hxy : ∀ U : OpenNormalSubgroup G, quotientProj U x = quotientProj U y) :
82 x = y := by
83 by_contra hne
84 have hdiff : x⁻¹ * y ≠ 1 := by
85 intro h
86 exact hne (inv_mul_eq_one.mp h)
87 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
88 letI : T2Space G := IsProfiniteGroup.t2Space hG
89 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
90 let W : Set G := ({x⁻¹ * y} : Set G)ᶜ
91 have hW : IsOpen W := by
92 simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
93 have h1W : (1 : G) ∈ W := by
94 simpa [W] using hdiff.symm
95 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
96 have hmem : x⁻¹ * y ∈ (U : Subgroup G) := by
97 exact QuotientGroup.eq.1 (hxy U)
98 exact hdiff <| by
99 have hxW : x⁻¹ * y ∈ W := hUW hmem
100 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
102end OpenNormalSubgroup
104/-- If the image of `y` modulo an open normal subgroup lies in the image of `H`, then
105`y` lies in `H ⊔ U`. -/
107 {Q : Type u} [TopologicalSpace Q] [Group Q]
108 (H : Subgroup Q) (U : OpenNormalSubgroup Q)
109 {y : Q}
110 (hy :
111 QuotientGroup.mk' (U : Subgroup Q) y ∈
112 H.map (QuotientGroup.mk' (U : Subgroup Q))) :
113 y ∈ H ⊔ (U : Subgroup Q) := by
114 rcases hy with ⟨h, hh, hhy⟩
115 have hU : h⁻¹ * y ∈ (U : Subgroup Q) := by
116 have hq : QuotientGroup.mk' (U : Subgroup Q) (h⁻¹ * y) = 1 := by
117 calc
118 QuotientGroup.mk' (U : Subgroup Q) (h⁻¹ * y)
119 = (QuotientGroup.mk' (U : Subgroup Q) h)⁻¹ *
120 QuotientGroup.mk' (U : Subgroup Q) y := by
121 simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_mul,
122 QuotientGroup.mk_inv]
123 _ = (QuotientGroup.mk' (U : Subgroup Q) h)⁻¹ *
124 QuotientGroup.mk' (U : Subgroup Q) h := by rw [← hhy]
125 _ = 1 := by simp only [QuotientGroup.mk'_apply, inv_mul_cancel]
126 exact (QuotientGroup.eq_one_iff (N := (U : Subgroup Q)) (h⁻¹ * y)).1 hq
127 exact
128 (Subgroup.mem_sup_of_normal_right (s := H) (t := (U : Subgroup Q))).2
129 ⟨h, hh, h⁻¹ * y, hU, by simp only [mul_inv_cancel_left]⟩
131/-- Closed-subgroup membership can be checked after adjoining every open normal subgroup. -/
133 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
134 [CompactSpace Q] [TotallyDisconnectedSpace Q]
135 (H : ClosedSubgroup Q) {y : Q}
136 (hy : ∀ U : OpenNormalSubgroup Q,
137 y ∈ (H : Subgroup Q) ⊔ (U : Subgroup Q)) :
138 y ∈ (H : Subgroup Q) := by
139 have hEq := closedSubgroup_eq_sInf_open (G := Q) H
140 rw [hEq]
141 rw [Subgroup.mem_sInf]
142 intro K hK
143 let Kopen : OpenSubgroup Q := ⟨K, hK.1⟩
144 let U : OpenNormalSubgroup Q := OpenNormalSubgroup.normalCore Kopen
145 have hyU := hy U
146 have hsup_le : (H : Subgroup Q) ⊔ (U : Subgroup Q) ≤ K := by
147 refine sup_le hK.2 ?_
148 exact OpenNormalSubgroup.normalCore_le Kopen
149 exact hsup_le hyU
151/-- Intersection of two open normal subgroups. -/
153 {Q : Type u} [TopologicalSpace Q] [Group Q]
154 (U V : OpenNormalSubgroup Q) : OpenNormalSubgroup Q where
155 toOpenSubgroup :=
156 { toSubgroup := (U : Subgroup Q) ⊓ (V : Subgroup Q)
157 isOpen' :=
158 (ProCGroups.openNormalSubgroup_isOpen (G := Q) U).inter
159 (ProCGroups.openNormalSubgroup_isOpen (G := Q) V) }
160 isNormal' := by
161 change ((U : Subgroup Q) ⊓ (V : Subgroup Q)).Normal
162 infer_instance
164/-- Cofinal separation from a closed subgroup by open normal subgroups. -/
166 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
167 [CompactSpace Q] [TotallyDisconnectedSpace Q]
168 (H : ClosedSubgroup Q) {x : Q} (hx : x ∉ (H : Subgroup Q))
169 (U : OpenNormalSubgroup Q) :
170 ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
171 x ∉ (H : Subgroup Q) ⊔ (W : Subgroup Q) := by
172 classical
173 have hEq := closedSubgroup_eq_sInf_open (G := Q) H
174 have hxInf :
175 x ∉ sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ (H : Subgroup Q) ≤ N} := by
176 simpa [← hEq] using hx
177 rw [Subgroup.mem_sInf] at hxInf
178 push_neg at hxInf
179 rcases hxInf with ⟨N, hN, hxN⟩
180 let Nopen : OpenSubgroup Q := ⟨N, hN.1⟩
181 let Ncore : OpenNormalSubgroup Q := OpenNormalSubgroup.normalCore Nopen
182 let W : OpenNormalSubgroup Q := openNormalSubgroup_inf Ncore U
183 refine ⟨W, ?_, ?_⟩
184 · intro y hy
185 exact hy.2
186 · intro hxSup
187 have hsup_le_N : (H : Subgroup Q) ⊔ (W : Subgroup Q) ≤ N := by
188 refine sup_le hN.2 ?_
189 intro y hy
190 exact OpenNormalSubgroup.normalCore_le Nopen hy.1
191 exact hxN (hsup_le_N hxSup)
193/-- The open normal subgroup `K ⊔ U`, where `K` is normal and `U` is open normal. -/
195 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
196 (K : Subgroup Q) [K.Normal] (U : OpenNormalSubgroup Q) :
197 OpenNormalSubgroup Q where
198 toOpenSubgroup :=
199 { toSubgroup := K ⊔ (U : Subgroup Q)
200 isOpen' :=
201 Subgroup.isOpen_of_openSubgroup (K ⊔ (U : Subgroup Q))
202 (show (U : Subgroup Q) ≤ K ⊔ (U : Subgroup Q) from le_sup_right) }
203 isNormal' := by
204 change (K ⊔ (U : Subgroup Q)).Normal
205 infer_instance
207/-- Build the cofinal quotient condition from a separation statement and finite-stage cyclic
208containment on quotients where `x^n` remains nontrivial modulo `K`. -/
210 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
211 [CompactSpace Q] [TotallyDisconnectedSpace Q]
212 (x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
213 (hnotK : x ^ n ∉ K)
214 (hfinite : ∀ W : OpenNormalSubgroup Q,
215 x ^ n ∉ K ⊔ (W : Subgroup Q) →
216 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
217 ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
218 QuotientGroup.mk' (V : Subgroup Q) y ∈
219 ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
220 ClosedSubgroup Q) :
221 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
222 ∀ U : OpenNormalSubgroup Q,
223 ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
224 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
225 ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
226 QuotientGroup.mk' (V : Subgroup Q) y ∈
227 ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
228 ClosedSubgroup Q) :
229 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q)) := by
230 intro U
231 let Kclosed : ClosedSubgroup Q := ⟨K, hKclosed⟩
232 rcases
234 (H := Kclosed) hnotK U with
235 ⟨W, hWU, hnotW⟩
236 refine ⟨W, hWU, ?_⟩
237 change x ^ n ∉ K ⊔ (W : Subgroup Q) at hnotW
238 exact hfinite W hnotW
240/-- Cofinal image criterion for bounding a centralizer by a cyclic subgroup joined with a closed
241normal subgroup. -/
243 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
244 [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
245 (x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
246 (himage : ∀ U : OpenNormalSubgroup Q,
247 ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
248 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
249 ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
250 QuotientGroup.mk' (V : Subgroup Q) y ∈
251 ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
252 ClosedSubgroup Q) :
253 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
254 ProCGroups.GroupTheory.centralizerOf (x ^ n) ≤
255 ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
256 ClosedSubgroup Q) :
257 Subgroup Q) ⊔ K := by
258 let L : Subgroup Q :=
259 ((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
260 ClosedSubgroup Q) : Subgroup Q)
261 let H : ClosedSubgroup Q :=
262 ⟨L ⊔ K,
264 (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q)).isClosed'
265 hKclosed⟩
266 intro y hy
268 intro U
269 rcases himage U with ⟨W, hWU, hWimage⟩
270 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
271 have hyVL :
272 QuotientGroup.mk' (V : Subgroup Q) y ∈
273 L.map (QuotientGroup.mk' (V : Subgroup Q)) := by
274 simpa [L, V] using hWimage y hy
275 have hySupV : y ∈ L ⊔ (V : Subgroup Q) :=
276 mem_sup_of_quotient_mk_mem_map L V hyVL
277 have hle : L ⊔ (V : Subgroup Q) ≤ (H : Subgroup Q) ⊔ (U : Subgroup Q) := by
278 change L ⊔ (K ⊔ (W : Subgroup Q)) ≤ (L ⊔ K) ⊔ (U : Subgroup Q)
279 refine sup_le ?_ ?_
280 · exact (show L ≤ L ⊔ K from le_sup_left).trans le_sup_left
281 · refine sup_le ?_ ?_
282 · exact (show K ≤ L ⊔ K from le_sup_right).trans le_sup_left
283 · exact hWU.trans le_sup_right
284 exact hle hySupV
286/-- Continuous homomorphisms into a profinite group are equal if they agree after every
289 {A : Type u} [Group A] [TopologicalSpace A]
290 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
291 (hH : IsProfiniteGroup H) {φ ψ : A →ₜ* H}
292 (h : ∀ U : OpenNormalSubgroup H,
293 (OpenNormalSubgroup.quotientProj U).comp φ =
294 (OpenNormalSubgroup.quotientProj U).comp ψ) :
295 φ = ψ := by
296 ext x
297 exact OpenNormalSubgroup.eq_of_forall_quotientProj_eq (G := H) hH
298 (fun U => by
299 have hU := congrArg (fun f : A →ₜ* H ⧸ (U : Subgroup H) => f x) (h U)
300 simpa using hU)
302end ProCGroups.ProC