Yamaguchi Lean 4 Library
ProCGroups/Generation/Convergence.lean
ProCGroups/Generation/Convergence/Source

ProCGroups/Generation/Convergence.lean

1import Mathlib.Topology.Compactification.OnePoint.Basic
2import ProCGroups.Generation.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
4import ProCGroups.Profinite.Basic
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/Generation/Convergence.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Topological generation
17Develops topological generation, generating families, convergence-to-one criteria, quotient generation, and profinite generation lemmas.
18-/
20open Set
21open scoped Topology Pointwise
23namespace ProCGroups.Generation
25universe u v
27open ProCGroups.ProC
29variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31/-- A continuous map between topological groups that sends `1` to `1` carries convergent sets to
32convergent sets, provided the source is profinite. -/
33theorem ConvergesToOne.image_of_continuous_pointed
34 {H : Type v} [Group H] [TopologicalSpace H]
35 (hG : IsProfiniteGroup G) {f : G → H} (hf : Continuous f) (hf1 : f 1 = 1)
36 {X : Set G} (hX : ConvergesToOne (G := G) X) :
37 ConvergesToOne (G := H) (f '' X) := by
38 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
39 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
40 intro U
41 have hpre : IsOpen (f ⁻¹' (U : Set H)) :=
42 (openSubgroup_isOpen (G := H) U).preimage hf
43 have h1pre : (1 : G) ∈ f ⁻¹' (U : Set H) := by
44 simp only [mem_preimage, hf1, SetLike.mem_coe, one_mem]
45 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hpre h1pre with ⟨V, hVU⟩
46 have hsubset : (f '' X) \ (U : Set H) ⊆ f '' (X \ (V : Set G)) := by
47 intro y hy
48 rcases hy with ⟨hyX, hyU⟩
49 rcases hyX with ⟨x, hxX, rfl⟩
50 refine ⟨x, ⟨hxX, ?_⟩, rfl⟩
51 intro hxV
52 exact hyU (hVU hxV)
53 exact (hX V.toOpenSubgroup).image f |>.subset hsubset
55omit [IsTopologicalGroup G] in
56/-- Passing to a subset preserves convergence to `1`. -/
57theorem ConvergesToOne.mono {X Y : Set G}
58 (hX : ConvergesToOne (G := G) X) (hYX : Y ⊆ X) :
59 ConvergesToOne (G := G) Y := by
60 intro U
61 exact (hX U).subset (by
62 intro y hy
63 exact ⟨hYX hy.1, hy.2⟩)
65omit [IsTopologicalGroup G] in
66/-- Finite enlargements preserve convergence to `1`. -/
67theorem ConvergesToOne.union_finite {X F : Set G}
68 (hX : ConvergesToOne (G := G) X) (hF : F.Finite) :
69 ConvergesToOne (G := G) (X ∪ F) := by
70 intro U
71 have h1 : (X \ (U : Set G)).Finite := hX U
72 have h2 : (F \ (U : Set G)).Finite := hF.subset (by
73 intro y hy
74 exact hy.1)
75 have hsubset : (X ∪ F) \ (U : Set G) ⊆ (X \ (U : Set G)) ∪ (F \ (U : Set G)) := by
76 intro y hy
77 rcases hy with ⟨hyXF, hyU⟩
78 rcases hyXF with hyX | hyF
79 · exact Or.inl ⟨hyX, hyU⟩
80 · exact Or.inr ⟨hyF, hyU⟩
81 exact (h1.union h2).subset hsubset
83omit [IsTopologicalGroup G] in
84/-- Finite modifications do not change convergence to `1`. -/
85theorem ConvergesToOne.union_finite_iff {X F : Set G}
86 (hF : F.Finite) :
87 ConvergesToOne (G := G) (X ∪ F) ↔ ConvergesToOne (G := G) X := by
88 constructor
89 · intro h
90 exact ConvergesToOne.mono (G := G) h (by
91 intro x hx
92 exact Or.inl hx)
93 · intro h
94 exact ConvergesToOne.union_finite (G := G) h hF
96omit [IsTopologicalGroup G] in
97/-- Single-point insertions do not change convergence to `1`. -/
98theorem ConvergesToOne.insert_iff {X : Set G} {x : G} :
99 ConvergesToOne (G := G) (Set.insert x X) ↔ ConvergesToOne (G := G) X := by
100 have hEq : Set.insert x X = X ∪ ({x} : Set G) := by
101 ext y
102 constructor
103 · intro hy
104 rcases Set.mem_insert_iff.mp hy with rfl | hyX
105 · exact Or.inr (by simp only [mem_singleton_iff])
106 · exact Or.inl hyX
107 · intro hy
108 rcases hy with hyX | hyx
109 · exact Set.mem_insert_iff.mpr (Or.inr hyX)
110 · exact Set.mem_insert_iff.mpr (Or.inl (by simpa using hyx))
111 rw [hEq]
112 exact ConvergesToOne.union_finite_iff (G := G) (X := X) (F := ({x} : Set G))
113 (Set.finite_singleton x)
115omit [IsTopologicalGroup G] in
116/-- Union with `{1}` does not affect convergence to `1`. -/
117theorem ConvergesToOne.union_one_iff {X : Set G} :
118 ConvergesToOne (G := G) (X ∪ ({1} : Set G)) ↔ ConvergesToOne (G := G) X := by
119 exact ConvergesToOne.union_finite_iff (G := G) (X := X) (F := ({1} : Set G))
120 (Set.finite_singleton 1)
122/-- A set converging to `1` is discrete away from `1`, and if it is infinite its closure is
123obtained by adjoining the unique possible limit point `1`. -/
125 (hX : ConvergesToOne (G := G) X) :
126 IsDiscrete (X \ {1}) ∧
127 (Set.Infinite X → closure X = X ∪ ({1} : Set G)) := by
128 letI : T2Space G := IsProfiniteGroup.t2Space hG
129 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
130 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
131 refine ⟨?_, ?_⟩
132 · rw [isDiscrete_iff_forall_exists_isOpen]
133 intro y hy
134 have hy1 : y ≠ 1 := by simpa using hy.2
135 let W : Set G := ({y} : Set G)ᶜ
136 have hWopen : IsOpen W := isClosed_singleton.isOpen_compl
137 have h1W : (1 : G) ∈ W := by simpa [W, eq_comm] using hy1
138 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨U, hUW⟩
139 have hyU : y ∉ (U : Set G) := by
140 intro hyU
141 have hyW : y ∈ W := hUW hyU
142 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hyW
143 let V : Set G := (fun z : G => y⁻¹ * z) ⁻¹' (U : Set G)
144 have hVopen : IsOpen V := by
145 exact (openNormalSubgroup_isOpen (G := G) U).preimage
146 (continuous_const.mul continuous_id)
147 have hyV : y ∈ V := by
148 simp only [mem_preimage, inv_mul_cancel, SetLike.mem_coe, one_mem, V]
149 have hsubset : V ∩ (X \ ({1} : Set G)) ⊆ X \ (U : Set G) := by
150 intro z hz
151 rcases hz with ⟨hzV, hzX⟩
152 refine ⟨hzX.1, ?_⟩
153 intro hzU
154 have hmem : z * (y⁻¹ * z)⁻¹ ∈ (U : Subgroup G) := U.mul_mem hzU (U.inv_mem hzV)
155 have : y ∈ (U : Subgroup G) := by
156 simpa [mul_assoc] using hmem
157 exact hyU this
158 have hfinite : (V ∩ (X \ ({1} : Set G))).Finite := by
159 exact (hX U.toOpenSubgroup).subset hsubset
160 rcases (isDiscrete_iff_forall_exists_isOpen.mp hfinite.isDiscrete) y ⟨hyV, hy⟩ with
161 ⟨V', hV'open, hV'⟩
162 refine ⟨V' ∩ V, hV'open.inter hVopen, ?_⟩
163 simpa [Set.inter_assoc, Set.inter_left_comm, Set.inter_comm] using hV'
164 · intro hXinfinite
165 apply subset_antisymm
166 · intro y hycl
167 by_cases hy1 : y = 1
168 · simp only [union_singleton, hy1, mem_insert_iff, true_or]
169 · by_cases hyX : y ∈ X
170 · simp only [union_singleton, mem_insert_iff, hy1, hyX, or_true]
171 · let W : Set G := ({y} : Set G)ᶜ
172 have hWopen : IsOpen W := isClosed_singleton.isOpen_compl
173 have h1W : (1 : G) ∈ W := by simpa [W, eq_comm] using hy1
174 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with
175 ⟨U, hUW⟩
176 have hyU : y ∉ (U : Set G) := by
177 intro hyU
178 have hyW : y ∈ W := hUW hyU
179 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hyW
180 let V : Set G := (fun z : G => y⁻¹ * z) ⁻¹' (U : Set G)
181 have hVopen : IsOpen V := by
182 exact (openNormalSubgroup_isOpen (G := G) U).preimage
183 (continuous_const.mul continuous_id)
184 have hyV : y ∈ V := by
185 simp only [mem_preimage, inv_mul_cancel, SetLike.mem_coe, one_mem, V]
186 have hsubset : V ∩ X ⊆ X \ (U : Set G) := by
187 intro z hz
188 rcases hz with ⟨hzV, hzX⟩
189 refine ⟨hzX, ?_⟩
190 intro hzU
191 have hmem : z * (y⁻¹ * z)⁻¹ ∈ (U : Subgroup G) := U.mul_mem hzU (U.inv_mem hzV)
192 have : y ∈ (U : Subgroup G) := by
193 simpa [mul_assoc] using hmem
194 exact hyU this
195 have hfinite : (V ∩ X).Finite := by
196 exact (hX U.toOpenSubgroup).subset hsubset
197 have hclosed : IsClosed (V ∩ X) := hfinite.isClosed
198 have hyVX : y ∉ V ∩ X := by
199 simp only [mem_inter_iff, hyV, hyX, and_false, not_false_eq_true]
200 have hne :=
201 (mem_closure_iff.1 hycl) (V \ (V ∩ X)) (hVopen.sdiff hclosed) ⟨hyV, hyVX⟩
202 rcases hne with ⟨z, hz⟩
203 exact False.elim (hz.1.2 ⟨hz.1.1, hz.2⟩)
204 · intro y hy
205 rcases hy with hyX | hy1
206 · exact subset_closure hyX
207 · subst hy1
208 refine mem_closure_iff.2 ?_
209 intro W hWopen h1W
210 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with
211 ⟨U, hUW⟩
212 have hproper : ¬ X ⊆ X \ (U : Set G) := by
213 intro hsub
214 have hXfinite : X.Finite := (hX U.toOpenSubgroup).subset hsub
215 exact hXinfinite hXfinite
216 rcases Set.not_subset.1 hproper with ⟨x, hxX, hxnot⟩
217 have hxU : x ∈ (U : Set G) := by
218 by_contra hxU
219 exact hxnot ⟨hxX, hxU⟩
220 exact ⟨x, hUW hxU, hxX⟩
222/-- A convergent set containing its only possible limit point `1` is closed. -/
223theorem ConvergesToOne.isClosed_of_one_mem (hG : IsProfiniteGroup G) {X : Set G}
224 (hX : ConvergesToOne (G := G) X) (h1 : (1 : G) ∈ X) :
225 IsClosed X := by
226 letI : T2Space G := IsProfiniteGroup.t2Space hG
227 rcases closure_generatorsConvergingToOne (G := G) hG hX with ⟨_, hclosure⟩
228 by_cases hfinite : X.Finite
229 · exact hfinite.isClosed
230 · have hEq : closure X = X := by
231 calc
232 closure X = X ∪ ({1} : Set G) := by
233 exact hclosure hfinite
234 _ = X := by simp only [union_singleton, h1, insert_eq_of_mem]
235 exact closure_eq_iff_isClosed.mp hEq
237/-- If `X` is infinite, converges to `1`, and does not contain `1`, then `closure X` is
238homeomorphic to the one-point compactification of the discrete space `X`. -/
240 (hG : IsProfiniteGroup G) {X : Set G}
241 (hX : ConvergesToOne (G := G) X) (hXinfinite : X.Infinite) (h1X : (1 : G) ∉ X) :
242 OnePoint X ≃ₜ closure X := by
243 classical
244 letI : T2Space G := IsProfiniteGroup.t2Space hG
245 rcases closure_generatorsConvergingToOne (G := G) hG hX with ⟨hdisc, hclosure⟩
246 have hdiff : X \ ({1} : Set G) = X := by
247 ext x
248 by_cases hx : x = 1
249 · simp only [h1X, not_false_eq_true, diff_singleton_eq_self, hx]
250 · simp only [mem_diff, mem_singleton_iff, hx, not_false_eq_true, and_true]
251 have hdiscX : IsDiscrete X := by
252 simpa [hdiff] using hdisc
253 letI : DiscreteTopology X := (isDiscrete_iff_discreteTopology).1 hdiscX
254 have h1closure : (1 : G) ∈ closure X := by
255 have : (1 : G) ∈ X ∪ ({1} : Set G) := by simp only [union_singleton, mem_insert_iff, true_or]
256 rw [hclosure hXinfinite]
257 simp only [union_singleton, mem_insert_iff, true_or]
258 let toClosure : OnePoint X → closure X
259 | OnePoint.infty => ⟨1, h1closure⟩
260 | (x : X) => ⟨x.1, subset_closure x.2⟩
261 let fromClosure : closure X → OnePoint X := fun y =>
262 if hy : (y : G) = 1 then
263 OnePoint.infty
264 else
265 OnePoint.some ⟨(y : G), by
266 have hy' : (y : G) ∈ X ∪ ({1} : Set G) := by
267 simpa [hclosure hXinfinite] using y.2
268 rcases hy' with hyX | hy1
269 · exact hyX
270 · exact False.elim (hy hy1)⟩
271 have hleft : Function.LeftInverse fromClosure toClosure := by
272 intro z
273 refine OnePoint.rec ?_ ?_ z
274 · simp only [↓reduceDIte, fromClosure, toClosure]
275 · intro x
276 have hx1 : (x : G) ≠ 1 := by
277 intro hx1
278 exact h1X (hx1 ▸ x.2)
279 simp only [hx1, ↓reduceDIte, Subtype.coe_eta, fromClosure, toClosure]
280 have hright : Function.RightInverse fromClosure toClosure := by
281 intro y
282 by_cases hy : (y : G) = 1
283 · apply Subtype.ext
284 simp only [hy, ↓reduceDIte, toClosure, fromClosure]
285 · apply Subtype.ext
286 simp only [hy, ↓reduceDIte, Subtype.coe_eta, toClosure, fromClosure]
287 let e : OnePoint X ≃ closure X :=
288 { toFun := toClosure
289 invFun := fromClosure
290 left_inv := hleft
291 right_inv := hright }
292 have hcont : Continuous e := by
293 rw [OnePoint.continuous_iff_from_discrete]
294 rw [tendsto_subtype_rng]
295 change Filter.Tendsto (fun x : X => ((toClosure (x : OnePoint X) : closure X) : G))
296 Filter.cofinite
297 (𝓝 (((toClosure OnePoint.infty : closure X) : G)))
298 change Filter.Tendsto (fun x : X => (x : G)) Filter.cofinite (𝓝 (1 : G))
299 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
300 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
301 rw [Filter.tendsto_def]
302 intro s hs
303 rcases mem_nhds_iff.mp hs with ⟨W, hWs, hWopen, h1W⟩
304 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨U, hUW⟩
305 have hfinite : (X \ (U : Set G)).Finite := hX U.toOpenSubgroup
306 have hcof : ∀ᶠ x : X in Filter.cofinite, (x : G) ∈ (U : Set G) := by
307 let f : X ↪ G := ⟨Subtype.val, Subtype.val_injective⟩
308 have hpre : {x : X | (x : G) ∉ (U : Set G)}.Finite := by
309 simpa [f, Set.preimage] using hfinite.preimage_embedding f
310 exact Filter.eventually_cofinite.2 hpre
311 exact hcof.mono fun x hx => hWs (hUW hx)
312 exact hcont.homeoOfBijectiveCompactToT2 e.bijective
314end ProCGroups.Generation