Yamaguchi Lean 4 Library
Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
ProCGroups/ReidemeisterSchreier/Profinite/OpenSubgroups/BasisTheorems/Source

Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems

1import ProCGroups.Completion.FiniteQuotientLifts
2import ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
3import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.ExactRightSchreierGeneration
5/-!
6# From exact Schreier generators to free pro-\(C\) bases
8This module turns the exact right-Schreier generation theorem into completion
9and basis statements. It isolates finite-quotient lifting, compares dense
10abstract free groups with their pro-\(C\) completions, and constructs compact
11pointed and converging-set bases for open subgroups.
12-/
14open scoped Topology Pointwise
16namespace ReidemeisterSchreier
17namespace Profinite
19open ProCGroups
20open ProCGroups.FreeProC
21open ProCGroups.ProC
23universe u
26/--
27Finite-discrete quotient lift property for a dense abstract Schreier model of an open subgroup.
28-/
29def DenseAbstractSchreierFiniteQuotientLiftProperty
30 (C : ProCGroups.FiniteGroupClass.{u})
31 {F : Type u} [Group F] [TopologicalSpace F]
32 (H : OpenSubgroup F)
33 {Y : Type u}
34 (φY : FreeGroup Y →* ↥(H : Subgroup F)) : Prop :=
35 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
36 [Finite Q] [DiscreteTopology Q],
37 C Q →
38 ∀ ψQ : FreeGroup Y →* Q,
39 ∃! φbar : ↥(H : Subgroup F) →* Q,
40 Continuous φbar ∧ φbar.comp φY = ψQ
42/-- Transport the finite-quotient lift property across an abstract free-group equivalence. -/
43theorem denseAbstractSchreierFiniteQuotientLiftProperty_of_equiv
44 (C : ProCGroups.FiniteGroupClass.{u})
45 {F : Type u} [Group F] [TopologicalSpace F]
46 (H : OpenSubgroup F)
47 {L : Type u} [Group L]
48 {Y : Type u}
49 (eY : FreeGroup Y ≃* L)
50 (ψ : L →* ↥(H : Subgroup F))
51 (hψfinite :
52 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
53 [Finite Q] [DiscreteTopology Q],
54 C Q →
55 ∀ χL : L →* Q,
56 ∃! φbar : ↥(H : Subgroup F) →* Q,
57 Continuous φbar ∧ φbar.comp ψ = χL) :
58 DenseAbstractSchreierFiniteQuotientLiftProperty
59 (C := C) H (ψ.comp eY.toMonoidHom) := by
60 intro Q _ _ _ _ _ hQ ψQ
61 let χL : L →* Q := ψQ.comp eY.symm.toMonoidHom
62 have hχLFac : χL.comp eY.toMonoidHom = ψQ := by
63 apply MonoidHom.ext
64 intro w
65 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe,
66 Function.comp_apply,
67 MulEquiv.symm_apply_apply, χL]
68 rcases hψfinite hQ χL with ⟨φbar, hφbar, hφbarUnique⟩
69 refine ⟨φbar, ?_, ?_⟩
70 · refine ⟨hφbar.1, ?_⟩
71 apply MonoidHom.ext
72 intro w
73 calc
74 (φbar.comp (ψ.comp eY.toMonoidHom)) w = (φbar.comp ψ) (eY w) := rfl
75 _ = χL (eY w) := by
76 exact congrArg (fun f : L →* Q => f (eY w)) hφbar.2
77 _ = ψQ w := by
78 exact congrArg (fun f : FreeGroup Y →* Q => f w) hχLFac
79 · intro φbar' hφbar'
80 apply hφbarUnique
81 refine ⟨hφbar'.1, ?_⟩
82 apply MonoidHom.ext
83 intro l
84 rcases eY.surjective l with ⟨w, rfl⟩
85 have hw' :
86 (φbar'.comp (ψ.comp eY.toMonoidHom)) w = ψQ w :=
87 congrArg (fun f : FreeGroup Y →* Q => f w) hφbar'.2
88 calc
89 (φbar'.comp ψ) (eY w) = (φbar'.comp (ψ.comp eY.toMonoidHom)) w := rfl
90 _ = ψQ w := hw'
91 _ = χL (eY w) := by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp,
92 MonoidHom.coe_coe, Function.comp_apply,
93 MulEquiv.symm_apply_apply, χL]
95/--
96A dense abstract Schreier model with the finite-discrete quotient lift property is the pro-\(C\)
97completion of that abstract free group.
98-/
99theorem isProCCompletion_denseAbstractSchreier_of_finiteQuotientLifts
100 (C : ProCGroups.FiniteGroupClass.{u})
104 {X : Type u}
105 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
106 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
107 {ι : X → F}
108 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
109 (C := C) X F ι)
110 (H : OpenSubgroup F)
111 {Y : Type u}
112 [TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
113 {φY : FreeGroup Y →ₜ* ↥(H : Subgroup F)}
114 (hφYdense : DenseRange φY)
115 (hfinite :
116 DenseAbstractSchreierFiniteQuotientLiftProperty (C := C) H φY.toMonoidHom) :
118 (C)
119 (FreeGroup Y) ↥(H : Subgroup F) φY := by
120 have hHproC : ProCGroups.ProC.HasOpenNormalBasisInClass C ↥(H : Subgroup F) := by
121 exact
123 (C := C) hIso hSub hF.hasOpenNormalBasisInClass (H : Subgroup F)
124 (Subgroup.isClosed_of_isOpen (H : Subgroup F) H.isOpen')
126 (C := C) (hForm := hForm) (G := FreeGroup Y) (Ghat := ↥(H : Subgroup F))
127 hHproC (ι := φY) hφYdense ?_
128 intro Q _ _ _ _ _ hQ ψQ
129 rcases hfinite hQ ψQ.toMonoidHom with ⟨φbar, hφbar, hφbarUnique⟩
130 let φbarCont : ↥(H : Subgroup F) →ₜ* Q :=
131 { toMonoidHom := φbar
132 continuous_toFun := hφbar.1 }
133 refine ⟨φbarCont, ?_, ?_⟩
134 · apply ContinuousMonoidHom.toMonoidHom_injective
135 exact hφbar.2
136 · intro φbarCont' hφbarCont'
137 apply ContinuousMonoidHom.toMonoidHom_injective
138 exact hφbarUnique φbarCont'.toMonoidHom
139 ⟨φbarCont'.continuous_toFun, congrArg ContinuousMonoidHom.toMonoidHom hφbarCont'⟩
143/--
144A topologically generating subset of an open subgroup generates a dense subgroup after including
145it into the ambient group.
146-/
147theorem subgroup_le_topologicalClosure_of_topologicallyGenerates_local
148 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
149 (H : OpenSubgroup G)
150 {S : Set ↥(H : Subgroup G)}
151 (hS : Generation.TopologicallyGenerates (G := ↥(H : Subgroup G)) S) :
152 (H : Subgroup G) ≤
153 (Subgroup.closure (((↑) : ↥(H : Subgroup G) → G) '' S)).topologicalClosure := by
154 let D : Subgroup ↥(H : Subgroup G) := Subgroup.closure S
155 have hDense : Dense (D : Set ↥(H : Subgroup G)) :=
156 (Generation.topologicallyGenerates_iff_dense (G := ↥(H : Subgroup G)) (X := S)).1 hS
157 rw [Subtype.dense_iff] at hDense
158 have hmap :
159 D.map (H : Subgroup G).subtype =
160 Subgroup.closure (((↑) : ↥(H : Subgroup G) → G) '' S) := by
161 simpa [TopologicalGroup.image_subtype_eq_map] using ((H : Subgroup G).subtype.map_closure S)
162 have himage :
163 ((↑) : ↥(H : Subgroup G) → G) '' (D : Set ↥(H : Subgroup G)) =
164 ((D.map (H : Subgroup G).subtype : Subgroup G) : Set G) := by
165 exact TopologicalGroup.image_subtype_eq_map (H : Subgroup G).subtype D
166 intro g hg
167 have hg' :
168 g ∈ closure (((D.map (H : Subgroup G).subtype : Subgroup G) : Set G)) := by
169 have : g ∈ closure (((↑) : ↥(H : Subgroup G) → G) '' (D : Set ↥(H : Subgroup G))) :=
170 hDense hg
171 rwa [himage] at this
172 have hg'' :
173 g ∈ ((D.map (H : Subgroup G).subtype).topologicalClosure : Set G) := by
174 simpa [Subgroup.topologicalClosure_coe] using hg'
175 rw [← hmap]
176 exact hg''
178/-- If an open subgroup is topologically finitely generated, then so is the ambient compact group. -/
179theorem topologicallyFinitelyGenerated_of_openSubgroup_local
180 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
181 [CompactSpace G]
182 (H : OpenSubgroup G)
185 classical
186 rcases hH with ⟨sH, hsH⟩
187 letI : Finite (OpenSubgroupRightQuotient H) :=
188 finite_openSubgroupRightQuotient (F := G) H
189 letI : Fintype (OpenSubgroupRightQuotient H) :=
190 Fintype.ofFinite (OpenSubgroupRightQuotient H)
191 let τ := openSubgroupRightCosetSection (F := G) H
192 let sReps : Finset G := Finset.univ.image τ
193 let s : Finset G := sReps ∪ sH.image Subtype.val
194 let K : Subgroup G := Subgroup.closure (s : Set G)
195 have hHle' :
196 (H : Subgroup G) ≤
197 (Subgroup.closure
198 (((↑) : ↥(H : Subgroup G) → G) ''
199 ((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G)))).topologicalClosure :=
200 subgroup_le_topologicalClosure_of_topologicallyGenerates_local H (by simpa using hsH)
201 have hImageLe : Subgroup.closure
202 (((↑) : ↥(H : Subgroup G) → G) ''
203 ((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G))) ≤ K := by
204 refine Subgroup.closure_mono ?_
205 intro g hg
206 rcases hg with ⟨x, hx, rfl⟩
207 have hx' : (x : G) ∈ sH.image Subtype.val := by
208 exact Finset.mem_image.mpr ⟨x, by simpa using hx, rfl⟩
209 exact Finset.mem_coe.2 (Finset.mem_union_right sReps hx')
210 have hImageLe' :
211 (Subgroup.closure
212 (((↑) : ↥(H : Subgroup G) → G) ''
213 ((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G)))).topologicalClosure ≤
214 K.topologicalClosure :=
215 Subgroup.topologicalClosure_minimal _
216 (hImageLe.trans (Subgroup.le_topologicalClosure _))
217 (Subgroup.isClosed_topologicalClosure _)
218 have hHle : (H : Subgroup G) ≤ K.topologicalClosure := fun g hg => hImageLe' (hHle' hg)
219 have htop : K.topologicalClosure = ⊤ := by
220 apply top_unique
221 intro g _hg
222 let q : OpenSubgroupRightQuotient H := openSubgroupRightCoset H g
223 have hEq0 : openSubgroupRightCoset H (τ q) = q :=
224 openSubgroupRightCosetSection_spec (F := G) H q
225 have hEq :
226 openSubgroupRightCoset H g = openSubgroupRightCoset H (τ q) := by
227 simpa [q] using hEq0.symm
228 have hrel : QuotientGroup.rightRel (H : Subgroup G) g (τ q) :=
229 Quotient.exact' hEq
230 have hgH0 : τ q * g⁻¹ ∈ (H : Subgroup G) := by
231 simpa using (QuotientGroup.rightRel_apply.mp hrel)
232 have hgH : g * (τ q)⁻¹ ∈ (H : Subgroup G) := by
233 simpa [mul_inv_rev, mul_assoc] using ((H : Subgroup G).inv_mem hgH0)
234 have hgH' : g * (τ q)⁻¹ ∈ (K.topologicalClosure : Subgroup G) :=
235 hHle hgH
236 have hτK : τ q ∈ (K.topologicalClosure : Subgroup G) := by
237 have hτmem : τ q ∈ (sReps : Set G) := by
238 exact Finset.mem_coe.2 <| Finset.mem_image.mpr ⟨q, Finset.mem_univ q, rfl⟩
239 have hτmem' : τ q ∈ (s : Set G) := by
240 exact Finset.mem_coe.2 (Finset.mem_union_left _ hτmem)
241 exact Subgroup.le_topologicalClosure K (Subgroup.subset_closure hτmem')
242 have hmul :
243 (g * (τ q)⁻¹) * τ q ∈ (K.topologicalClosure : Subgroup G) :=
244 (K.topologicalClosure).mul_mem hgH' hτK
245 simpa [mul_assoc] using hmul
246 refine ⟨s, ?_⟩
247 simpa [Generation.TopologicallyGenerates, K, s] using htop
251/--
252A finite converging-set free pro-\(C\) basis realizes the pro-\(C\) completion of the abstract
253free group on the same basis.
254-/
255theorem isProCCompletion_freeGroupLift_of_finiteBasis
256 {C : ProCGroups.FiniteGroupClass.{u}}
259 {X : Type u} [Finite X]
260 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
261 [DiscreteTopology (FreeGroup X)]
262 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
263 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
264 {ι : X → F}
265 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
266 (C := C) X F ι) :
268 (C)
269 (FreeGroup X) F
270 { toMonoidHom := FreeGroup.lift ι
271 continuous_toFun := continuous_of_discreteTopology } := by
272 let φ : FreeGroup X →ₜ* F :=
273 { toMonoidHom := FreeGroup.lift ι
274 continuous_toFun := continuous_of_discreteTopology }
276 (C) (FreeGroup X) F φ
277 refine
278 { hasOpenNormalBasisInClass := hF.hasOpenNormalBasisInClass
279 denseRange := ?_
280 existsUnique_lift := ?_ }
281 · change DenseRange (FreeGroup.lift ι)
282 exact denseRange_freeGroupLift_of_topologicallyGenerates
283 (F := F) (X := X) hF.generates_range
284 · intro G _ _ _ _ _ _ hG ψ
285 let φX : X → G := fun x => ψ (FreeGroup.of x)
286 let S : Subgroup G := (Subgroup.closure (Set.range φX)).topologicalClosure
287 letI : CompactSpace S :=
288 (Subgroup.isClosed_topologicalClosure _).isClosedEmbedding_subtypeVal.compactSpace
290 exact
292 (C := C) hIso hSub hG S (Subgroup.isClosed_topologicalClosure _)
293 let φS : X → S := fun x =>
294 ⟨φX x, Subgroup.le_topologicalClosure _
295 (Subgroup.subset_closure ⟨x, rfl⟩)⟩
296 have hφSconv : FamilyConvergesToOneAlongOpenSubgroups (G := S) φS := by
297 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := S) φS
298 have hφSgen :
299 Generation.TopologicallyGenerates (G := S) (Set.range φS) := by
300 simpa [S, φS, φX] using
301 topologicallyGenerates_topologicalClosure_of_range φX
302 rcases hF.existsUnique_lift hSproC φS hφSconv hφSgen with
303 ⟨σS, hσS, _⟩
304 let σ : F →ₜ* G :=
305 { toMonoidHom := S.subtype.comp σS
306 continuous_toFun := by
307 simpa using continuous_subtype_val.comp hσS.1 }
308 have hσfac : σ.comp φ = ψ := by
309 apply ContinuousMonoidHom.toMonoidHom_injective
310 apply FreeGroup.ext_hom
311 intro x
312 change (S.subtype.comp σS) (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x)
313 simpa [φS, φX] using congrArg Subtype.val (hσS.2 x)
314 refine ⟨σ, hσfac, ?_⟩
315 intro g hg
316 apply ContinuousMonoidHom.toMonoidHom_injective
317 apply continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
318 (G := F) (A := G) hF.generates_range g.continuous_toFun σ.continuous_toFun
319 intro y hy
320 rcases hy with ⟨x, rfl⟩
321 have hσx := congrArg (fun k : FreeGroup X →ₜ* G => k (FreeGroup.of x)) hσfac
322 have hgx := congrArg (fun k : FreeGroup X →ₜ* G => k (FreeGroup.of x)) hg
323 have hσx' : σ (ι x) = ψ (FreeGroup.of x) := by
324 change σ (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x) at hσx
325 simpa using hσx
326 have hgx' : g (ι x) = ψ (FreeGroup.of x) := by
327 change g (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x) at hgx
328 simpa using hgx
329 exact hgx'.trans hσx'.symm
331/--
332If a finite generating family has the same cardinality as an abstract free model whose
333completion is the target, then that family realizes the same pro-C completion. The finite index
334type is arbitrary in the ambient universe.
335-/
336theorem isProCCompletion_freeGroupLift_of_exactGeneratingFamily_of_completion
337 {C : ProCGroups.FiniteGroupClass.{u}}
341 (hcyc :
342 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
343 C A ∧ IsCyclic A ∧ Nontrivial A)
344 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
345 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
346 {Y Z : Type u} [Finite Z]
347 [TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
348 [DiscreteTopology (FreeGroup Y)]
349 [TopologicalSpace (FreeGroup Z)] [IsTopologicalGroup (FreeGroup Z)]
350 [DiscreteTopology (FreeGroup Z)]
351 (hYZcard : Nat.card Y = Nat.card Z)
352 {φY : FreeGroup Y →ₜ* H}
353 (hCompY :
355 (C) (FreeGroup Y) H φY)
356 {κ : Z → H}
357 (hκ : Generation.GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (Set.range κ)) :
359 (C)
360 (FreeGroup Z) H
361 { toMonoidHom := FreeGroup.lift κ
362 continuous_toFun := continuous_of_discreteTopology } := by
363 have hYfin : Finite Y := by
364 by_cases h0 : Nat.card Z = 0
365 · haveI : IsEmpty Z :=
366 (Nat.card_eq_zero.1 h0).resolve_right <| Finite.not_infinite ‹_›
367 have hκrange : Set.range κ = (∅ : Set H) := by
368 ext z
369 constructor
370 · rintro ⟨x, rfl⟩
371 exact isEmptyElim x
372 · intro hz
373 simp only [Set.mem_empty_iff_false] at hz
374 have hHtriv : ∀ x : H, x = 1 := by
375 intro x
376 have hxmem :
377 x ∈ ((Subgroup.closure (Set.range κ)).topologicalClosure : Set H) := by
378 have hκgen : Generation.TopologicallyGenerates (G := H) (Set.range κ) := hκ.1
379 rw [Generation.TopologicallyGenerates] at hκgen
380 rw [hκgen]
381 simp only [Subgroup.coe_top, Set.mem_univ]
382 have hxmemEmpty :
383 x ∈ ((Subgroup.closure ((∅ : Set H))).topologicalClosure : Set H) := by
384 simpa [hκrange] using hxmem
385 simpa [Subgroup.coe_topologicalClosure_bot, closure_singleton] using hxmemEmpty
386 have hYempty : IsEmpty Y := by
387 refine ⟨fun y => ?_⟩
388 rcases
389 exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass
390 C hQuot hcyc with
391 ⟨A, _instGroupA, _instTopA, _instTopGroupA, _instCompactA, _instT2A,
392 _instTDA, hA, a, ha1, _hgena⟩
393 let ψY : FreeGroup Y →ₜ* A :=
394 { toMonoidHom := FreeGroup.lift (fun _ : Y => a)
395 continuous_toFun := continuous_of_discreteTopology }
396 have hψYne : ψY (FreeGroup.of y) ≠ 1 := by
397 change FreeGroup.lift (fun _ : Y => a) (FreeGroup.of y) ≠ 1
398 simpa using ha1
399 rcases hCompY.existsUnique_lift hA ψY with
400 ⟨σ, hσ, _⟩
401 have hyfac :=
402 congrArg (fun f : FreeGroup Y →ₜ* A => f (FreeGroup.of y)) hσ
403 have hyEq : ψY (FreeGroup.of y) = 1 := by
404 calc
405 ψY (FreeGroup.of y) = σ (φY (FreeGroup.of y)) := hyfac.symm
406 _ = σ 1 := by rw [hHtriv (φY (FreeGroup.of y))]
407 _ = 1 := map_one σ
408 exact hψYne hyEq
409 letI : IsEmpty Y := hYempty
410 infer_instance
411 · exact Nat.finite_of_card_ne_zero (α := Y) (by rw [hYZcard]; exact h0)
412 letI : Finite Y := hYfin
413 have hFreeY :
414 IsEpimorphicallyFreeProCGroupOnConvergingSet
415 (C := C)
416 Y H (fun y => φY (FreeGroup.of y)) := by
417 exact
418 proCCompletionOfAbstractFreeGroup_is_free
419 (C := C)
420 (X := Y) (Fhat := H) (ι := φY) hCompY
421 have hcardinal : Cardinal.mk Y = Cardinal.mk Z := by
422 exact Cardinal.mk_congr
423 ((Finite.equivFinOfCardEq hYZcard).trans
424 (Finite.equivFinOfCardEq (α := Z) rfl).symm)
425 have hFreeκ :
426 IsEpimorphicallyFreeProCGroupOnConvergingSet
427 (C := C) Z H κ := by
428 exact
429 finite_generatingFamily_is_basis_of_finiteGroupClass
430 (C := C) (X := Y) (Y := Z) hFreeY hcardinal hκ.1
431 exact
432 isProCCompletion_freeGroupLift_of_finiteBasis
433 (C := C) hSub hIso hFreeκ
436/--
437Compact pointed basis bridge: adjoining the point at infinity to a discrete converging basis,
438the open subgroup inherits a compact pointed right Schreier basis.
439-/
440theorem exists_compactPointedBasis_openSubgroup_of_freeProCOnConvergingSet
441 (C : ProCGroups.FiniteGroupClass.{u})
446 {X : Type u}
447 [TopologicalSpace X] [DiscreteTopology X]
448 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
449 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
450 {ι : X → F}
451 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
452 (C := C) X F ι)
453 (H : OpenSubgroup F) :
454 ∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
455 Continuous κ ∧
456 (∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
457 κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
458 IsCompact (Set.range κ) ∧
459 IsClosed (Set.range κ) ∧
460 IsEpimorphicallyPointedFreeProCGroupOn
461 (C := C)
462 (Set.range κ)
463 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
464 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
465 ↥(H : Subgroup F) Subtype.val := by
466 classical
467 let iInf : OnePoint X → F := fun z => z.elim 1 ι
468 have hιTendsto : Filter.Tendsto ι Filter.cofinite (𝓝 (1 : F)) := by
469 rw [Filter.tendsto_def]
470 intro s hs
471 rcases mem_nhds_iff.mp hs with ⟨W, hWs, hWopen, h1W⟩
473 (G := F) hWopen h1W with
474 ⟨U, hUW⟩
475 have hfinite : {x : X | ι x ∉ (U : Set F)}.Finite :=
476 hF.convergesToOneAlongOpenSubgroups U.toOpenSubgroup
477 have hcof : ∀ᶠ x : X in Filter.cofinite, ι x ∈ (U : Set F) :=
478 Filter.eventually_cofinite.2 hfinite
479 exact hcof.mono fun x hx => hWs (hUW hx)
480 have hPointed :
481 IsEpimorphicallyPointedFreeProCGroupOn
482 (C := C)
483 (OnePoint X) OnePoint.infty F iInf := by
484 refine ⟨hF.hasOpenNormalBasisInClass, ?_, by simp only [OnePoint.elim_infty, iInf], ?_, ?_⟩
485 · rw [OnePoint.continuous_iff_from_discrete]
486 simpa [iInf] using hιTendsto
487 · have hsub : Set.range ι ⊆ Set.range iInf := by
488 rintro y ⟨x, rfl⟩
489 exact ⟨(x : OnePoint X), rfl⟩
490 exact Generation.topologicallyGenerates_mono (G := F) hF.generates_range hsub
491 · intro G _ _ _ _ _ _ hG φ hφ hφ0 hgenφ
492 let ψ : X → G := fun x => φ x
493 have hψTendsto : Filter.Tendsto ψ Filter.cofinite (𝓝 (1 : G)) := by
494 have hraw := (OnePoint.continuous_iff_from_discrete (f := φ)).1 hφ
495 simpa [ψ, hφ0] using hraw
496 have hψconv : FamilyConvergesToOneAlongOpenSubgroups (G := G) ψ := by
497 intro U
498 exact Filter.eventually_cofinite.mp <|
499 hψTendsto (U.isOpen'.mem_nhds U.one_mem')
500 have hφrange : Set.range φ = Set.range ψ ∪ ({1} : Set G) := by
501 ext z
502 constructor
503 · rintro ⟨x, rfl⟩
504 refine OnePoint.rec ?_ ?_ x
505 · right
506 simpa [iInf] using hφ0
507 · intro y
508 left
509 exact ⟨y, rfl⟩
510 · intro hz
511 rcases hz with hz | hz
512 · rcases hz with ⟨y, rfl⟩
513 exact ⟨(y : OnePoint X), rfl⟩
514 · exact ⟨OnePoint.infty, hφ0.trans hz.symm⟩
515 have hψgen : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
516 have hgenφ' :
517 Generation.TopologicallyGenerates (G := G) (Set.range ψ ∪ ({1} : Set G)) := by
518 simpa [hφrange] using hgenφ
519 exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range ψ)).1
520 hgenφ'
521 rcases hF.existsUnique_lift hG ψ hψconv hψgen with ⟨f, hf, huniq⟩
522 refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
523 · intro x
524 refine OnePoint.rec ?_ ?_ x
525 · calc
526 f (iInf OnePoint.infty) = f 1 := rfl
527 _ = 1 := map_one f
528 _ = φ OnePoint.infty := hφ0.symm
529 · intro y
530 exact hf.2 y
531 · intro g hg
532 apply huniq g
533 refine ⟨hg.1, ?_⟩
534 intro y
535 simpa [iInf, ψ] using hg.2 (y : OnePoint X)
536 exact
537 exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup
538 (C := C) hForm hSub hIso hExt hPointed H
542end Profinite
543end ReidemeisterSchreier