Yamaguchi Lean 4 Library
Source: ProCGroups.ProC.OpenNormalSubgroups.Separation
ProCGroups/ProC/OpenNormalSubgroups/Separation/Source

Source: ProCGroups.ProC.OpenNormalSubgroups.Separation

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/-!
9# Separation by open normal quotients
11This file detects equality and closed-subgroup membership in all open normal quotients. It also
12develops refinements avoiding a chosen coset, cyclic-containment consequences, and extensionality
13of continuous homomorphisms from their finite quotient maps.
14-/
16open scoped Topology
18namespace ProCGroups
20universe u
22/--
23Membership in a closed subset of a profinite group can be tested on all open-normal quotients.
24-/
25theorem mem_closed_iff_forall_openNormal_quotient
26 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27 [CompactSpace G] [TotallyDisconnectedSpace G]
28 {S : Set G} (hSclosed : IsClosed S) {x : G} :
29 x ∈ S ↔
30 ∀ U : OpenNormalSubgroup G,
31 ∃ y ∈ S, QuotientGroup.mk' (U : Subgroup G) y =
32 QuotientGroup.mk' (U : Subgroup G) x := by
33 constructor
34 · intro hx U
35 exact ⟨x, hx, rfl⟩
36 · intro hx
37 by_contra hxS
38 let A : Set G := (fun y : G => y⁻¹ * x) '' S
39 have hAclosed : IsClosed A := by
40 exact (hSclosed.isCompact.image (continuous_inv.mul continuous_const)).isClosed
41 have h1A : (1 : G) ∉ A := by
42 rintro ⟨y, hyS, hyx⟩
43 have hxy : x = y := by
44 have h := congrArg (fun z : G => y * z) hyx
45 simpa [mul_assoc] using h
46 exact hxS (by simpa [hxy] using hyS)
47 have hAcomplOpen : IsOpen (Aᶜ) := hAclosed.isOpen_compl
48 have h1Acompl : (1 : G) ∈ Aᶜ := h1A
49 rcases ProC.exists_openNormalSubgroup_sub_open_nhds_of_one
50 (G := G) hAcomplOpen h1Acompl with ⟨U, hUA⟩
51 rcases hx U with ⟨y, hyS, hyquot⟩
52 have hyU : y⁻¹ * x ∈ (U : Subgroup G) :=
53 QuotientGroup.eq.1 hyquot
54 have hyA : y⁻¹ * x ∈ A := ⟨y, hyS, rfl⟩
55 exact hUA hyU hyA
57end ProCGroups
59namespace ProCGroups.ProC
61universe u v
63variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
65namespace OpenNormalSubgroup
67/-- Two elements of a profinite group are equal if all their open-normal quotient projections
68agree. -/
69theorem eq_of_forall_quotientProj_eq [CompactSpace G] [T2Space G]
70 [TotallyDisconnectedSpace G] {x y : G}
71 (hxy : ∀ U : OpenNormalSubgroup G, quotientProj U x = quotientProj U y) :
72 x = y := by
73 by_contra hne
74 have hdiff : x⁻¹ * y ≠ 1 := by
75 intro h
76 exact hne (inv_mul_eq_one.mp h)
77 let W : Set G := ({x⁻¹ * y} : Set G)ᶜ
78 have hW : IsOpen W := by
79 simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
80 have h1W : (1 : G) ∈ W := by
81 simpa [W] using hdiff.symm
82 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
83 have hmem : x⁻¹ * y ∈ (U : Subgroup G) := by
84 exact QuotientGroup.eq.1 (hxy U)
85 exact hdiff <| by
86 have hxW : x⁻¹ * y ∈ W := hUW hmem
87 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
89end OpenNormalSubgroup
91/--
92If the image of y modulo an open normal subgroup lies in the image of H, then y lies in H
93\(\sqcup\) U.
94-/
95theorem mem_sup_of_quotient_mk_mem_map
96 {Q : Type u} [TopologicalSpace Q] [Group Q]
97 (H : Subgroup Q) (U : OpenNormalSubgroup Q)
98 {y : Q}
99 (hy :
100 QuotientGroup.mk' (U : Subgroup Q) y ∈
101 H.map (QuotientGroup.mk' (U : Subgroup Q))) :
102 y ∈ H ⊔ (U : Subgroup Q) := by
103 rcases hy with ⟨h, hh, hhy⟩
104 have hU : h⁻¹ * y ∈ (U : Subgroup Q) := by
105 have hq : QuotientGroup.mk' (U : Subgroup Q) (h⁻¹ * y) = 1 := by
106 calc
107 QuotientGroup.mk' (U : Subgroup Q) (h⁻¹ * y)
108 = (QuotientGroup.mk' (U : Subgroup Q) h)⁻¹ *
109 QuotientGroup.mk' (U : Subgroup Q) y := by
110 simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_mul,
111 QuotientGroup.mk_inv]
112 _ = (QuotientGroup.mk' (U : Subgroup Q) h)⁻¹ *
113 QuotientGroup.mk' (U : Subgroup Q) h := by rw [← hhy]
114 _ = 1 := by simp only [QuotientGroup.mk'_apply, inv_mul_cancel]
115 exact (QuotientGroup.eq_one_iff (N := (U : Subgroup Q)) (h⁻¹ * y)).1 hq
116 exact
117 (Subgroup.mem_sup_of_normal_right (s := H) (t := (U : Subgroup Q))).2
118 ⟨h, hh, h⁻¹ * y, hU, by simp only [mul_inv_cancel_left]⟩
120/-- Closed-subgroup membership can be checked after adjoining every open normal subgroup. -/
121theorem mem_closedSubgroup_of_forall_openNormal_sup
122 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
123 [CompactSpace Q] [TotallyDisconnectedSpace Q]
124 (H : ClosedSubgroup Q) {y : Q}
125 (hy : ∀ U : OpenNormalSubgroup Q,
126 y ∈ (H : Subgroup Q) ⊔ (U : Subgroup Q)) :
127 y ∈ (H : Subgroup Q) := by
128 have hEq := closedSubgroup_eq_sInf_open (G := Q) H
129 rw [hEq]
130 rw [Subgroup.mem_sInf]
131 intro K hK
132 let Kopen : OpenSubgroup Q := ⟨K, hK.1⟩
133 let U : OpenNormalSubgroup Q := OpenNormalSubgroup.normalCore Kopen
134 have hyU := hy U
135 have hsup_le : (H : Subgroup Q) ⊔ (U : Subgroup Q) ≤ K := by
136 refine sup_le hK.2 ?_
137 exact OpenNormalSubgroup.normalCore_le Kopen
138 exact hsup_le hyU
140/-- The intersection of two open normal subgroups is open and normal. -/
141def openNormalSubgroup_inf
142 {Q : Type u} [TopologicalSpace Q] [Group Q]
143 (U V : OpenNormalSubgroup Q) : OpenNormalSubgroup Q where
144 toOpenSubgroup :=
145 { toSubgroup := (U : Subgroup Q) ⊓ (V : Subgroup Q)
146 isOpen' :=
149 isNormal' := by
150 change ((U : Subgroup Q) ⊓ (V : Subgroup Q)).Normal
151 infer_instance
153/-- Cofinal separation from a closed subgroup by open normal subgroups. -/
154theorem exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup
155 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
156 [CompactSpace Q] [TotallyDisconnectedSpace Q]
157 (H : ClosedSubgroup Q) {x : Q} (hx : x ∉ (H : Subgroup Q))
158 (U : OpenNormalSubgroup Q) :
159 ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
160 x ∉ (H : Subgroup Q) ⊔ (W : Subgroup Q) := by
161 classical
162 have hEq := closedSubgroup_eq_sInf_open (G := Q) H
163 have hxInf :
164 x ∉ sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ (H : Subgroup Q) ≤ N} := by
165 simpa [← hEq] using hx
166 rw [Subgroup.mem_sInf] at hxInf
167 push Not at hxInf
168 rcases hxInf with ⟨N, hN, hxN⟩
169 let Nopen : OpenSubgroup Q := ⟨N, hN.1⟩
170 let Ncore : OpenNormalSubgroup Q := OpenNormalSubgroup.normalCore Nopen
171 let W : OpenNormalSubgroup Q := openNormalSubgroup_inf Ncore U
172 refine ⟨W, ?_, ?_⟩
173 · intro y hy
174 exact hy.2
175 · intro hxSup
176 have hsup_le_N : (H : Subgroup Q) ⊔ (W : Subgroup Q) ≤ N := by
177 refine sup_le hN.2 ?_
178 intro y hy
179 exact OpenNormalSubgroup.normalCore_le Nopen hy.1
180 exact hxN (hsup_le_N hxSup)
182/-- The open normal subgroup K \(\sqcup\) U, where K is normal and U is open normal. -/
183def openNormalSubgroup_sup_normal
184 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
185 (K : Subgroup Q) [K.Normal] (U : OpenNormalSubgroup Q) :
186 OpenNormalSubgroup Q where
187 toOpenSubgroup :=
188 { toSubgroup := K ⊔ (U : Subgroup Q)
189 isOpen' :=
190 Subgroup.isOpen_of_openSubgroup (K ⊔ (U : Subgroup Q))
191 (show (U : Subgroup Q) ≤ K ⊔ (U : Subgroup Q) from le_sup_right) }
192 isNormal' := by
193 change (K ⊔ (U : Subgroup Q)).Normal
194 infer_instance
196/--
197The cofinal quotient condition obtained from a separation statement and finite-stage cyclic
198containment on quotients where \(x^n\) remains nontrivial modulo \(K\).
199-/
200theorem cofinal_openNormal_cyclic_containment_of_finite_lift
201 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
202 [CompactSpace Q] [TotallyDisconnectedSpace Q]
203 (x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
204 (hnotK : x ^ n ∉ K)
205 (hfinite : ∀ W : OpenNormalSubgroup Q,
206 x ^ n ∉ K ⊔ (W : Subgroup Q) →
207 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
208 ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
209 QuotientGroup.mk' (V : Subgroup Q) y ∈
211 ClosedSubgroup Q) :
212 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
213 ∀ U : OpenNormalSubgroup Q,
214 ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
215 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
216 ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
217 QuotientGroup.mk' (V : Subgroup Q) y ∈
219 ClosedSubgroup Q) :
220 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q)) := by
221 intro U
222 let Kclosed : ClosedSubgroup Q := ⟨K, hKclosed⟩
223 rcases
224 exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup
225 (H := Kclosed) hnotK U with
226 ⟨W, hWU, hnotW⟩
227 refine ⟨W, hWU, ?_⟩
228 change x ^ n ∉ K ⊔ (W : Subgroup Q) at hnotW
229 exact hfinite W hnotW
231/--
232Cofinal image criterion for bounding a centralizer by a cyclic subgroup joined with a closed
233normal subgroup.
234-/
235theorem centralizerOf_zpow_le_cyclic_join_closedNormal_of_cofinal_openNormal_image
236 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
237 [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
238 (x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
239 (himage : ∀ U : OpenNormalSubgroup Q,
240 ∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
241 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
242 ∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
243 QuotientGroup.mk' (V : Subgroup Q) y ∈
245 ClosedSubgroup Q) :
246 Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
249 ClosedSubgroup Q) :
250 Subgroup Q) ⊔ K := by
251 let L : Subgroup Q :=
253 ClosedSubgroup Q) : Subgroup Q)
254 let H : ClosedSubgroup Q :=
255 ⟨L ⊔ K,
256 Subgroup.isClosed_sup_of_normal L K
257 (ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q)).isClosed'
258 hKclosed⟩
259 intro y hy
260 apply mem_closedSubgroup_of_forall_openNormal_sup H
261 intro U
262 rcases himage U with ⟨W, hWU, hWimage⟩
263 let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
264 have hyVL :
265 QuotientGroup.mk' (V : Subgroup Q) y ∈
266 L.map (QuotientGroup.mk' (V : Subgroup Q)) := by
267 simpa [L, V] using hWimage y hy
268 have hySupV : y ∈ L ⊔ (V : Subgroup Q) :=
269 mem_sup_of_quotient_mk_mem_map L V hyVL
270 have hle : L ⊔ (V : Subgroup Q) ≤ (H : Subgroup Q) ⊔ (U : Subgroup Q) := by
271 change L ⊔ (K ⊔ (W : Subgroup Q)) ≤ (L ⊔ K) ⊔ (U : Subgroup Q)
272 refine sup_le ?_ ?_
273 · exact (show L ≤ L ⊔ K from le_sup_left).trans le_sup_left
274 · refine sup_le ?_ ?_
275 · exact (show K ≤ L ⊔ K from le_sup_right).trans le_sup_left
276 · exact hWU.trans le_sup_right
277 exact hle hySupV
279/--
280Continuous homomorphisms into a profinite group are equal if they agree after every open-normal
281finite quotient of the target.
282-/
283theorem continuousMonoidHom_ext_openNormalQuotients
284 {A : Type u} [Group A] [TopologicalSpace A]
285 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
286 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
287 {φ ψ : A →ₜ* H}
288 (h : ∀ U : OpenNormalSubgroup H,
289 (OpenNormalSubgroup.quotientProj U).comp φ =
290 (OpenNormalSubgroup.quotientProj U).comp ψ) :
291 φ = ψ := by
292 ext x
293 exact OpenNormalSubgroup.eq_of_forall_quotientProj_eq (G := H)
294 (fun U => by
295 have hU := congrArg (fun f : A →ₜ* H ⧸ (U : Subgroup H) => f x) (h U)
296 simpa using hU)
298end ProCGroups.ProC