ReidemeisterSchreier/Profinite/OpenSubgroups/BasisTheorems.lean
1import ProCGroups.Completion.FiniteQuotientLifts
2import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
3import ReidemeisterSchreier.Profinite.OpenSubgroups.ExactRightSchreierGeneration
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/BasisTheorems.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Profinite open-subgroup Schreier theory
16Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.
17-/
19open scoped Topology Pointwise
21namespace ReidemeisterSchreier
22namespace Profinite
24open ProCGroups
25open ProCGroups.FreeProC
26open ProCGroups.ProC
28universe u
31/-- Finite-discrete quotient lift property for a dense abstract Schreier model of an open
32subgroup. -/
34 (C : ProCGroups.FiniteGroupClass.{u})
35 {F : Type u} [Group F] [TopologicalSpace F]
36 (H : OpenSubgroup F)
37 {Y : Type u}
38 (φY : FreeGroup Y →* ↥(H : Subgroup F)) : Prop :=
39 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
40 [Finite Q] [DiscreteTopology Q],
41 C Q →
42 ∀ ψQ : FreeGroup Y →* Q,
43 ∃! φbar : ↥(H : Subgroup F) →* Q,
44 Continuous φbar ∧ φbar.comp φY = ψQ
46/-- Transport the finite-quotient lift property across an abstract free-group equivalence. -/
48 (C : ProCGroups.FiniteGroupClass.{u})
49 {F : Type u} [Group F] [TopologicalSpace F]
50 (H : OpenSubgroup F)
51 {L : Type u} [Group L]
52 {Y : Type u}
53 (eY : FreeGroup Y ≃* L)
54 (ψ : L →* ↥(H : Subgroup F))
55 (hψfinite :
56 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
57 [Finite Q] [DiscreteTopology Q],
58 C Q →
59 ∀ χL : L →* Q,
60 ∃! φbar : ↥(H : Subgroup F) →* Q,
61 Continuous φbar ∧ φbar.comp ψ = χL) :
63 (C := C) H (ψ.comp eY.toMonoidHom) := by
64 intro Q _ _ _ _ _ hQ ψQ
65 let χL : L →* Q := ψQ.comp eY.symm.toMonoidHom
66 have hχLFac : χL.comp eY.toMonoidHom = ψQ := by
67 apply MonoidHom.ext
68 intro w
69 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
70 MulEquiv.symm_apply_apply, χL]
71 rcases hψfinite hQ χL with ⟨φbar, hφbar, hφbarUnique⟩
72 refine ⟨φbar, ?_, ?_⟩
73 · refine ⟨hφbar.1, ?_⟩
74 apply MonoidHom.ext
75 intro w
76 calc
77 (φbar.comp (ψ.comp eY.toMonoidHom)) w = (φbar.comp ψ) (eY w) := rfl
78 _ = χL (eY w) := by
79 exact congrArg (fun f : L →* Q => f (eY w)) hφbar.2
80 _ = ψQ w := by
81 exact congrArg (fun f : FreeGroup Y →* Q => f w) hχLFac
82 · intro φbar' hφbar'
83 apply hφbarUnique
84 refine ⟨hφbar'.1, ?_⟩
85 apply MonoidHom.ext
86 intro l
87 rcases eY.surjective l with ⟨w, rfl⟩
88 have hw' :
89 (φbar'.comp (ψ.comp eY.toMonoidHom)) w = ψQ w :=
90 congrArg (fun f : FreeGroup Y →* Q => f w) hφbar'.2
91 calc
92 (φbar'.comp ψ) (eY w) = (φbar'.comp (ψ.comp eY.toMonoidHom)) w := rfl
93 _ = ψQ w := hw'
94 _ = χL (eY w) := by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
95 MulEquiv.symm_apply_apply, χL]
97/-- A dense abstract Schreier model with the finite-discrete quotient lift property is the
98pro-`C` completion of that abstract free group. -/
100 (C : ProCGroups.FiniteGroupClass.{u})
101 (hForm : ProCGroups.FiniteGroupClass.Formation C)
102 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
103 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
104 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
105 {X : Type u}
106 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
107 {ι : X → F}
109 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
110 (H : OpenSubgroup F)
111 {Y : Type u}
112 [TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
113 [DiscreteTopology (FreeGroup Y)]
114 {φY : FreeGroup Y →ₜ* ↥(H : Subgroup F)}
115 (hφYdense : DenseRange φY)
116 (hfinite :
117 DenseAbstractSchreierFiniteQuotientLiftProperty (C := C) H φY.toMonoidHom) :
120 (FreeGroup Y) ↥(H : Subgroup F) φY := by
121 have hHproC : ProCGroups.ProC.IsProCGroup C ↥(H : Subgroup F) := by
122 exact
124 (C := C) hIso hSub hQuot hF.isProC (H : Subgroup F)
125 (Subgroup.isClosed_of_isOpen (H : Subgroup F) H.isOpen')
127 (C := C) (hForm := hForm) (G := FreeGroup Y) (Ghat := ↥(H : Subgroup F))
128 hHproC (ι := φY) hφYdense ?_
129 intro Q _ _ _ _ _ hQ ψQ
130 rcases hfinite hQ ψQ.toMonoidHom with ⟨φbar, hφbar, hφbarUnique⟩
131 let φbarCont : ↥(H : Subgroup F) →ₜ* Q :=
132 { toMonoidHom := φbar
133 continuous_toFun := hφbar.1 }
134 refine ⟨φbarCont, ?_, ?_⟩
135 · apply ContinuousMonoidHom.toMonoidHom_injective
136 exact hφbar.2
137 · intro φbarCont' hφbarCont'
138 apply ContinuousMonoidHom.toMonoidHom_injective
139 exact hφbarUnique φbarCont'.toMonoidHom
140 ⟨φbarCont'.continuous_toFun, congrArg ContinuousMonoidHom.toMonoidHom hφbarCont'⟩
144/-- A topologically generating subset of an open subgroup generates a dense subgroup after
145including it into the ambient group. -/
147 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
148 (H : OpenSubgroup G)
149 {S : Set ↥(H : Subgroup G)}
150 (hS : Generation.TopologicallyGenerates (G := ↥(H : Subgroup G)) S) :
151 (H : Subgroup G) ≤
152 (Subgroup.closure (((↑) : ↥(H : Subgroup G) → G) '' S)).topologicalClosure := by
153 let D : Subgroup ↥(H : Subgroup G) := Subgroup.closure S
154 have hDense : Dense (D : Set ↥(H : Subgroup G)) :=
155 (Generation.topologicallyGenerates_iff_dense (G := ↥(H : Subgroup G)) (X := S)).1 hS
156 rw [Subtype.dense_iff] at hDense
157 have hmap :
159 Subgroup.closure (((↑) : ↥(H : Subgroup G) → G) '' S) := by
160 simpa [TopologicalGroup.image_subtype_eq_map] using ((H : Subgroup G).subtype.map_closure S)
161 have himage :
162 ((↑) : ↥(H : Subgroup G) → G) '' (D : Set ↥(H : Subgroup G)) =
164 exact TopologicalGroup.image_subtype_eq_map (H : Subgroup G).subtype D
165 intro g hg
166 have hg' :
168 have : g ∈ closure (((↑) : ↥(H : Subgroup G) → G) '' (D : Set ↥(H : Subgroup G))) :=
169 hDense hg
170 rwa [himage] at this
171 have hg'' :
172 g ∈ ((D.map (H : Subgroup G).subtype).topologicalClosure : Set G) := by
173 simpa [Subgroup.topologicalClosure_coe] using hg'
174 simpa [hmap] using hg''
177 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
178 [CompactSpace G]
179 (H : OpenSubgroup G)
180 (hH : ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated ↥(H : Subgroup G)) :
182 classical
183 rcases hH with ⟨sH, hsH⟩
184 letI : Finite (OpenSubgroupRightQuotient H) :=
185 finite_openSubgroupRightQuotient (F := G) H
186 letI : Fintype (OpenSubgroupRightQuotient H) :=
187 Fintype.ofFinite (OpenSubgroupRightQuotient H)
188 let τ := openSubgroupRightCosetSection (F := G) H
189 let sReps : Finset G := Finset.univ.image τ
190 let s : Finset G := sReps ∪ sH.image Subtype.val
191 let K : Subgroup G := Subgroup.closure (s : Set G)
192 have hHle' :
193 (H : Subgroup G) ≤
194 (Subgroup.closure
195 (((↑) : ↥(H : Subgroup G) → G) ''
196 ((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G)))).topologicalClosure :=
197 subgroup_le_topologicalClosure_of_topologicallyGenerates_local H (by simpa using hsH)
198 have hImageLe : Subgroup.closure
199 (((↑) : ↥(H : Subgroup G) → G) ''
200 ((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G))) ≤ K := by
201 refine Subgroup.closure_mono ?_
202 intro g hg
203 rcases hg with ⟨x, hx, rfl⟩
204 have hx' : (x : G) ∈ sH.image Subtype.val := by
205 exact Finset.mem_image.mpr ⟨x, by simpa using hx, rfl⟩
206 exact Finset.mem_coe.2 (Finset.mem_union_right sReps hx')
207 have hImageLe' :
208 (Subgroup.closure
209 (((↑) : ↥(H : Subgroup G) → G) ''
210 ((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G)))).topologicalClosure ≤
211 K.topologicalClosure :=
212 Subgroup.topologicalClosure_minimal _
213 (hImageLe.trans (Subgroup.le_topologicalClosure _))
214 (Subgroup.isClosed_topologicalClosure _)
215 have hHle : (H : Subgroup G) ≤ K.topologicalClosure := fun g hg => hImageLe' (hHle' hg)
216 have htop : K.topologicalClosure = ⊤ := by
217 apply top_unique
218 intro g _hg
219 let q : OpenSubgroupRightQuotient H := openSubgroupRightCoset H g
220 have hEq0 : openSubgroupRightCoset H (τ q) = q :=
221 openSubgroupRightCosetSection_spec (F := G) H q
222 have hEq :
223 openSubgroupRightCoset H g = openSubgroupRightCoset H (τ q) := by
224 simpa [q] using hEq0.symm
225 have hrel : QuotientGroup.rightRel (H : Subgroup G) g (τ q) :=
226 Quotient.exact' hEq
227 have hgH0 : τ q * g⁻¹ ∈ (H : Subgroup G) := by
228 simpa using (QuotientGroup.rightRel_apply.mp hrel)
229 have hgH : g * (τ q)⁻¹ ∈ (H : Subgroup G) := by
230 simpa [mul_inv_rev, mul_assoc] using ((H : Subgroup G).inv_mem hgH0)
231 have hgH' : g * (τ q)⁻¹ ∈ (K.topologicalClosure : Subgroup G) :=
232 hHle hgH
233 have hτK : τ q ∈ (K.topologicalClosure : Subgroup G) := by
234 have hτmem : τ q ∈ (sReps : Set G) := by
235 exact Finset.mem_coe.2 <| Finset.mem_image.mpr ⟨q, Finset.mem_univ q, rfl⟩
236 have hτmem' : τ q ∈ (s : Set G) := by
237 exact Finset.mem_coe.2 (Finset.mem_union_left _ hτmem)
238 exact Subgroup.le_topologicalClosure K (Subgroup.subset_closure hτmem')
239 have hmul :
240 (g * (τ q)⁻¹) * τ q ∈ (K.topologicalClosure : Subgroup G) :=
241 (K.topologicalClosure).mul_mem hgH' hτK
242 simpa [mul_assoc] using hmul
243 refine ⟨s, ?_⟩
244 simpa [Generation.TopologicallyGenerates, K, s] using htop
248/-- A finite converging-set free pro-`C` basis realizes the pro-`C` completion of the abstract
249free group on the same basis. -/
251 {C : ProCGroups.FiniteGroupClass.{u}}
252 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
253 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
254 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
255 {X : Type u} [Finite X]
256 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
257 [DiscreteTopology (FreeGroup X)]
258 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
259 {ι : X → F}
261 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
264 (FreeGroup X) F
265 { toMonoidHom := FreeGroup.lift ι
266 continuous_toFun := continuous_of_discreteTopology } := by
267 let φ : FreeGroup X →ₜ* F :=
268 { toMonoidHom := FreeGroup.lift ι
269 continuous_toFun := continuous_of_discreteTopology }
271 (ProCGroups.ProC.finiteGroupClassProCPredicate C) (FreeGroup X) F φ
272 refine
274 denseRange := ?_
275 existsUnique_lift := ?_ }
276 · simpa [φ] using
278 (F := F) (X := X) hF.generates_range
279 · intro G _ _ _ hG ψ
280 let φX : X → G := fun x => ψ (FreeGroup.of x)
281 let S : Subgroup G := (Subgroup.closure (Set.range φX)).topologicalClosure
282 have hSproC : ProCGroups.ProC.IsProCGroup C S := by
283 exact
285 (C := C) hIso hSub hQuot hG S (Subgroup.isClosed_topologicalClosure _)
286 let φS : X → S := fun x =>
287 ⟨φX x, Subgroup.le_topologicalClosure _
288 (Subgroup.subset_closure ⟨x, rfl⟩)⟩
289 have hφSconv : FamilyConvergesToOne (G := S) φS := by
290 exact FamilyConvergesToOne.of_finite_domain (G := S) φS
291 have hφSgen :
292 Generation.TopologicallyGenerates (G := S) (Set.range φS) := by
293 simpa [S, φS, φX] using
295 rcases hF.existsUnique_lift hSproC φS hφSconv hφSgen with
296 ⟨σS, hσS, _⟩
297 let σ : F →ₜ* G :=
298 { toMonoidHom := S.subtype.comp σS
299 continuous_toFun := by
300 simpa using continuous_subtype_val.comp hσS.1 }
301 have hσfac : σ.comp φ = ψ := by
302 apply ContinuousMonoidHom.toMonoidHom_injective
303 apply FreeGroup.ext_hom
304 intro x
305 change (S.subtype.comp σS) (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x)
306 simpa [φS, φX] using congrArg Subtype.val (hσS.2 x)
307 refine ⟨σ, hσfac, ?_⟩
308 intro g hg
309 letI : T2Space G := ProCGroups.ProC.IsProCGroup.t2Space hG
310 apply ContinuousMonoidHom.toMonoidHom_injective
312 (G := F) (A := G) hF.generates_range g.continuous_toFun σ.continuous_toFun
313 intro y hy
314 rcases hy with ⟨x, rfl⟩
315 have hσx := congrArg (fun k : FreeGroup X →ₜ* G => k (FreeGroup.of x)) hσfac
316 have hgx := congrArg (fun k : FreeGroup X →ₜ* G => k (FreeGroup.of x)) hg
317 have hσx' : σ (ι x) = ψ (FreeGroup.of x) := by
318 change σ (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x) at hσx
319 simpa using hσx
320 have hgx' : g (ι x) = ψ (FreeGroup.of x) := by
321 change g (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x) at hgx
322 simpa using hgx
323 exact hgx'.trans hσx'.symm
325/-- If a finite exact generating family has the same cardinality as an abstract free model whose
326completion is the target, then that exact family realizes the same pro-`C` completion. -/
328 {C : ProCGroups.FiniteGroupClass.{u}}
329 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
330 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
331 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
332 (hcyc :
333 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
334 C A ∧ IsCyclic A ∧ Nontrivial A)
335 {n : ℕ}
336 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
337 {Y : Type u}
338 [TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
339 [DiscreteTopology (FreeGroup Y)]
340 [TopologicalSpace (FreeGroup (ULift.{u} (Fin n)))]
341 [IsTopologicalGroup (FreeGroup (ULift.{u} (Fin n)))]
342 [DiscreteTopology (FreeGroup (ULift.{u} (Fin n)))]
343 (hYcard : Nat.card Y = n)
344 {φY : FreeGroup Y →ₜ* H}
345 (hCompY :
347 (ProCGroups.ProC.finiteGroupClassProCPredicate C) (FreeGroup Y) H φY)
348 {κ : ULift.{u} (Fin n) → H}
349 (hκ : Generation.GeneratesAndConvergesToOne (G := H) (Set.range κ)) :
352 (FreeGroup (ULift.{u} (Fin n))) H
353 { toMonoidHom := FreeGroup.lift κ
354 continuous_toFun := continuous_of_discreteTopology } := by
355 have hYfin : Finite Y := by
356 by_cases h0 : n = 0
357 · have hY0 : Nat.card Y = 0 := by rw [hYcard, h0]
358 letI : CompactSpace H := ProCGroups.ProC.IsProCGroup.compactSpace hCompY.isProC
359 letI : T2Space H := ProCGroups.ProC.IsProCGroup.t2Space hCompY.isProC
360 letI : TotallyDisconnectedSpace H :=
361 ProCGroups.ProC.IsProCGroup.totallyDisconnectedSpace hCompY.isProC
362 haveI : IsEmpty (ULift.{u} (Fin n)) := by
363 rw [h0]
364 infer_instance
365 have hκrange : Set.range κ = (∅ : Set H) := by
366 ext z
367 constructor
368 · rintro ⟨x, rfl⟩
369 exact isEmptyElim x
370 · intro hz
371 simp only [Set.mem_empty_iff_false] at hz
372 have hHtriv : ∀ x : H, x = 1 := by
373 intro x
374 have hxmem :
375 x ∈ ((Subgroup.closure (Set.range κ)).topologicalClosure : Set H) := by
376 have hκgen : Generation.TopologicallyGenerates (G := H) (Set.range κ) := hκ.1
377 rw [Generation.TopologicallyGenerates] at hκgen
378 rw [hκgen]
379 simp only [Subgroup.coe_top, Set.mem_univ]
380 have hxmem' :
381 x ∈ ((Subgroup.closure ((∅ : Set H))).topologicalClosure : Set H) := by
382 simpa [hκrange] using hxmem
383 simpa [Subgroup.coe_topologicalClosure_bot, closure_singleton] using hxmem'
384 have hYempty : IsEmpty Y := by
385 refine ⟨fun y => ?_⟩
386 rcases
388 C hQuot hcyc with
389 ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, _hgena⟩
390 let ψY : FreeGroup Y →ₜ* A :=
391 { toMonoidHom := FreeGroup.lift (fun _ : Y => a)
392 continuous_toFun := continuous_of_discreteTopology }
393 have hψYne : ψY (FreeGroup.of y) ≠ 1 := by
394 change FreeGroup.lift (fun _ : Y => a) (FreeGroup.of y) ≠ 1
395 simpa using ha1
396 rcases hCompY.existsUnique_lift hA ψY with
397 ⟨σ, hσ, _⟩
398 have hyfac :=
399 congrArg (fun f : FreeGroup Y →ₜ* A => f (FreeGroup.of y)) hσ
400 have hyEq : ψY (FreeGroup.of y) = 1 := by
401 calc
402 ψY (FreeGroup.of y) = σ (φY (FreeGroup.of y)) := hyfac.symm
403 _ = σ 1 := by rw [hHtriv (φY (FreeGroup.of y))]
405 exact hψYne hyEq
406 letI : IsEmpty Y := hYempty
407 infer_instance
408 · exact Nat.finite_of_card_ne_zero (α := Y) (by rw [hYcard]; exact h0)
409 letI : Finite Y := hYfin
410 have hFreeY :
412 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
413 Y H (fun y => φY (FreeGroup.of y)) := by
414 exact
416 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
417 (X := Y) (Fhat := H) (ι := φY) hCompY
418 have hcard :
419 Cardinal.mk Y = Cardinal.mk (ULift.{u} (Fin n)) := by
420 exact Cardinal.mk_congr ((Finite.equivFinOfCardEq hYcard).trans Equiv.ulift.symm)
421 have hFreeκ :
423 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
424 (ULift.{u} (Fin n)) H κ := by
425 exact
427 (C := C) (X := Y) (Y := ULift.{u} (Fin n)) hFreeY hcard hκ.1
428 exact
430 (C := C) hSub hIso hQuot hFreeκ
434/-- Compact pointed basis bridge: adjoining the point at infinity to a discrete converging basis,
435the open subgroup inherits a compact pointed right Schreier basis. -/
437 (C : ProCGroups.FiniteGroupClass.{u})
438 (hForm : ProCGroups.FiniteGroupClass.Formation C)
439 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
440 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
441 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
442 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
443 {X : Type u}
444 [TopologicalSpace X] [DiscreteTopology X]
445 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
446 {ι : X → F}
448 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
449 (H : OpenSubgroup F) :
450 ∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
451 Continuous κ ∧
452 (∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
453 κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
455 IsClosed (Set.range κ) ∧
457 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
458 (Set.range κ)
459 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
460 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
461 ↥(H : Subgroup F) Subtype.val := by
462 classical
463 let iInf : OnePoint X → F := fun z => z.elim 1 ι
464 have hιTendsto : Filter.Tendsto ι Filter.cofinite (𝓝 (1 : F)) := by
465 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
466 letI : T2Space F := IsProCGroup.t2Space hF.isProC
467 letI : TotallyDisconnectedSpace F := IsProCGroup.totallyDisconnectedSpace hF.isProC
468 rw [Filter.tendsto_def]
469 intro s hs
470 rcases mem_nhds_iff.mp hs with ⟨W, hWs, hWopen, h1W⟩
472 (G := F) hWopen h1W with
473 ⟨U, hUW⟩
474 have hfinite : {x : X | ι x ∉ (U : Set F)}.Finite :=
475 hF.convergesToOne U.toOpenSubgroup
476 have hcof : ∀ᶠ x : X in Filter.cofinite, ι x ∈ (U : Set F) :=
477 Filter.eventually_cofinite.2 hfinite
478 exact hcof.mono fun x hx => hWs (hUW hx)
479 have hPointed :
481 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
482 (OnePoint X) OnePoint.infty F iInf := by
483 refine ⟨hF.isProC, ?_, by simp only [OnePoint.elim_infty, iInf], ?_, ?_⟩
484 · rw [OnePoint.continuous_iff_from_discrete]
485 simpa [iInf] using hιTendsto
486 · have hsub : Set.range ι ⊆ Set.range iInf := by
487 rintro y ⟨x, rfl⟩
488 exact ⟨(x : OnePoint X), rfl⟩
489 exact Generation.topologicallyGenerates_mono (G := F) hF.generates_range hsub
490 · intro G _ _ _ hG φ hφ hφ0 hgenφ
491 let ψ : X → G := fun x => φ x
492 have hψTendsto : Filter.Tendsto ψ Filter.cofinite (𝓝 (1 : G)) := by
493 have hraw := (OnePoint.continuous_iff_from_discrete (f := φ)).1 hφ
494 simpa [ψ, hφ0] using hraw
495 have hψconv : FamilyConvergesToOne (G := G) ψ := by
496 intro U
497 exact Filter.eventually_cofinite.mp <|
498 hψTendsto (U.isOpen'.mem_nhds U.one_mem')
499 have hφrange : Set.range φ = Set.range ψ ∪ ({1} : Set G) := by
500 ext z
501 constructor
502 · rintro ⟨x, rfl⟩
503 refine OnePoint.rec ?_ ?_ x
504 · right
505 simpa [iInf] using hφ0
506 · intro y
507 left
508 exact ⟨y, rfl⟩
509 · intro hz
510 rcases hz with hz | hz
511 · rcases hz with ⟨y, rfl⟩
512 exact ⟨(y : OnePoint X), rfl⟩
513 · exact ⟨OnePoint.infty, hφ0.trans hz.symm⟩
514 have hψgen : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
515 have hgenφ' :
516 Generation.TopologicallyGenerates (G := G) (Set.range ψ ∪ ({1} : Set G)) := by
517 simpa [hφrange] using hgenφ
518 exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range ψ)).1
519 hgenφ'
520 rcases hF.existsUnique_lift hG ψ hψconv hψgen with ⟨f, hf, huniq⟩
521 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
522 · intro x
523 refine OnePoint.rec ?_ ?_ x
524 · calc
525 f (iInf OnePoint.infty) = f 1 := rfl
527 _ = φ OnePoint.infty := hφ0.symm
528 · intro y
529 exact hf.2 y
530 · intro g hg
531 apply huniq g
532 refine ⟨hg.1, ?_⟩
533 intro y
534 simpa [iInf, ψ] using hg.2 (y : OnePoint X)
535 exact
537 (C := C) hForm hSub hIso hQuot hExt hPointed H
539/-- An open subgroup of a compact pointed free pro-`C` group admits a free pro-`C` model on a set
540converging to `1`, assuming the standard pointed-to-converging-set basis bridge for `ProC`.
542The Schreier part of the proof is the explicit right Schreier family from
543`exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup`; the final conversion is delegated
544to the ProCGroups bridge rather than wrapped in project-specific vocabulary. -/
546 {C : ProCGroups.FiniteGroupClass.{u}}
547 (hForm : ProCGroups.FiniteGroupClass.Formation C)
548 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
549 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
550 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
551 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
552 (hBridge :
554 {X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
555 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
556 {ι : X → F}
557 (hF : IsPointedFreeProCGroupOn
558 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X x0 F ι)
559 (H : OpenSubgroup F) :
560 ∃ Fdata : FreeProCGroupOnConvergingSetData
561 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
562 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) := by
563 rcases
565 (C := C) hForm hSub hIso hQuot hExt hF H with
566 ⟨κ, _hκcont, _hκbase, _hκone, _hκcompact, _hκclosed, hκfree⟩
567 exact hBridge hκfree
569/-- Converging-set version of the open-subgroup basis theorem under the finite-class closure
570bundle. -/
572 (C : ProCGroups.FiniteGroupClass.{u})
573 (hForm : ProCGroups.FiniteGroupClass.Formation C)
574 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
575 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
576 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
577 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
578 (hBridge :
580 {X : Type u}
581 [TopologicalSpace X] [DiscreteTopology X]
582 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
583 {ι : X → F}
585 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
586 (H : OpenSubgroup F) :
587 ∃ Fdata : FreeProCGroupOnConvergingSetData
588 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
589 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) := by
590 rcases
592 C hForm hSub hIso hQuot hExt hF H with
593 ⟨κ, _hκcont, _hκbase, _hκone, _hκcompact, _hκclosed, hκfree⟩
594 exact hBridge hκfree
596/-- Extension-closed variety case, phrased directly with ProCGroups finite-class closure data. -/
598 (C : ProCGroups.FiniteGroupClass.{u})
599 (hBridge :
601 (hVar : ProCGroups.FiniteGroupClass.Variety C)
602 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
603 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
604 {X : Type u}
605 [TopologicalSpace X] [DiscreteTopology X]
606 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
607 {ι : X → F}
609 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
610 (H : OpenSubgroup F) :
611 ∃ Fdata : FreeProCGroupOnConvergingSetData
612 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
613 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) := by
614 rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
615 ⟨hForm, hSub, hIso', hQuot, hExt'⟩
616 exact
618 C hForm hSub hIso' hQuot hExt' hBridge hF H
620/-- Melnikov-formation variant with explicit subgroup closure. The conclusion is stated for an
621arbitrary open subgroup because the ProCGroups closure bundle is already strong enough for the
622Schreier argument. -/
624 (C : ProCGroups.FiniteGroupClass.{u})
625 (hBridge :
628 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
629 {X : Type u}
630 [TopologicalSpace X] [DiscreteTopology X]
631 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
632 {ι : X → F}
634 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
635 (H : OpenSubgroup F) :
636 ∃ Fdata : FreeProCGroupOnConvergingSetData
637 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
638 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) := by
639 rcases hC.closureBundle_of_subgroupClosed hSub with
640 ⟨hForm, hSub', hIso, hQuot, hExt⟩
641 exact
643 C hForm hSub' hIso hQuot hExt hBridge hF H
647end Profinite
648end ReidemeisterSchreier