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

ProCGroups/Generation/QuotientGeneratorConvergingPairs.lean

1import ProCGroups.Generation.Convergence
2import ProCGroups.Generation.GeneratorConvergingPairs
3import ProCGroups.ProC.Quotients.ClosedNormal
4import ProCGroups.Profinite.MathlibBridge
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/Generation/QuotientGeneratorConvergingPairs.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.InverseSystems
28open ProCGroups.ProC
30variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32section Proposition244
35 N : Subgroup G
36 normal_N : N.Normal
37 closed_N : IsClosed (N : Set G)
38 Y : Set (G ⧸ N)
39 subset_compl : Y ⊆ ({1} : Set (G ⧸ N))ᶜ
40 converges : ConvergesToOne (G := G ⧸ N) Y
41 generates : TopologicallyGenerates (G := G ⧸ N) Y
43attribute [instance] QuotientGeneratorConvergingPair.normal_N
45def QuotientGeneratorConvergingPair.sourceSet
47 Set (G ⧸ A.N) :=
48 ({1} : Set (G ⧸ A.N)) ∪ A.Y
50abbrev QuotientGeneratorConvergingPair.Source
52 ↥(A.sourceSet)
56 TopologicalSpace A.Source :=
57 inferInstanceAs (TopologicalSpace ↥(A.sourceSet))
59def QuotientGeneratorConvergingPair.sourceOne
60 (A : QuotientGeneratorConvergingPair (G := G)) : A.Source :=
61 ⟨1, Or.inl rfl⟩
63def QuotientGeneratorConvergingPair.sourceOfY
64 (A : QuotientGeneratorConvergingPair (G := G)) (y : A.Y) : A.Source :=
65 ⟨y.1, Or.inr y.2⟩
67theorem QuotientGeneratorConvergingPair.source_cases
68 (A : QuotientGeneratorConvergingPair (G := G)) (x : A.Source) :
69 x = A.sourceOne ∨ ∃ y : A.Y, x = A.sourceOfY y := by
70 rcases x with ⟨x, hx⟩
71 rcases hx with hx1 | hxY
72 · left
73 ext
74 simpa [QuotientGeneratorConvergingPair.sourceOne] using hx1
75 · right
76 refine ⟨⟨x, hxY⟩, ?_⟩
77 ext
78 rfl
80def QuotientGeneratorConvergingPair.yImage
82 (σ : A.Source → G ⧸ B.N) : Set (G ⧸ B.N) :=
83 Set.range fun y : A.Y => σ (A.sourceOfY y)
85def QuotientGeneratorConvergingPair.Le
86 (A B : QuotientGeneratorConvergingPair (G := G)) : Prop :=
87 ∃ hBA : B.N ≤ A.N,
88 ∃ σ : A.Source → (G ⧸ B.N),
89 Continuous σ ∧
90 (∀ x : A.Source, leftQuotientProjection (B.N) (A.N) hBA (σ x) = x.1) ∧
91 σ A.sourceOne = 1 ∧
92 (∀ y : A.Y, σ (A.sourceOfY y) ∈ B.Y) ∧
93 B.Y \ A.yImage B σ ⊆
94 {q : G ⧸ B.N | leftQuotientProjection (B.N) (A.N) hBA q = 1}
98 le := QuotientGeneratorConvergingPair.Le
101 Preorder (QuotientGeneratorConvergingPair (G := G)) where
102 le_refl A := by
103 refine ⟨le_rfl, Subtype.val, ?_, ?_, rfl, ?_, ?_⟩
104 · change Continuous (fun x : A.Source => (x : G ⧸ A.N))
105 exact continuous_subtype_val
106 · intro q
107 simp only [leftQuotientProjection_id, id_eq]
108 · intro y
109 simp only [QuotientGeneratorConvergingPair.sourceOfY, Subtype.coe_prop]
110 · simp only [QuotientGeneratorConvergingPair.yImage, QuotientGeneratorConvergingPair.sourceOfY,
111 Subtype.range_coe_subtype, setOf_mem_eq, sdiff_self, bot_eq_empty, leftQuotientProjection_id, id_eq,
112 setOf_eq_eq_singleton, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff, implies_true]
113 le_trans A B C hAB hBC := by
114 classical
115 rcases hAB with ⟨hBA, σAB, hσABcont, hσABright, hσABone, hσABmem, hσABdiff⟩
116 rcases hBC with ⟨hCB, σBC, hσBCcont, hσBCright, hσBCone, hσBCmem, hσBCdiff⟩
117 let τ : A.Source → B.Source := fun x =>
118 ⟨σAB x, by
119 rcases A.source_cases x with h1 | ⟨y, rfl⟩
120 · rw [h1]
121 exact Or.inl hσABone
122 · exact Or.inr (hσABmem y)⟩
123 have hτcont : Continuous τ := by
124 exact hσABcont.subtype_mk <| by
125 intro x
126 rcases A.source_cases x with h1 | ⟨y, rfl⟩
127 · rw [h1]
128 exact Or.inl hσABone
129 · exact Or.inr (hσABmem y)
130 have hτone : τ A.sourceOne = B.sourceOne := by
131 apply Subtype.ext
132 exact hσABone
133 have hτofY (y : A.Y) :
134 τ (A.sourceOfY y) = B.sourceOfY ⟨σAB (A.sourceOfY y), hσABmem y⟩ := by
135 apply Subtype.ext
136 rfl
137 have hEqBC :
138 ∀ (y : B.Y) {q : G ⧸ C.N},
139 q ∈ C.Y →
140 leftQuotientProjection (C.N) (B.N) hCB q = y.1 →
141 q = σBC (B.sourceOfY y) := by
142 intro y q hqY hqproj
143 by_cases hqim : q ∈ B.yImage C σBC
144 · rcases hqim with ⟨y', hy'Eq⟩
145 have hproj' :
146 leftQuotientProjection (C.N) (B.N) hCB q = y'.1 := by
147 simpa [hy'Eq] using hσBCright (B.sourceOfY y')
148 have hyEq : y' = y := by
149 apply Subtype.ext
150 exact hproj'.symm.trans hqproj
151 simpa [hyEq] using hy'Eq.symm
152 · have hker :
153 leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqim⟩
154 have hyne : y.1 ≠ 1 := by
155 simpa using B.subset_compl y.2
156 exact False.elim (hyne (hqproj.symm.trans hker))
157 refine ⟨hCB.trans hBA, fun x => σBC (τ x), hσBCcont.comp hτcont, ?_, ?_, ?_, ?_⟩
158 · intro x
159 calc
160 leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) (σBC (τ x)) =
161 leftQuotientProjection (B.N) (A.N) hBA
162 (leftQuotientProjection (C.N) (B.N) hCB (σBC (τ x))) := by
164 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
165 (L := (A.N : Subgroup G)) hCB hBA (σBC (τ x))
166 _ = leftQuotientProjection (B.N) (A.N) hBA ((τ x).1) := by
167 rw [hσBCright (τ x)]
168 _ = leftQuotientProjection (B.N) (A.N) hBA (σAB x) := by
169 rfl
170 _ = x.1 := hσABright x
171 · simpa [hτone] using hσBCone
172 · intro y
173 let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩
174 simpa [hτofY, yB] using hσBCmem yB
175 · intro q hq
176 rcases hq with ⟨hqY, hqnotAC⟩
177 by_cases hqimB : q ∈ B.yImage C σBC
178 · rcases hqimB with ⟨z, hzEq⟩
179 have hzNotInA : z.1 ∉ A.yImage B σAB := by
180 intro hzInA
181 rcases hzInA with ⟨y, hyEq⟩
182 let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩
183 have hprojqz :
184 leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by
185 simpa [hzEq] using hσBCright (B.sourceOfY z)
186 have hprojq :
187 leftQuotientProjection (C.N) (B.N) hCB q = yB.1 := by
188 calc
189 leftQuotientProjection (C.N) (B.N) hCB q = z.1 := hprojqz
190 _ = yB.1 := by
191 simpa [yB] using hyEq.symm
192 have hqEq : q = σBC (B.sourceOfY yB) := hEqBC yB hqY hprojq
193 have hqInAC : q ∈ A.yImage C (fun x => σBC (τ x)) := by
194 refine ⟨y, ?_⟩
195 simpa [hτofY] using hqEq.symm
196 exact hqnotAC hqInAC
197 have hzProjA :
198 leftQuotientProjection (B.N) (A.N) hBA z.1 = 1 :=
199 hσABdiff ⟨z.2, hzNotInA⟩
200 have hprojqB :
201 leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by
202 simpa [hzEq] using hσBCright (B.sourceOfY z)
203 calc
204 leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =
205 leftQuotientProjection (B.N) (A.N) hBA
206 (leftQuotientProjection (C.N) (B.N) hCB q) := by
208 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
209 (L := (A.N : Subgroup G)) hCB hBA q
210 _ = leftQuotientProjection (B.N) (A.N) hBA z.1 := by
211 rw [hprojqB]
212 _ = 1 := hzProjA
213 · have hprojqB :
214 leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqimB⟩
215 calc
216 leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =
217 leftQuotientProjection (B.N) (A.N) hBA
218 (leftQuotientProjection (C.N) (B.N) hCB q) := by
220 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
221 (L := (A.N : Subgroup G)) hCB hBA q
222 _ = leftQuotientProjection (B.N) (A.N) hBA 1 := by
223 rw [hprojqB]
224 _ = 1 := by
225 rfl
227noncomputable def QuotientGeneratorConvergingPair.le_hBA
228 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
229 B.N ≤ A.N :=
230 Classical.choose hAB
232noncomputable def QuotientGeneratorConvergingPair.le_map
233 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
234 A.Source → G ⧸ B.N :=
235 Classical.choose (Classical.choose_spec hAB)
237theorem QuotientGeneratorConvergingPair.le_map_continuous
238 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
239 Continuous (A.le_map hAB) :=
240 (Classical.choose_spec (Classical.choose_spec hAB)).1
242@[simp] theorem QuotientGeneratorConvergingPair.le_map_right
243 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
244 (x : A.Source) :
245 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) (A.le_map hAB x) = x.1 :=
246 (Classical.choose_spec (Classical.choose_spec hAB)).2.1 x
248@[simp] theorem QuotientGeneratorConvergingPair.le_map_one
249 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
250 A.le_map hAB A.sourceOne = 1 :=
251 (Classical.choose_spec (Classical.choose_spec hAB)).2.2.1
253@[simp] theorem QuotientGeneratorConvergingPair.le_map_mem
254 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
255 (y : A.Y) :
256 A.le_map hAB (A.sourceOfY y) ∈ B.Y :=
257 (Classical.choose_spec (Classical.choose_spec hAB)).2.2.2.1 y
259theorem QuotientGeneratorConvergingPair.le_map_diff
260 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
261 B.Y \ A.yImage B (A.le_map hAB) ⊆
262 {q : G ⧸ B.N |
263 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = 1} :=
264 (Classical.choose_spec (Classical.choose_spec hAB)).2.2.2.2
266theorem QuotientGeneratorConvergingPair.eq_le_map_of_mem_of_proj_eq
267 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
268 (y : A.Y) {q : G ⧸ B.N}
269 (hqY : q ∈ B.Y)
270 (hqproj : leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = y.1) :
271 q = A.le_map hAB (A.sourceOfY y) := by
272 by_cases hqim : q ∈ A.yImage B (A.le_map hAB)
273 · rcases hqim with ⟨y', hy'Eq⟩
274 have hproj' :
275 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = y'.1 := by
276 simpa [hy'Eq] using A.le_map_right hAB (A.sourceOfY y')
277 have hyEq : y' = y := by
278 ext
279 exact hproj'.symm.trans hqproj
280 simpa [hyEq] using hy'Eq.symm
281 · have hker :
282 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = 1 :=
283 A.le_map_diff hAB ⟨hqY, hqim⟩
284 have hyne : y.1 ≠ 1 := by
285 simpa using A.subset_compl y.2
286 exact False.elim (hyne (hqproj.symm.trans hker))
288theorem QuotientGeneratorConvergingPair.le_map_compat
290 (hAB : A ≤ B) (hAC : A ≤ C) (hBC : B ≤ C)
291 (y : A.Y) :
292 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
293 (A.le_map hAC (A.sourceOfY y)) =
294 A.le_map hAB (A.sourceOfY y) := by
295 have hCy :
296 A.le_map hAC (A.sourceOfY y) ∈ C.Y := A.le_map_mem hAC y
297 have hIn :
298 A.le_map hAC (A.sourceOfY y) ∈ B.yImage C (B.le_map hBC) := by
299 by_contra hNot
300 have hker :
301 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
302 (A.le_map hAC (A.sourceOfY y)) = 1 :=
303 B.le_map_diff hBC ⟨hCy, hNot⟩
304 have hy1 : y.1 = 1 := by
305 calc
306 y.1 = leftQuotientProjection (C.N) (A.N) (A.le_hBA hAC)
307 (A.le_map hAC (A.sourceOfY y)) := by
308 exact (A.le_map_right hAC (A.sourceOfY y)).symm
309 _ = leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB)
310 (leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
311 (A.le_map hAC (A.sourceOfY y))) := by
312 exact
314 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
315 (L := (A.N : Subgroup G)) (B.le_hBA hBC) (A.le_hBA hAB)
316 (A.le_map hAC (A.sourceOfY y)))
317 _ = leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) 1 := by rw [hker]
318 _ = 1 := by rfl
319 have hyne : y.1 ≠ 1 := by
320 simpa using A.subset_compl y.2
321 exact hyne hy1
322 rcases hIn with ⟨z, hzEq⟩
323 have hqY :
324 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
325 (A.le_map hAC (A.sourceOfY y)) ∈ B.Y := by
326 have hEq :
327 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
328 (A.le_map hAC (A.sourceOfY y)) = z.1 := by
329 simpa [hzEq] using B.le_map_right hBC (B.sourceOfY z)
330 exact hEq ▸ z.2
331 have hqproj :
332 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB)
333 (leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
334 (A.le_map hAC (A.sourceOfY y))) = y.1 := by
336 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
337 (L := (A.N : Subgroup G)) (B.le_hBA hBC) (A.le_hBA hAB)
338 (A.le_map hAC (A.sourceOfY y))).trans
339 (A.le_map_right hAC (A.sourceOfY y))
340 exact A.eq_le_map_of_mem_of_proj_eq hAB y hqY hqproj
342theorem ConvergesToOne.range_subtype_pointed
343 {H : Type v} [Group H] [TopologicalSpace H]
344 (hG : IsProfiniteGroup G) {X : Set G}
345 {f : ↥((({1} : Set G) ∪ X)) → H}
346 (hf : Continuous f)
347 (hf1 : f ⟨1, Or.inl rfl⟩ = 1)
348 (hX : ConvergesToOne (G := G) X) :
350 (Set.range fun x : X => f ⟨x.1, Or.inr x.2⟩) := by
351 letI : T2Space G := IsProfiniteGroup.t2Space hG
352 let S : Set G := ({1} : Set G) ∪ X
353 let g : X → H := fun x => f ⟨x.1, Or.inr x.2⟩
354 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
355 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
356 intro U
357 have hpre : IsOpen (f ⁻¹' (U : Set H)) :=
358 (openSubgroup_isOpen (G := H) U).preimage hf
359 have h1pre : (⟨1, Or.inl rfl⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by
360 simp only [singleton_union, mem_preimage, hf1, SetLike.mem_coe, one_mem, S]
361 rcases isOpen_induced_iff.mp hpre with ⟨W, hWopen, hWeq⟩
362 have h1W : (1 : G) ∈ W := by
363 have : (⟨1, Or.inl rfl⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by
364 exact hWeq.symm ▸ h1pre
365 simpa using this
366 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨V, hVW⟩
367 have hsubset :
368 Set.range g \ (U : Set H) ⊆ g '' {x : X | (x : G) ∉ (V : Set G)} := by
369 intro y hy
370 rcases hy with ⟨hyY, hyU⟩
371 rcases hyY with ⟨x, rfl⟩
372 refine ⟨x, ?_, rfl⟩
373 intro hxV
374 have hxW : (x : G) ∈ W := hVW hxV
375 have hxpre : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by
376 simpa [S] using hxW
377 have hxpreU : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by
378 exact hWeq ▸ hxpre
379 have : g x ∈ (U : Set H) := by
380 simpa [g] using hxpreU
381 exact hyU this
382 have hfinite_pre : {x : X | (x : G) ∉ (V : Set G)}.Finite := by
383 let e : X ↪ G := ⟨Subtype.val, Subtype.val_injective⟩
384 have hfinite : (X \ (V : Set G)).Finite := hX V.toOpenSubgroup
385 have hfinite' : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)}.Finite := by
386 simpa [Set.preimage] using hfinite.preimage_embedding e
387 have hEq : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)} = {x : X | (x : G) ∉ (V : Set G)} := by
388 ext x
389 simp only [Function.Embedding.coeFn_mk, Subtype.coe_prop, SetLike.mem_coe, true_and, mem_setOf_eq, e]
390 exact hEq ▸ hfinite'
391 exact hfinite_pre.image g |>.subset hsubset
395 (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty)
396 (U : OpenSubgroup G)
397 (hInf : iInf (fun p : c => p.1.N) ≤ (U : Subgroup G)) :
398 ∃ p : c, p.1.N ≤ (U : Subgroup G) := by
399 classical
400 have hInter :
401 (⋂ p : c, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := by
402 intro x hx
403 exact hInf (by simpa [Subgroup.mem_iInf] using hx)
405 (H := fun p : c => p.1.N)
406 (hclosed := fun p => p.1.closed_N)
407 U hInter with ⟨s, hs⟩
408 by_cases hsne : s.Nonempty
409 · have hc' : IsChain (· ≤ ·) (Set.univ : Set c) := by
410 intro a ha b hb hne
411 have hne' : (a : QuotientGeneratorConvergingPair (G := G)) ≠ b := by
412 intro h
413 exact hne (Subtype.ext h)
414 simpa using hc a.2 b.2 hne'
415 rcases finite_subset_chain_has_upper hc' s (by intro z hz; simp only [mem_univ]) hsne with ⟨m, hm, hmax⟩
416 refine ⟨m, ?_⟩
417 intro x hx
418 have hx' :
419 x ∈ ⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G)) := by
420 refine mem_iInter₂.2 ?_
421 intro p hp
422 exact (QuotientGeneratorConvergingPair.le_hBA (hmax p hp)) hx
423 exact hs hx'
424 · rcases hcne with ⟨p, hp⟩
425 refine ⟨⟨p, hp⟩, ?_⟩
426 have htop : ((⊤ : Subgroup G) : Set G) ⊆ ((U : Subgroup G) : Set G) := by
427 have :
428 (⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := hs
429 simpa [Finset.not_nonempty_iff_eq_empty.mp hsne] using this
430 intro x hx
431 exact htop (by simp only [Subgroup.coe_top, mem_univ])
436 (hc : IsChain (· ≤ ·) c) (a : c) :
437 let K : Subgroup G := iInf fun p : c => p.1.N
438 letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
439 ∃ σ : a.1.Source → G ⧸ K,
440 Continuous σ ∧
441 (∀ b : c, ∀ hab : a.1 ≤ b.1,
443 (iInf_le (fun p : c => p.1.N) b) ∘ σ =
444 a.1.le_map hab) ∧
445 σ a.1.sourceOne = 1 := by
446 classical
447 let K : Subgroup G := iInf fun p : c => p.1.N
448 letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
449 let Tail := {b : c // a.1 ≤ b.1}
450 letI : Nonempty Tail := ⟨⟨a, le_rfl⟩⟩
451 let L : Tail → ClosedSubgroup G := fun b =>
452 ⟨b.1.1.N, b.1.1.closed_N⟩
453 have hL : ∀ {i j : Tail}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G) := by
454 intro i j hij
455 exact QuotientGeneratorConvergingPair.le_hBA hij
456 have hdir : Directed (· ≤ ·) (id : Tail → Tail) := by
457 intro i j
458 by_cases hij : i ≤ j
459 · exact ⟨j, hij, le_rfl⟩
460 · have hji : j ≤ i := by
461 by_cases hEq : i = j
462 · exact hEq ▸ le_rfl
463 · rcases hc i.1.2 j.1.2 (by
464 intro h
465 exact hEq (Subtype.ext (Subtype.ext h))) with hij' | hji'
466 · exact False.elim (hij hij')
467 · exact hji'
468 exact ⟨i, le_rfl, hji⟩
469 let η : ∀ b : Tail, a.1.Source → G ⧸ (L b : Subgroup G) := fun b =>
470 a.1.le_map b.2
471 have hηcont : ∀ b : Tail, Continuous (η b) := by
472 intro b
473 exact a.1.le_map_continuous b.2
474 have hηcompat : ∀ {i j : Tail} (hij : i ≤ j),
475 leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i := by
476 intro i j hij
477 funext x
478 rcases a.1.source_cases x with rfl | ⟨y, rfl⟩
479 · have h1j : η j a.1.sourceOne = 1 := by
480 change a.1.le_map j.2 a.1.sourceOne = 1
481 exact a.1.le_map_one j.2
482 have h1i : η i a.1.sourceOne = 1 := by
483 change a.1.le_map i.2 a.1.sourceOne = 1
484 exact a.1.le_map_one i.2
485 calc
486 (leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j)
487 a.1.sourceOne
488 = leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)
489 (η j a.1.sourceOne) := by
490 simp only [Function.comp]
491 _ = leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) 1 := by
492 rw [h1j]
493 _ = 1 := by rfl
494 _ = η i a.1.sourceOne := by rw [h1i]
495 · simpa [η] using a.1.le_map_compat i.2 j.2 hij y
496 have hηone : ∀ b : Tail, η b a.1.sourceOne = 1 := by
497 intro b
498 change a.1.le_map b.2 a.1.sourceOne = 1
499 exact a.1.le_map_one b.2
500 obtain ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩ :=
502 (G := G) hG L hL hdir η hηcont hηcompat a.1.sourceOne hηone
503 let H : Subgroup G := ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)
504 have hKeq : H = K := by
505 apply le_antisymm
506 · refine le_iInf ?_
507 intro p
508 by_cases hap : a.1 ≤ p.1
509 · exact iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨p, hap⟩
510 · have hKa :
511 H ≤ a.1.N :=
512 iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨a, le_rfl⟩
513 by_cases hEq : p = a
514 · simpa [K, hEq] using hKa
515 · rcases hc p.2 a.2 (by
516 intro h
517 exact hEq (Subtype.ext h)) with hpa | hap'
518 · exact hKa.trans (QuotientGeneratorConvergingPair.le_hBA hpa)
519 · exact False.elim (hap hap')
520 · refine le_iInf ?_
521 intro b
522 exact iInf_le (fun p : c => p.1.N) b.1
523 letI : H.Normal := by
524 exact Subgroup.normal_iInf_normal fun b : Tail => b.1.1.normal_N
525 have hGoal :
526 ∃ σ : a.1.Source → G ⧸ H,
527 Continuous σ ∧
528 (∀ b : c, ∀ hab : a.1 ≤ b.1,
530 (closedSubgroup_sInf_le (L := L) ⟨b, hab⟩) ∘ σ =
531 a.1.le_map hab) ∧
532 σ a.1.sourceOne = 1 := by
533 refine ⟨ηinf, hηinf_continuous, ?_, hηinf_one⟩
534 intro b hab
535 simpa [Tail, L, η] using hηinf_fac ⟨b, hab⟩
536 have hGoal' :
537 ∃ σ : a.1.Source → G ⧸ H,
538 Continuous σ ∧
539 (∀ b : c, ∀ hab : a.1 ≤ b.1,
541 (hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)) ∘ σ =
542 a.1.le_map hab) ∧
543 σ a.1.sourceOne = 1 := by
544 rcases hGoal with ⟨σ, hσcont, hσfac, hσone⟩
545 refine ⟨σ, hσcont, ?_, hσone⟩
546 intro b hab
547 simpa using hσfac b hab
548 change
549 ∃ σ : a.1.Source → G ⧸ K,
550 Continuous σ ∧
551 (∀ b : c, ∀ hab : a.1 ≤ b.1,
553 (iInf_le (fun p : c => p.1.N) b) ∘ σ =
554 a.1.le_map hab) ∧
555 σ a.1.sourceOne = 1
556 let Data : Type _ := { J : Subgroup G // J.Normal ∧ ∀ b : c, J ≤ b.1.N }
557 let P : Data → Prop := fun d =>
558 letI : d.1.Normal := d.2.1
559 ∃ σ : a.1.Source → G ⧸ d.1,
560 Continuous σ ∧
561 (∀ b : c, ∀ hab : a.1 ≤ b.1,
562 leftQuotientProjection d.1 b.1.N (d.2.2 b) ∘ σ =
563 a.1.le_map hab) ∧
564 σ a.1.sourceOne = 1
565 let dH : Data :=
566 ⟨H, ⟨inferInstance, fun b => hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)⟩⟩
567 let dK : Data :=
568 ⟨K, ⟨inferInstance, fun b => iInf_le (fun p : c => p.1.N) b⟩⟩
569 have hd : dH = dK := by
570 apply Subtype.ext
571 exact hKeq
572 have hPdH : P dH := by
573 simpa [P, dH] using hGoal'
574 have hPdK : P dK := by
575 exact Eq.mp (congrArg P hd) hPdH
576 simpa [P, dK] using hPdK
578noncomputable def quotientGeneratorPairTop :
580 N := ⊤
581 normal_N := by infer_instance
582 closed_N := isClosed_univ
583 Y := ∅
584 subset_compl := by intro q hq; simp only [mem_empty_iff_false] at hq
585 converges := by intro U; simp only [empty_diff, finite_empty]
586 generates := by
587 classical
589 apply top_unique
590 intro q hq
591 rcases Quotient.exists_rep q with ⟨g, rfl⟩
592 have hg1 : QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G)) := by
593 exact (QuotientGroup.eq_one_iff (N := (⊤ : Subgroup G)) g).2 (by simp only [Subgroup.mem_top])
594 have hbot :
595 QuotientGroup.mk' (⊤ : Subgroup G) g ∈ (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) := by
596 change QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G))
597 exact hg1
598 simpa [Subgroup.closure_eq] using
599 (Subgroup.le_topologicalClosure (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) hbot)
604 (hne : p.N ≠ ⊥) :
605 ∃ p' : QuotientGeneratorConvergingPair (G := G), p ≤ p' ∧ ¬ p' ≤ p := by
606 classical
607 rcases (Subgroup.ne_bot_iff_exists_ne_one).1 hne with ⟨m, hmne⟩
608 have hmne' : (m : G) ≠ 1 := by
609 intro hm1
610 apply hmne
611 ext
612 simpa using hm1
613 rcases exists_openNormalSubgroup_not_mem (G := G) hG hmne' with ⟨U, hmU⟩
614 let N' : Subgroup G := (U : Subgroup G) ⊓ p.N
615 have hN'closed : IsClosed (N' : Set G) := by
616 exact (openNormalSubgroup_isClosed (G := G) U).inter p.closed_N
617 have hN'proper : ¬ p.N ≤ N' := by
618 intro hp
619 exact hmU (hp m.2).1
620 obtain ⟨σ, hσcont, hσright, hσone⟩ :=
622 (G := G) hG
623 ⟨N', hN'closed⟩
624 ⟨p.N, p.closed_N⟩
625 inf_le_right
627 (M := p.N) (hMclosed := p.closed_N) U with ⟨T, hTfin, hTsub, hTgen⟩
628 let Tbar : Set (G ⧸ N') := (QuotientGroup.mk' N') '' T
629 let Y' : Set (G ⧸ N') := σ '' p.Y ∪ Tbar
630 have hY'compl : Y' ⊆ ({1} : Set (G ⧸ N'))ᶜ := by
631 intro q hq
632 rcases hq with hq | hq
633 · rcases hq with ⟨y, hy, rfl⟩
634 intro hq1
635 have hσy1 : σ y = 1 := by
636 simpa using hq1
637 have : y = 1 := by
638 calc
639 y = leftQuotientProjection (N') (p.N) inf_le_right (σ y) := (hσright y).symm
640 _ = leftQuotientProjection (N') (p.N) inf_le_right 1 := by rw [hσy1]
641 _ = 1 := rfl
642 exact p.subset_compl hy this
643 · rcases hq with ⟨t, ht, rfl⟩
644 intro hq1
645 have htN' : t ∈ N' := (QuotientGroup.eq_one_iff (N := N') t).1 hq1
646 exact (hTsub ht).2 htN'
647 have hY'conv : ConvergesToOne (G := G ⧸ N') Y' := by
648 let hGquot : IsProfiniteGroup (G ⧸ p.N) :=
649 isProfinite_quotient_closedNormal (G := G) hG p.closed_N
650 letI : T2Space (G ⧸ p.N) := IsProfiniteGroup.t2Space hGquot
651 intro V
652 have hσconv :
653 ((σ '' p.Y) \ (V : Set (G ⧸ N'))).Finite := by
654 exact
655 (ConvergesToOne.image_of_continuous_pointed
656 (G := G ⧸ p.N) (H := G ⧸ N')
657 hGquot
658 hσcont hσone p.converges) V
659 have hTconv : (Tbar \ (V : Set (G ⧸ N'))).Finite :=
660 (hTfin.image (QuotientGroup.mk' N')).subset (by
661 intro q hq
662 exact hq.1)
663 exact (hσconv.union hTconv).subset (by
664 intro q hq
665 rcases hq with ⟨hqY, hqV⟩
666 rcases hqY with hqσ | hqT
667 · exact Or.inl ⟨hqσ, hqV⟩
668 · exact Or.inr ⟨hqT, hqV⟩)
669 have hY'gen :
670 TopologicallyGenerates (G := G ⧸ N') Y' := by
672 (G := G) hG p.closed_N hN'closed inf_le_right
673 p.generates hσright hTgen
674 refine ⟨{ N := N'
675 normal_N := by infer_instance
676 closed_N := hN'closed
677 Y := Y'
678 subset_compl := hY'compl
679 converges := hY'conv
680 generates := hY'gen }, ?_, ?_⟩
681 · let σ' : p.Source → G ⧸ N' := fun x => σ x.1
682 refine ⟨inf_le_right, σ', ?_, ?_, ?_, ?_, ?_⟩
683 · change Continuous (fun x : p.Source => σ x.1)
684 exact hσcont.comp continuous_subtype_val
685 · intro x
686 exact hσright x.1
687 · exact hσone
688 · intro q
689 exact Or.inl ⟨q.1, q.2, rfl⟩
690 · intro q hq
691 rcases hq with ⟨hqY', hqnotσ⟩
692 rcases hqY' with hqσ | hqT
693 · rcases hqσ with ⟨y, hy, rfl⟩
694 exact False.elim (hqnotσ ⟨⟨y, hy⟩, rfl⟩)
695 · rcases hqT with ⟨t, ht, rfl⟩
696 have htN : t ∈ p.N := (hTsub ht).1
698 (QuotientGroup.eq_one_iff (N := p.N) t).2 htN
699 · intro hp'
700 exact hN'proper hp'.1
702omit [IsTopologicalGroup G] in
703/-- The trivial subgroup of a profinite group is closed. -/
705 IsClosed (((⊥ : Subgroup G) : Set G)) := by
706 letI : T2Space G := IsProfiniteGroup.t2Space hG
707 exact (isClosed_singleton : IsClosed ({(1 : G)} : Set G))
711 (N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG) =
712 (quotientBotContinuousMulEquiv (G := G) hG).symm := by
713 funext q
714 apply (quotientBotContinuousMulEquiv (G := G) hG).injective
715 have h1 :
718 (N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG) q) = q := by
721 (N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG) q)
722 have h2 :
724 ((quotientBotContinuousMulEquiv (G := G) hG).symm q) = q := by
725 simp only [ContinuousMulEquiv.apply_symm_apply]
726 exact h1.trans h2.symm
728noncomputable def QuotientGeneratorConvergingPair.toAmbientSet
730 (hG : IsProfiniteGroup G) : Set G :=
731 closedNormalQuotientSection (G := G) hG (N := p.N) p.closed_N '' p.Y
733theorem QuotientGeneratorConvergingPair.toAmbientSet_generatesAndConvergesToOne
735 (hG : IsProfiniteGroup G) (hbot : p.N = ⊥) :
736 GeneratesAndConvergesToOne (G := G) (p.toAmbientSet hG) := by
737 rcases p with ⟨N, hNnormal, hNclosed, Y, hYcompl, hYconv, hYgen⟩
738 cases hbot
739 constructor
740 · let e : (G ⧸ (⊥ : Subgroup G)) ≃ₜ* G := (quotientBotContinuousMulEquiv (G := G) hG).symm
741 have hgen :
744 (G := G ⧸ (⊥ : Subgroup G)) e hYgen
745 rw [QuotientGeneratorConvergingPair.toAmbientSet, closedNormalQuotientSection_bot_eq]
746 simpa using hgen
747 · let hqbot : IsProfiniteGroup (G ⧸ (⊥ : Subgroup G)) :=
748 IsProfiniteGroup.ofContinuousMulEquiv
749 (G := G) hG (quotientBotContinuousMulEquiv (G := G) hG)
750 have hconv :
753 (N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG)) '' Y) := by
754 exact ConvergesToOne.image_of_continuous_pointed
755 (G := G ⧸ (⊥ : Subgroup G)) (H := G)
756 hqbot
758 (N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG))
760 (N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG))
761 hYconv
762 rw [QuotientGeneratorConvergingPair.toAmbientSet]
765end Proposition244
766section Generators
768variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
774 (hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :
775 ∃ ub : QuotientGeneratorConvergingPair (G := G), ∀ a ∈ c, a ≤ ub := by
776 classical
777 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
778 let K : Subgroup G := iInf fun p : c => p.1.N
779 letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
780 have hKclosed : IsClosed (K : Set G) := by
781 simpa [K] using isClosed_iInter (fun p : c => p.1.closed_N)
782 let hGquotK : IsProfiniteGroup (G ⧸ K) :=
784 letI : T2Space (G ⧸ K) := IsProfiniteGroup.t2Space hGquotK
785 letI : TotallyDisconnectedSpace (G ⧸ K) :=
786 IsProfiniteGroup.totallyDisconnectedSpace hGquotK
787 let lift : (a : c) → a.1.Source → G ⧸ K := fun a =>
788 Classical.choose (quotientGeneratorPair_exists_liftToInf (G := G) hG hc a)
789 have hlift_continuous : ∀ a : c, Continuous (lift a) := by
790 intro a
791 exact (Classical.choose_spec
793 have hlift_fac :
794 ∀ (a b : c) (hab : a.1 ≤ b.1),
796 (iInf_le (fun p : c => p.1.N) b) ∘ lift a =
797 a.1.le_map hab := by
798 intro a b hab
799 exact (Classical.choose_spec
800 (quotientGeneratorPair_exists_liftToInf (G := G) hG hc a)).2.1 b hab
801 have hlift_one : ∀ a : c, lift a a.1.sourceOne = 1 := by
802 intro a
803 exact (Classical.choose_spec
805 have exists_stage_above_le_open :
806 ∀ (a : c) {U : OpenSubgroup G}, K ≤ (U : Subgroup G) →
807 ∃ b : c, a.1 ≤ b.1 ∧ b.1.N ≤ (U : Subgroup G) := by
808 intro a U hKU
809 let d : Set (QuotientGeneratorConvergingPair (G := G)) :=
810 {p | p ∈ c ∧ a.1 ≤ p}
811 have hdchain : IsChain (· ≤ ·) d := by
812 intro x hx y hy hxy
813 exact hc hx.1 hy.1 hxy
814 have hdne : d.Nonempty := ⟨a.1, a.2, le_rfl⟩
815 have hdEq : iInf (fun p : d => p.1.N) = K := by
816 apply le_antisymm
817 · refine le_iInf ?_
818 intro p
819 by_cases hap : a.1 ≤ p.1
820 · exact iInf_le (fun q : d => q.1.N) ⟨p.1, p.2, hap⟩
821 · have hda :
822 iInf (fun q : d => q.1.N) ≤ a.1.N :=
823 iInf_le (fun q : d => q.1.N) ⟨a.1, a.2, le_rfl⟩
824 by_cases hEq : p.1 = a.1
825 · simpa [hEq] using hda
826 · rcases hc p.2 a.2 hEq with hpa | hap'
827 · exact hda.trans (QuotientGeneratorConvergingPair.le_hBA hpa)
828 · exact False.elim (hap hap')
829 · refine le_iInf ?_
830 intro p
831 exact iInf_le (fun q : c => q.1.N) ⟨p.1, p.2.1⟩
832 have hdKU : iInf (fun p : d => p.1.N) ≤ (U : Subgroup G) := by
833 simpa [hdEq] using hKU
835 (G := G) hdchain hdne U hdKU with ⟨b, hbU⟩
836 exact ⟨⟨b.1, b.2.1⟩, b.2.2, hbU⟩
837 let stageImage : c → Set (G ⧸ K) := fun a =>
838 Set.range fun y : a.1.Y => lift a (a.1.sourceOfY y)
839 have hlift_eq_of_le :
840 ∀ {a b : c} (hAB : a.1 ≤ b.1) (y : a.1.Y),
841 lift a (a.1.sourceOfY y) =
842 lift b (b.1.sourceOfY
843 ⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩) := by
844 intro a b hAB y
845 let yb : b.1.Y :=
846 ⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩
847 let q1 := lift a (a.1.sourceOfY y)
848 let q2 := lift b (b.1.sourceOfY yb)
849 have hmem :
850 ∀ W : OpenNormalSubgroup (G ⧸ K), q1⁻¹ * q2 ∈ (W : Set (G ⧸ K)) := by
851 intro W
852 let V : OpenNormalSubgroup G :=
853 OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
854 have hKV : K ≤ (V : Subgroup G) := by
855 intro g hg
856 change QuotientGroup.mk' K g ∈ W
857 have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=
858 (QuotientGroup.eq_one_iff (N := K) g).2 hg
859 rw [hg1]
860 exact W.one_mem'
861 obtain ⟨p, hbp, hpV⟩ := exists_stage_above_le_open b hKV
862 have hcompat :
863 a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) =
864 b.1.le_map hbp (b.1.sourceOfY yb) := by
865 have hqY :
866 a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) ∈ p.1.Y :=
867 a.1.le_map_mem (hAB.trans hbp) y
868 have hqproj :
869 leftQuotientProjection (p.1.N) (b.1.N) (b.1.le_hBA hbp)
870 (a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y)) = yb.1 := by
871 simpa [yb] using a.1.le_map_compat hAB (hAB.trans hbp) hbp y
872 exact b.1.eq_le_map_of_mem_of_proj_eq hbp yb hqY hqproj
873 have hEqp :
875 (iInf_le (fun r : c => r.1.N) p) q1 =
877 (iInf_le (fun r : c => r.1.N) p) q2 := by
878 have hq1 :=
879 congrFun (hlift_fac a p (hAB.trans hbp)) (a.1.sourceOfY y)
880 have hq2 :=
881 congrFun (hlift_fac b p hbp) (b.1.sourceOfY yb)
882 calc
884 (iInf_le (fun r : c => r.1.N) p) q1
885 = a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) := by
886 simpa [q1] using hq1
887 _ = b.1.le_map hbp (b.1.sourceOfY yb) := hcompat
889 (iInf_le (fun r : c => r.1.N) p) q2 := by
890 simpa [q2] using hq2.symm
891 have hEqV :
892 leftQuotientProjection K (V : Subgroup G) hKV q1 =
893 leftQuotientProjection K (V : Subgroup G) hKV q2 := by
894 calc
895 leftQuotientProjection K (V : Subgroup G) hKV q1
896 = leftQuotientProjection (p.1.N) (V : Subgroup G) hpV
898 (iInf_le (fun r : c => r.1.N) p) q1) := by
899 exact
901 (K := (K : Subgroup G)) (H := (p.1.N : Subgroup G))
902 (L := (V : Subgroup G)) (iInf_le (fun r : c => r.1.N) p)
903 hpV q1
904 _ = leftQuotientProjection (p.1.N) (V : Subgroup G) hpV
906 (iInf_le (fun r : c => r.1.N) p) q2) := by
907 rw [hEqp]
908 _ = leftQuotientProjection K (V : Subgroup G) hKV q2 := by
910 (K := (K : Subgroup G)) (H := (p.1.N : Subgroup G))
911 (L := (V : Subgroup G)) (iInf_le (fun r : c => r.1.N) p) hpV q2).symm
912 revert hEqV
913 refine Quotient.inductionOn₂' q1 q2 ?_
914 intro g1 g2 hEqV
915 change QuotientGroup.mk' K (g1⁻¹ * g2) ∈ W
916 have hEqV' :
917 QuotientGroup.mk' (V : Subgroup G) g1 =
918 QuotientGroup.mk' (V : Subgroup G) g2 := by
919 simpa [leftQuotientProjection_mk] using hEqV
920 have hgV : g1⁻¹ * g2 ∈ (V : Subgroup G) := (QuotientGroup.eq).1 hEqV'
921 simpa [V, OpenNormalSubgroup.mem_comap] using hgV
922 have hq1 :
923 q1⁻¹ * q2 = 1 := by
925 (G := G ⧸ K) hmem
926 calc
927 q1 = q1 * 1 := by simp only [mul_one]
928 _ = q1 * (q1⁻¹ * q2) := by rw [hq1]
929 _ = q2 := by simp only [mul_inv_cancel_left]
930 have hstage_mono :
931 ∀ {a b : c} (hAB : a.1 ≤ b.1), stageImage a ⊆ stageImage b := by
932 intro a b hAB q hq
933 rcases hq with ⟨y, rfl⟩
934 refine ⟨⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩, ?_⟩
935 exact (hlift_eq_of_le hAB y).symm
936 have hstage_diff :
937 ∀ {a b : c} (hAB : a.1 ≤ b.1),
938 stageImage b \ stageImage a ⊆
939 {q : G ⧸ K |
941 (iInf_le (fun p : c => p.1.N) a) q = 1} := by
942 intro a b hAB q hq
943 rcases hq.1 with ⟨yb, rfl⟩
944 by_cases hybim : yb.1 ∈ a.1.yImage b.1 (a.1.le_map hAB)
945 · rcases hybim with ⟨y, hyEq⟩
946 have hEq :
947 lift b (b.1.sourceOfY yb) = lift a (a.1.sourceOfY y) := by
948 calc
949 lift b (b.1.sourceOfY yb)
950 = lift b (b.1.sourceOfY
951 ⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩) := by
952 simp only [hyEq, Subtype.coe_eta]
953 _ = lift a (a.1.sourceOfY y) := (hlift_eq_of_le hAB y).symm
954 exact False.elim (hq.2 ⟨y, hEq.symm⟩)
955 · have hybker :
956 leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB) yb.1 = 1 :=
957 a.1.le_map_diff hAB ⟨yb.2, hybim⟩
958 have hqb :
960 (iInf_le (fun p : c => p.1.N) b)
961 (lift b (b.1.sourceOfY yb)) = yb.1 := by
962 calc
964 (iInf_le (fun p : c => p.1.N) b)
965 (lift b (b.1.sourceOfY yb)) = b.1.le_map le_rfl (b.1.sourceOfY yb) := by
966 exact congrFun (hlift_fac b b le_rfl) (b.1.sourceOfY yb)
967 _ = yb.1 := by
968 simpa [QuotientGeneratorConvergingPair.le_map,
969 QuotientGeneratorConvergingPair.le_hBA] using
970 b.1.le_map_right le_rfl (b.1.sourceOfY yb)
971 calc
973 (iInf_le (fun p : c => p.1.N) a)
974 (lift b (b.1.sourceOfY yb))
975 = leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB)
977 (iInf_le (fun p : c => p.1.N) b)
978 (lift b (b.1.sourceOfY yb))) := by
979 exact
981 (K := (K : Subgroup G)) (H := (b.1.N : Subgroup G))
982 (L := (a.1.N : Subgroup G)) (iInf_le (fun p : c => p.1.N) b)
983 (a.1.le_hBA hAB) (lift b (b.1.sourceOfY yb))).symm
984 _ = leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB) yb.1 := by
985 rw [hqb]
986 _ = 1 := hybker
987 let Y : Set (G ⧸ K) := ⋃ a : c, stageImage a
988 have hYcompl : Y ⊆ ({1} : Set (G ⧸ K))ᶜ := by
989 intro q hq
990 rcases mem_iUnion.mp hq with ⟨a, hqa⟩
991 rcases hqa with ⟨y, rfl⟩
992 have hqy :
994 (iInf_le (fun p : c => p.1.N) a)
995 (lift a (a.1.sourceOfY y)) = y.1 := by
996 have hliftProjection := congrFun (hlift_fac a a le_rfl) (a.1.sourceOfY y)
997 calc
999 (iInf_le (fun p : c => p.1.N) a)
1000 (lift a (a.1.sourceOfY y))
1001 = a.1.le_map le_rfl (a.1.sourceOfY y) := by
1002 simpa using hliftProjection
1003 _ = y.1 := by
1004 simpa [QuotientGeneratorConvergingPair.le_map,
1005 QuotientGeneratorConvergingPair.le_hBA] using
1006 a.1.le_map_right le_rfl (a.1.sourceOfY y)
1007 intro hq1
1008 have hq1' : lift a (a.1.sourceOfY y) = 1 := by simpa using hq1
1009 have hy1 : y.1 = 1 := by
1010 calc
1012 (iInf_le (fun p : c => p.1.N) a)
1013 (lift a (a.1.sourceOfY y)) := hqy.symm
1015 (iInf_le (fun p : c => p.1.N) a) 1 := by rw [hq1']
1016 _ = 1 := by rfl
1017 exact a.1.subset_compl y.2 hy1
1018 have hYconv : ConvergesToOne (G := G ⧸ K) Y := by
1019 intro W
1020 let V : OpenSubgroup G :=
1021 OpenSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
1022 have hKV : K ≤ (V : Subgroup G) := by
1023 intro g hg
1024 change QuotientGroup.mk' K g ∈ W
1025 have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=
1026 (QuotientGroup.eq_one_iff (N := K) g).2 hg
1027 rw [hg1]
1028 exact W.one_mem'
1030 (G := G) hc hcn V (by simpa [K] using hKV) with ⟨a, haV⟩
1031 have hstageconv : ConvergesToOne (G := G ⧸ K) (stageImage a) := by
1032 let hGquotA : IsProfiniteGroup (G ⧸ a.1.N) :=
1033 isProfinite_quotient_closedNormal (G := G) hG a.1.closed_N
1034 letI : T2Space (G ⧸ a.1.N) := IsProfiniteGroup.t2Space hGquotA
1035 letI : TotallyDisconnectedSpace (G ⧸ a.1.N) :=
1036 IsProfiniteGroup.totallyDisconnectedSpace hGquotA
1037 simpa [stageImage] using
1038 (ConvergesToOne.range_subtype_pointed
1039 (G := G ⧸ a.1.N) (H := G ⧸ K)
1040 hGquotA (hf := hlift_continuous a) (hf1 := hlift_one a) (hX := a.1.converges))
1041 have hsubset : Y \ (W : Set (G ⧸ K)) ⊆ stageImage a \ (W : Set (G ⧸ K)) := by
1042 intro q hq
1043 rcases hq with ⟨hqY, hqW⟩
1044 rcases mem_iUnion.mp hqY with ⟨b, hbq⟩
1045 by_cases hba : b.1 ≤ a.1
1046 · exact ⟨hstage_mono hba hbq, hqW⟩
1047 · have hcmp : a.1 ≤ b.1 := by
1048 by_cases hEq : a = b
1049 · exact hEq ▸ le_rfl
1050 · rcases hc a.2 b.2 (by
1051 intro h
1052 exact hEq (Subtype.ext h)) with hab | hba'
1053 · exact hab
1054 · exact False.elim (hba hba')
1055 by_cases hqa : q ∈ stageImage a
1056 · exact ⟨hqa, hqW⟩
1057 · have hq1 :
1059 (iInf_le (fun p : c => p.1.N) a) q = 1 :=
1060 hstage_diff hcmp ⟨hbq, hqa⟩
1061 have hqWin : q ∈ W := by
1062 rcases Quotient.exists_rep q with ⟨g, rfl⟩
1063 change QuotientGroup.mk' K g ∈ W
1064 have hgA : g ∈ a.1.N := by
1066 (QuotientGroup.eq_one_iff (N := a.1.N) g).1 hq1
1067 have hgV : g ∈ (V : Subgroup G) := haV hgA
1068 simpa [V, OpenSubgroup.mem_comap] using hgV
1069 exact False.elim (hqW hqWin)
1070 exact (hstageconv W).subset hsubset
1071 have hYgen : TopologicallyGenerates (G := G ⧸ K) Y := by
1072 have hbotclosed : IsClosed ((⊥ : Subgroup (G ⧸ K)) : Set (G ⧸ K)) := by
1073 change IsClosed ({(1 : G ⧸ K)} : Set (G ⧸ K))
1074 simp only [finite_singleton, Finite.isClosed]
1075 have hgen1 :
1076 TopologicallyGenerates (G := G ⧸ K) (Y ∪ ({1} : Set (G ⧸ K))) := by
1078 (G := G ⧸ K) hGquotK
1079 (N := (⊥ : Subgroup (G ⧸ K))) (X := Y)).2
1080 intro W hbotW
1081 let V : OpenNormalSubgroup G :=
1082 OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
1083 have hKV : K ≤ (V : Subgroup G) := by
1084 intro g hg
1085 change QuotientGroup.mk' K g ∈ W
1086 have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=
1087 (QuotientGroup.eq_one_iff (N := K) g).2 hg
1088 rw [hg1]
1089 exact W.one_mem'
1091 (G := G) hc hcn V.toOpenSubgroup (by simpa [K] using hKV) with ⟨a, haV⟩
1092 have hVaClosed : IsClosed ((V : Subgroup G) : Set G) :=
1094 have hmapW :
1095 ((V : Subgroup G).map (QuotientGroup.mk' K)) = (W : Subgroup (G ⧸ K)) := by
1096 ext q
1097 rcases Quotient.exists_rep q with ⟨g, rfl⟩
1098 constructor
1099 · rintro ⟨g', hg'V, hg'q⟩
1100 have : QuotientGroup.mk' K g' ∈ W := by
1101 simpa [V, OpenNormalSubgroup.mem_comap] using hg'V
1102 simpa [hg'q] using this
1103 · intro hgW
1104 refine ⟨g, ?_, rfl⟩
1105 simpa [V, OpenNormalSubgroup.mem_comap] using hgW
1106 let QV : Subgroup (G ⧸ K) := (V : Subgroup G).map (QuotientGroup.mk' K)
1107 let Wmap : OpenNormalSubgroup (G ⧸ K) :=
1108 { toOpenSubgroup :=
1109 { toSubgroup := QV
1110 isOpen' := by
1111 simpa [QV, hmapW] using W.isOpen' }
1112 isNormal' := by
1113 simpa [QV, hmapW] using (show (W : Subgroup (G ⧸ K)).Normal from inferInstance) }
1114 have hWmap : Wmap = W := by
1115 ext q
1116 change q ∈ QV ↔ q ∈ (W : Subgroup (G ⧸ K))
1117 simp only [hmapW, OpenSubgroup.mem_toSubgroup, QV]
1118 let e0 :
1119 ((G ⧸ K) ⧸ QV) ≃ₜ* G ⧸ (V : Subgroup G) :=
1121 (G := G) hG hVaClosed hKclosed hKV
1122 have hstageProj :
1123 ∀ y : a.1.Y,
1124 leftQuotientProjection K (V : Subgroup G) hKV
1125 (lift a (a.1.sourceOfY y)) =
1126 leftQuotientProjection a.1.N (V : Subgroup G) haV y.1 := by
1127 intro y
1128 have hqy0 :=
1129 congrFun (hlift_fac a a le_rfl) (a.1.sourceOfY y)
1130 have hqy :
1132 (iInf_le (fun p : c => p.1.N) a)
1133 (lift a (a.1.sourceOfY y)) = y.1 := by
1134 calc
1136 (iInf_le (fun p : c => p.1.N) a)
1137 (lift a (a.1.sourceOfY y)) = a.1.le_map le_rfl (a.1.sourceOfY y) := by
1138 exact hqy0
1139 _ = y.1 := by
1140 simpa [QuotientGeneratorConvergingPair.le_map,
1141 QuotientGeneratorConvergingPair.le_hBA] using
1142 a.1.le_map_right le_rfl (a.1.sourceOfY y)
1143 calc
1144 leftQuotientProjection K (V : Subgroup G) hKV
1145 (lift a (a.1.sourceOfY y))
1146 = leftQuotientProjection (a.1.N) (V : Subgroup G) haV
1148 (iInf_le (fun p : c => p.1.N) a)
1149 (lift a (a.1.sourceOfY y))) := by
1150 exact
1152 (K := (K : Subgroup G)) (H := (a.1.N : Subgroup G))
1153 (L := (V : Subgroup G)) (iInf_le (fun p : c => p.1.N) a) haV
1154 (lift a (a.1.sourceOfY y))
1155 _ = leftQuotientProjection (a.1.N) (V : Subgroup G) haV y.1 := by
1156 rw [hqy]
1157 have hstageImgEq :
1158 (leftQuotientProjection K (V : Subgroup G) hKV) '' stageImage a =
1159 (leftQuotientProjection a.1.N (V : Subgroup G) haV) '' a.1.Y := by
1160 ext q
1161 constructor
1162 · rintro ⟨x, ⟨y, rfl⟩, rfl⟩
1163 exact ⟨y.1, y.2, (hstageProj y).symm⟩
1164 · rintro ⟨y, hyY, hyq⟩
1165 let y' : a.1.Y := ⟨y, hyY⟩
1166 refine ⟨lift a (a.1.sourceOfY y'), ⟨y', rfl⟩, ?_⟩
1167 calc
1168 leftQuotientProjection K (V : Subgroup G) hKV
1169 (lift a (a.1.sourceOfY y'))
1170 = leftQuotientProjection a.1.N (V : Subgroup G) haV y := by
1171 simpa [y'] using hstageProj y'
1172 _ = q := hyq
1173 have hstageGenV :
1174 TopologicallyGenerates (G := G ⧸ (V : Subgroup G))
1175 ((leftQuotientProjection K (V : Subgroup G) hKV) '' stageImage a) := by
1176 let fV : (G ⧸ a.1.N) →* G ⧸ (V : Subgroup G) :=
1177 { toFun := leftQuotientProjection a.1.N (V : Subgroup G) haV
1178 map_one' := rfl
1179 map_mul' := by
1180 intro x y
1181 refine Quotient.inductionOn₂' x y ?_
1182 intro g h
1183 rfl }
1184 have hgenV :
1185 TopologicallyGenerates (G := G ⧸ (V : Subgroup G))
1186 (fV '' a.1.Y) := by
1188 (G := G ⧸ a.1.N) (H := G ⧸ (V : Subgroup G)) fV
1189 (by
1190 simpa [fV] using
1192 (G := G) (K := a.1.N) (H := (V : Subgroup G)) haV))
1193 (by
1194 simpa [fV] using
1196 (G := G) (K := a.1.N) (H := (V : Subgroup G)) haV))
1197 a.1.generates
1198 rw [hstageImgEq]
1199 simpa [fV] using hgenV
1200 have hquotProj0 :
1201 ∀ y : G ⧸ K,
1202 e0 ((QuotientGroup.mk' QV) y) =
1203 leftQuotientProjection K (V : Subgroup G) hKV y := by
1204 intro y
1205 refine Quotient.inductionOn y ?_
1206 intro g
1207 rfl
1208 have hquotPreimgEq0 :
1209 e0.symm '' ((leftQuotientProjection K (V : Subgroup G) hKV) '' Y) =
1210 (QuotientGroup.mk' QV '' Y) := by
1211 ext q
1212 constructor
1213 · rintro ⟨z, ⟨y, hy, hzy⟩, hqz⟩
1214 refine ⟨y, hy, ?_⟩
1215 have hzq : z = e0 q := by
1216 calc
1217 z = e0 (e0.symm z) := by symm; exact e0.right_inv z
1218 _ = e0 q := by rw [hqz]
1219 have heqy : e0 ((QuotientGroup.mk' QV) y) = z := by
1220 exact (hquotProj0 y).trans hzy
1221 exact e0.injective (heqy.trans hzq)
1222 · rintro ⟨y, hy, rfl⟩
1223 refine ⟨leftQuotientProjection K (V : Subgroup G) hKV y, ⟨y, hy, rfl⟩, ?_⟩
1224 calc
1225 e0.symm (leftQuotientProjection K (V : Subgroup G) hKV y)
1226 = e0.symm (e0 ((QuotientGroup.mk' QV) y)) := by
1227 rw [hquotProj0 y]
1228 _ = QuotientGroup.mk' QV y := e0.left_inv _
1229 have hgenYV :
1230 TopologicallyGenerates (G := G ⧸ (V : Subgroup G))
1231 ((leftQuotientProjection K (V : Subgroup G) hKV) '' Y) := by
1232 exact topologicallyGenerates_mono hstageGenV (by
1233 intro q hq
1234 rcases hq with ⟨x, hx, rfl⟩
1235 exact ⟨x, mem_iUnion.mpr ⟨a, hx⟩, rfl⟩)
1236 have hgenQuot0 :
1237 TopologicallyGenerates (G := ((G ⧸ K) ⧸ QV))
1238 ((QuotientGroup.mk' QV) '' Y) := by
1239 rw [← hquotPreimgEq0]
1241 (G := G ⧸ (V : Subgroup G)) e0.symm hgenYV
1242 have hgenQuotMap :
1244 (G := ((G ⧸ K) ⧸ (Wmap : Subgroup (G ⧸ K))))
1245 ((QuotientGroup.mk' (Wmap : Subgroup (G ⧸ K))) '' Y) := by
1246 simpa [QV, Wmap] using hgenQuot0
1247 have hgenQuot :
1248 TopologicallyGenerates (G := ((G ⧸ K) ⧸ (W : Subgroup (G ⧸ K))))
1249 ((QuotientGroup.mk' (W : Subgroup (G ⧸ K))) '' Y) := by
1250 simpa using (hWmap ▸ hgenQuotMap)
1251 exact hgenQuot
1252 exact (topologicallyGenerates_union_one_iff (G := G ⧸ K) (X := Y)).1 hgen1
1253 refine ⟨{ N := K
1254 normal_N := inferInstance
1255 closed_N := hKclosed
1256 Y := Y
1257 subset_compl := hYcompl
1258 converges := hYconv
1259 generates := hYgen }, ?_⟩
1260 intro a ha
1261 let a' : c := ⟨a, ha⟩
1262 refine ⟨iInf_le (fun p : c => p.1.N) a', lift a', ?_, ?_, ?_, ?_, ?_⟩
1263 · exact hlift_continuous a'
1264 · intro x
1265 have hliftProjection := congrFun (hlift_fac a' a' le_rfl) x
1266 calc
1267 leftQuotientProjection K a.N (iInf_le (fun p : c => p.1.N) a')
1268 (lift a' x) = a.le_map le_rfl x := by
1269 simpa using hliftProjection
1270 _ = x.1 := by
1271 simpa [QuotientGeneratorConvergingPair.le_map,
1272 QuotientGeneratorConvergingPair.le_hBA] using
1273 a.le_map_right le_rfl x
1274 · exact hlift_one a'
1275 · intro y
1276 exact mem_iUnion.mpr ⟨a', ⟨y, rfl⟩⟩
1277 · intro q hq
1278 rcases mem_iUnion.mp hq.1 with ⟨b, hbq⟩
1279 by_cases hba : b.1 ≤ a
1280 · exact False.elim (hq.2 (hstage_mono (a := b) (b := a') hba hbq))
1281 · have hab : a ≤ b.1 := by
1282 by_cases hEq : a = b.1
1283 · exact hEq ▸ le_rfl
1284 · rcases hc ha b.2 (by
1285 intro h
1286 exact hEq h) with hab | hba'
1287 · exact hab
1288 · exact False.elim (hba hba')
1289 exact hstage_diff (a := a') (b := b) hab ⟨hbq, hq.2⟩
1291/-- 4.4. Existence theorem used by the public theorem.
1294 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X := by
1295 classical
1297 letI : Nonempty Pair := ⟨quotientGeneratorPairTop (G := G)⟩
1298 obtain ⟨m, hmmax⟩ := zorn_le_nonempty (α := Pair) <| by
1299 intro c hc hcn
1301 ⟨ub, hub⟩
1302 exact ⟨ub, hub⟩
1303 have hmbot : m.N = ⊥ := by
1304 by_contra hne
1306 ⟨m', hmm', hm'm⟩
1307 exact hm'm (hmmax hmm')
1308 exact ⟨m.toAmbientSet hG, m.toAmbientSet_generatesAndConvergesToOne hG hmbot⟩
1311section DerivedAPI
1313/-- A surjective continuous homomorphism preserves generating sets converging to `1`. -/
1314theorem GeneratesAndConvergesToOne.image_of_continuousSurjective
1316 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
1317 (f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
1318 {X : Set G} (hX : GeneratesAndConvergesToOne (G := G) X) :
1319 GeneratesAndConvergesToOne (G := H) (f '' X) := by
1320 refine ⟨?_, ?_⟩
1322 (G := G) (H := H) f hf hfsurj hX.1
1323 · exact ConvergesToOne.image_of_continuous_pointed
1324 (G := G) (H := H) hG hf (by simp only [map_one]) hX.2
1326/-- A continuous multiplicative equivalence preserves generating sets converging to `1`. -/
1327theorem GeneratesAndConvergesToOne.image_of_continuousMulEquiv
1329 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
1330 (e : G ≃ₜ* H) {X : Set G}
1331 (hX : GeneratesAndConvergesToOne (G := G) X) :
1332 GeneratesAndConvergesToOne (G := H) (e '' X) := by
1333 refine ⟨?_, ?_⟩
1335 (G := G) e hX.1
1336 · exact ConvergesToOne.image_of_continuous_pointed
1337 (G := G) (H := H) hG e.continuous (by simp only [Homeomorph.homeomorph_mk_coe, ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,
1338 EquivLike.coe_coe, map_one]) hX.2
1340/-- A continuous multiplicative equivalence preserves and reflects convergence to `1`. -/
1341theorem ConvergesToOne.image_of_continuousMulEquiv_iff
1343 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
1345 (e : G ≃ₜ* H) {X : Set G} :
1346 ConvergesToOne (G := H) (e '' X) ↔ ConvergesToOne (G := G) X := by
1347 constructor
1348 · intro h
1349 have hback : ConvergesToOne (G := G) (e.symm '' (e '' X)) :=
1350 ConvergesToOne.image_of_continuous_pointed
1351 (G := H) (H := G) hH e.symm.continuous (by simp only [Homeomorph.homeomorph_mk_coe, ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,
1352 EquivLike.coe_coe, map_one]) (X := e '' X) h
1353 have himage : e.symm '' (e '' X) = X := by
1354 ext x
1355 constructor
1356 · rintro ⟨y, ⟨z, hz, rfl⟩, rfl⟩
1357 simpa using hz
1358 · intro hx
1359 exact ⟨e x, ⟨x, hx, rfl⟩, by simp only [ContinuousMulEquiv.symm_apply_apply]⟩
1360 simpa [himage] using hback
1361 · intro h
1362 exact ConvergesToOne.image_of_continuous_pointed
1363 (G := G) (H := H) hG e.continuous (by simp only [Homeomorph.homeomorph_mk_coe, ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,
1364 EquivLike.coe_coe, map_one]) h
1366/-- A continuous multiplicative equivalence preserves and reflects the combined predicate. -/
1367theorem GeneratesAndConvergesToOne.image_of_continuousMulEquiv_iff
1369 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
1371 (e : G ≃ₜ* H) {X : Set G} :
1372 GeneratesAndConvergesToOne (G := H) (e '' X) ↔ GeneratesAndConvergesToOne (G := G) X := by
1373 constructor
1374 · intro h
1375 exact ⟨
1376 (topologicallyGenerates_continuousMulEquiv_image_iff (G := G) (H := H) e (X := X)).1 h.1,
1377 (ConvergesToOne.image_of_continuousMulEquiv_iff
1378 (G := G) (H := H) hG hH e (X := X)).1 h.2⟩
1379 · intro h
1380 exact ⟨
1381 (topologicallyGenerates_continuousMulEquiv_image_iff (G := G) (H := H) e (X := X)).2 h.1,
1382 (ConvergesToOne.image_of_continuousMulEquiv_iff
1383 (G := G) (H := H) hG hH e (X := X)).2 h.2⟩
1387 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
1388 (hH : IsProfiniteGroup H) (e : G ≃ₜ* H) :
1390 apply le_antisymm
1391 · rcases exists_generatorsConvergingToOne (G := H) hH with ⟨Y, hY⟩
1393 (G := H) ⟨Y, hY⟩ with
1394 ⟨Ymin, hYmin, hYcard⟩
1395 calc
1396 topologicalRank G ≤ Cardinal.mk (e.symm '' Ymin) := by
1398 (G := G)
1399 (GeneratesAndConvergesToOne.image_of_continuousMulEquiv
1400 (G := H) hH e.symm hYmin)
1401 _ ≤ Cardinal.mk Ymin := Cardinal.mk_image_le
1402 _ = topologicalRank H := hYcard
1403 · rcases exists_generatorsConvergingToOne (G := G) hG with ⟨X, hX⟩
1405 (G := G) ⟨X, hX⟩ with
1406 ⟨Xmin, hXmin, hXcard⟩
1407 calc
1408 topologicalRank H ≤ Cardinal.mk (e '' Xmin) := by
1410 (G := H)
1411 (GeneratesAndConvergesToOne.image_of_continuousMulEquiv
1412 (G := G) hG e hXmin)
1413 _ ≤ Cardinal.mk Xmin := Cardinal.mk_image_le
1414 _ = topologicalRank G := hXcard
1416end DerivedAPI
1418end Generators
1420end ProCGroups.Generation