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

ProCGroups/Generation/GeneratorConvergingPairs.lean

1import ProCGroups.Generation.QuotientCriteria
2import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Generation/GeneratorConvergingPairs.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Topological generation
15Develops topological generation, generating families, convergence-to-one criteria, quotient generation, and profinite generation lemmas.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ProCGroups.Generation
23universe u v
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31/-- A partial generating set together with a closed normal subgroup modulo which it converges. -/
33 N : Subgroup G
34 normal_N : N.Normal
35 closed_N : IsClosed (N : Set G)
36 X : Set G
37 subset_compl : X ⊆ (N : Set G)ᶜ
38 convergesToOne_mod :
39 ∀ U : OpenSubgroup G, N ≤ (U : Subgroup G) → (X \ (U : Set G)).Finite
40 generates : TopologicallyGenerates (G := G) (X ∪ (N : Set G))
43 le A B := B.N ≤ A.N ∧ A.X ⊆ B.X ∧ B.X \ A.X ⊆ (A.N : Set G)
46 le_refl A := ⟨le_rfl, subset_rfl, by simp only [sdiff_self, bot_eq_empty, empty_subset]⟩
47 le_trans A B C hAB hBC := by
48 rcases hAB with ⟨hABN, hABX, hABdiff⟩
49 rcases hBC with ⟨hBCN, hBCX, hBCdiff⟩
50 refine ⟨hBCN.trans hABN, hABX.trans hBCX, ?_⟩
51 intro x hx
52 rcases hx with ⟨hxC, hxA⟩
53 by_cases hxB : x ∈ B.X
54 · exact hABdiff ⟨hxB, hxA⟩
55 · exact hABN (hBCdiff ⟨hxC, hxB⟩)
57/-- The initial generator-converging pair. -/
59 N := ⊤
60 normal_N := by infer_instance
61 closed_N := isClosed_univ
62 X := ∅
63 subset_compl := by intro x hx; simp only [mem_empty_iff_false] at hx
64 convergesToOne_mod := by
65 intro U hU
66 simp only [empty_diff, finite_empty]
67 generates := by
68 simpa [TopologicallyGenerates, Set.empty_union, Subgroup.closure_eq] using
69 (top_unique (Subgroup.le_topologicalClosure (⊤ : Subgroup G)) :
70 (⊤ : Subgroup G).topologicalClosure = ⊤)
72/-- A finite subset of a chain has an upper element from that subset. -/
73theorem finite_subset_chain_has_upper {α : Type*} [Preorder α] {c : Set α}
74 (hc : IsChain (· ≤ ·) c) :
75 ∀ s : Finset α, ↑s ⊆ c → s.Nonempty → ∃ m ∈ s, ∀ z ∈ s, z ≤ m := by
76 classical
77 intro s
78 refine Finset.induction_on s ?_ ?_
79 · intro hs hne
80 exact False.elim (hne.ne_empty rfl)
81 · intro a s ha ih hs hne
82 by_cases hsne : s.Nonempty
83 · rcases ih
84 (by
85 intro z hz
86 exact hs (by simp only [Finset.coe_insert, mem_insert_iff, hz, or_true]))
87 hsne with ⟨m, hm, hmax⟩
88 have ha' : a ∈ c := hs (by simp only [Finset.coe_insert, mem_insert_iff, SetLike.mem_coe, true_or])
89 have hm' : m ∈ c := hs (by simp only [Finset.coe_insert, mem_insert_iff, SetLike.mem_coe, hm, or_true])
90 have hcmp : a ≤ m ∨ m ≤ a := by
91 by_cases hEq : a = m
92 · exact Or.inl (hEq ▸ le_rfl)
93 · exact hc ha' hm' hEq
94 cases hcmp with
95 | inl ham =>
96 refine ⟨m, by simp only [Finset.mem_insert, hm, or_true], ?_⟩
97 intro z hz
98 rcases Finset.mem_insert.mp hz with rfl | hz'
99 · exact ham
100 · exact hmax z hz'
101 | inr hma =>
102 refine ⟨a, by simp only [Finset.mem_insert, true_or], ?_⟩
103 intro z hz
104 rcases Finset.mem_insert.mp hz with rfl | hz'
105 · exact le_rfl
106 · exact (hmax z hz').trans hma
107 · have hs0 : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hsne
108 refine ⟨a, by simp only [hs0, insert_empty_eq, Finset.mem_singleton], ?_⟩
109 intro z hz
110 have hz' : z = a := by simpa [hs0] using hz
111 subst z
112 exact le_rfl
114/-- If the infimum of the closed normal subgroups in a chain lies in an open subgroup, then one
115stage already lies in that open subgroup. -/
117 {c : Set (GeneratorConvergingPair (G := G))}
118 (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty)
119 (U : OpenSubgroup G)
120 (hInf : iInf (fun p : c => p.1.N) ≤ (U : Subgroup G)) :
121 ∃ p : c, p.1.N ≤ (U : Subgroup G) := by
122 classical
123 have hInter :
124 (⋂ p : c, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := by
125 intro x hx
126 exact hInf (by simpa [Subgroup.mem_iInf] using hx)
128 (H := fun p : c => p.1.N)
129 (hclosed := fun p => p.1.closed_N)
130 U hInter with ⟨s, hs⟩
131 by_cases hsne : s.Nonempty
132 · have hc' : IsChain (· ≤ ·) (Set.univ : Set c) := by
133 intro a ha b hb hne
134 have hne' : (a : GeneratorConvergingPair (G := G)) ≠ b := by
135 intro h
136 exact hne (Subtype.ext h)
137 simpa using hc a.2 b.2 hne'
138 rcases finite_subset_chain_has_upper hc' s (by intro z hz; simp only [mem_univ]) hsne with ⟨m, hm, hmax⟩
139 refine ⟨m, ?_⟩
140 intro x hx
141 have hx' :
142 x ∈ ⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G)) := by
143 refine mem_iInter₂.2 ?_
144 intro p hp
145 exact (hmax p hp).1 hx
146 exact hs hx'
147 · rcases hcne with ⟨p, hp⟩
148 refine ⟨⟨p, hp⟩, ?_⟩
149 have htop : ((⊤ : Subgroup G) : Set G) ⊆ ((U : Subgroup G) : Set G) := by
150 have : (⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := hs
151 simpa [Finset.not_nonempty_iff_eq_empty.mp hsne] using this
152 intro x hx
153 exact htop (by simp only [Subgroup.coe_top, mem_univ])
155/-- Upper bound of a nonempty chain of generator-converging pairs. -/
158 {c : Set (GeneratorConvergingPair (G := G))}
159 (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty) :
161 N := iInf fun p : c => p.1.N
162 normal_N := by
163 classical
164 exact Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
165 closed_N := by
166 classical
167 simpa using isClosed_iInter (fun p : c => p.1.closed_N)
168 X := ⋃ p : c, p.1.X
169 subset_compl := by
170 intro x hx
171 rcases mem_iUnion.mp hx with ⟨p, hpx⟩
172 refine by
173 intro hxK
174 exact p.1.subset_compl hpx ((iInf_le (fun q : c => q.1.N) p) hxK)
175 convergesToOne_mod := by
176 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
177 intro U hKU
179 hKU with ⟨p, hpU⟩
180 have hEq : ((⋃ q : c, q.1.X) \ (U : Set G)) = (p.1.X \ (U : Set G)) := by
181 ext x
182 constructor
183 · intro hx
184 rcases hx with ⟨hxX, hxU⟩
185 rcases mem_iUnion.mp hxX with ⟨q, hqx⟩
186 have hcmp :
187 (q.1 ≤ p.1) ∨ (p.1 ≤ q.1) := by
188 by_cases hqp : q = p
189 · exact Or.inl (hqp ▸ le_rfl)
190 · have hqp' : (q : GeneratorConvergingPair (G := G)) ≠ p := by
191 intro h
192 exact hqp (Subtype.ext h)
193 exact hc q.2 p.2 hqp'
194 cases hcmp with
195 | inl hqp =>
196 exact ⟨hqp.2.1 hqx, hxU⟩
197 | inr hpq =>
198 by_cases hxp : x ∈ p.1.X
199 · exact ⟨hxp, hxU⟩
200 · have hxN : x ∈ (p.1.N : Set G) := hpq.2.2 ⟨hqx, hxp⟩
201 exact False.elim (hxU (hpU hxN))
202 · intro hx
203 exact ⟨mem_iUnion.mpr ⟨p, hx.1⟩, hx.2⟩
204 rw [hEq]
205 exact p.1.convergesToOne_mod U hpU
206 generates := by
207 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
208 letI : T2Space G := IsProfiniteGroup.t2Space hG
209 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
210 let K : Subgroup G := iInf fun p : c => p.1.N
211 letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
212 have hKclosed : IsClosed (K : Set G) := by
213 simpa [K] using isClosed_iInter (fun p : c => p.1.closed_N)
215 (G := G) hG
216 (N := K) (X := ⋃ p : c, p.1.X)).2
217 intro U hKU
218 rcases exists_pair_le_openSubgroup_of_chain_iInf_le (G := G) hc hcne U.toOpenSubgroup
219 (by simpa [K] using hKU) with ⟨p, hpU⟩
220 have hpgen :
221 TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
222 ((QuotientGroup.mk' (U : Subgroup G)) '' p.1.X) := by
223 letI : p.1.N.Normal := p.1.normal_N
224 exact
226 (G := G) hG
227 (N := p.1.N) (X := p.1.X)).1
228 p.1.generates U hpU
230 intro y hy
231 rcases hy with ⟨x, hx, rfl⟩
232 exact ⟨x, mem_iUnion.mpr ⟨p, hx⟩, rfl⟩)
234/-- The generator-converging-pair order is inductive over chains. -/
236 (c : Set (GeneratorConvergingPair (G := G)))
237 (hc : IsChain (· ≤ ·) c) :
238 BddAbove c := by
239 classical
240 rcases c.eq_empty_or_nonempty with rfl | hcne
241 · exact ⟨initialGeneratorConvergingPair (G := G), by intro a ha; cases ha⟩
242 · refine ⟨chainUpperBoundOfNonempty (G := G) hG hc hcne, ?_⟩
243 intro p hp
244 refine ⟨?_, ?_, ?_⟩
245 · exact iInf_le (fun q : {q // q ∈ c} => q.1.N) ⟨p, hp⟩
246 · intro x hx
247 exact mem_iUnion.mpr ⟨⟨p, hp⟩, hx⟩
248 · intro x hx
249 rcases hx with ⟨hxX, hxpX⟩
250 rcases mem_iUnion.mp hxX with ⟨q, hqx⟩
251 by_cases hqp : q = ⟨p, hp⟩
252 · exact False.elim (hxpX (by simpa [hqp] using hqx))
253 · have hqp' : (q : GeneratorConvergingPair (G := G)) ≠ p := by
254 intro h
255 exact hqp (Subtype.ext h)
256 rcases hc q.2 hp hqp' with hqle | hple
257 · exact False.elim (hxpX (hqle.2.1 hqx))
258 · exact hple.2.2 ⟨hqx, hxpX⟩
260/-- An open-normal quotient of a closed normal subgroup has a finite generating set modulo the
261intersection with the open normal subgroup. -/
263 (hG : IsProfiniteGroup G) {M : Subgroup G}
264 (hMclosed : IsClosed (M : Set G)) (U : OpenNormalSubgroup G) :
265 ∃ T : Set G,
266 T.Finite ∧
267 T ⊆ (M : Set G) \ (((U : Subgroup G) ⊓ M : Subgroup G) : Set G) ∧
268 M ≤ Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) := by
269 classical
270 have hMprof : IsProfiniteGroup M := IsProfiniteGroup.of_isClosed_subgroup (G := G) hG M hMclosed
271 letI : CompactSpace M := IsProfiniteGroup.compactSpace hMprof
272 let UM : OpenNormalSubgroup M :=
273 OpenNormalSubgroup.comap (M.subtype) continuous_subtype_val U
274 obtain ⟨σ, -, hσright, -⟩ :=
276 let q1 : M ⧸ (UM : Subgroup M) := ((1 : M) : M ⧸ (UM : Subgroup M))
277 let Tsub : Set M := σ '' ({q1} : Set (M ⧸ (UM : Subgroup M)))ᶜ
278 let T : Set G := Subtype.val '' Tsub
279 refine ⟨T, ?_, ?_, ?_⟩
280 · letI : Finite (M ⧸ (UM : Subgroup M)) := openNormalSubgroup_finiteQuotient (G := M) UM
281 have hfin : ({q1} : Set (M ⧸ (UM : Subgroup M)))ᶜ.Finite := Set.toFinite _
282 exact hfin.image σ |>.image Subtype.val
283 · intro x hx
284 rcases hx with ⟨y, hy, rfl⟩
285 rcases hy with ⟨q, hq, rfl⟩
286 refine ⟨(σ q).2, ?_⟩
287 intro hxUM
288 have hσUM : σ q ∈ (UM : Subgroup M) := by
289 change (((σ q : M) : G) ∈ (U : Subgroup G))
290 exact hxUM.1
291 have : q = q1 := by
292 calc
293 q = QuotientGroup.mk' (UM : Subgroup M) (σ q) := (hσright q).symm
294 _ = q1 := by
295 have hq1 :
296 QuotientGroup.mk' (UM : Subgroup M) (σ q) = (1 : M ⧸ (UM : Subgroup M)) :=
297 (QuotientGroup.eq_one_iff (N := (UM : Subgroup M)) (σ q)).2 hσUM
298 simpa [q1] using hq1
299 exact hq this
300 · intro m hmM
301 let mM : M := ⟨m, hmM⟩
302 let q : M ⧸ (UM : Subgroup M) := QuotientGroup.mk' (UM : Subgroup M) mM
303 by_cases hq : q = q1
304 · have hmUM : (⟨m, hmM⟩ : M) ∈ (UM : Subgroup M) := by
305 have hq1 : QuotientGroup.mk' (UM : Subgroup M) mM = (1 : M ⧸ (UM : Subgroup M)) := by
306 simpa [q, q1, mM] using hq
307 exact (QuotientGroup.eq_one_iff (N := (UM : Subgroup M)) mM).1 hq1
308 have hmN' : m ∈ ((U : Subgroup G) ⊓ M : Subgroup G) := by
309 refine ⟨?_, hmM⟩
310 change (((⟨m, hmM⟩ : M) : G) ∈ (U : Subgroup G))
311 simpa using hmUM
312 exact Subgroup.subset_closure (Or.inr hmN')
313 · have hT : ((σ q : M) : G) ∈ T := by
314 exact ⟨σ q, ⟨q, hq, rfl⟩, rfl⟩
315 have hEq :
316 QuotientGroup.mk' (UM : Subgroup M) (σ q) =
317 QuotientGroup.mk' (UM : Subgroup M) mM := by
318 simpa [q, mM] using hσright q
319 have hdiv : (σ q)⁻¹ * mM ∈ (UM : Subgroup M) := by
320 exact (QuotientGroup.eq).1 hEq
321 have hdivU : (((σ q : M) : G)⁻¹ * m) ∈ (U : Subgroup G) := by
322 change ((((σ q)⁻¹ * mM : M) : G) ∈ (U : Subgroup G))
323 simpa [mM] using hdiv
324 have hdivM : (((σ q : M) : G)⁻¹ * m) ∈ M := by
325 change ((((σ q)⁻¹ * mM : M) : G) ∈ M)
326 exact (((σ q)⁻¹ * mM : M)).2
327 have hN' : (((σ q : M) : G)⁻¹ * m) ∈ ((U : Subgroup G) ⊓ M : Subgroup G) := by
328 exact ⟨hdivU, hdivM⟩
329 have hσ' :
330 ((σ q : M) : G) ∈
331 Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) :=
332 Subgroup.subset_closure (Or.inl hT)
333 have hdiv' :
334 ((σ q : M) : G)⁻¹ * m ∈
335 Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) :=
336 Subgroup.subset_closure (Or.inr hN')
337 have hmEq : m = ((σ q : M) : G) * (((σ q : M) : G)⁻¹ * m) := by
338 simp only [mul_inv_cancel_left]
339 rw [hmEq]
340 exact (Subgroup.closure _).mul_mem hσ' hdiv'
343end ProCGroups.Generation