ReidemeisterSchreier/Profinite/OpenSubgroups/ExactRightSchreierGeneration.lean
1import ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel
2import ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/ExactRightSchreierGeneration.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Profinite open-subgroup Schreier theory
15Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ReidemeisterSchreier
22namespace Profinite
24open ProCGroups
25open ProCGroups.FreeProC
26open ProCGroups.ProC
27open ProCGroups.WreathProducts
28open ReidemeisterSchreier.Discrete
29open ReidemeisterSchreier.Discrete.OpenSubgroups
31universe u v
33section ExactRightSchreierGeneration
35open FreeGroup
37variable {X : Type u} [TopologicalSpace X]
38variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
39variable {P : Type u} [Group P]
40variable {ι : X → F}
41variable {φ : FreeGroup X →* F}
43variable {K : Subgroup P}
46/-- The profinite minimal-power argument reduces its distinguished Schreier generator to the
49 [DecidableEq X]
50 (β : FreeGroup X →* P) (K : Subgroup P) (x : X) {N : ℕ}
51 (hN : 0 < N)
52 (hpow : β ((FreeGroup.of x) ^ N) ∈ K)
53 (hmin : ∀ m : ℕ, 0 < m → m < N → β ((FreeGroup.of x) ^ m) ∉ K) :
54 ∃ T : Set (FreeGroup X), ∃ hT :
55 IsRightSchreierTransversal (X := X) (Subgroup.comap β K) T,
56 (FreeGroup.of x) ^ (N - 1) ∈ T ∧
57 schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =
58 ⟨(FreeGroup.of x) ^ N, hpow⟩ := by
59 exact
61 (X := X) (L := Subgroup.comap β K) x hN hpow hmin
63omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] in
64/-- On elements of the abstract Schreier transversal, the transported cocycle in the ambient
65group matches the image of the discrete Schreier generator. -/
67 [DecidableEq X]
68 {T : Set (FreeGroup X)}
69 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
70 (hβsurj : Function.Surjective (π.comp φ))
71 {t : FreeGroup X} (ht : t ∈ T) (x : X) :
72 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
73 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
75 rightQuotientSectionCocycle (H := Hc) τ hτ (φ (FreeGroup.of x))
76 (Quotient.mk'' (φ t)) =
77 ⟨φ (schreierGenerator (X := X) hT t x), by
78 change (π.comp φ) ↑(schreierGenerator (X := X) hT t x) ∈ K
79 exact (schreierGenerator (X := X) hT t x).2⟩ := by
80 classical
81 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
82 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
84 letI : MulAction F (Quotient (QuotientGroup.rightRel Hc)) :=
85 rightCosetMulAction Hc
86 let rep := schreierRepresentative (X := X) hT (t * FreeGroup.of x)
87 have hτt :
88 τ (Quotient.mk'' (φ t)) = φ t := by
89 simpa [τ] using
90 (rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT ht)
91 have hrep_rel :
92 QuotientGroup.rightRel Hc (φ ((rep : T) : FreeGroup X)) (φ (t * FreeGroup.of x)) := by
93 rw [QuotientGroup.rightRel_apply]
94 dsimp [Hc]
96 have hrel :
97 t * FreeGroup.of x * (((rep : T) : FreeGroup X))⁻¹ ∈
98 Subgroup.comap (π.comp φ) K := by
99 simpa [schreierRepresentative, Subgroup.IsComplement.toRightFun] using
100 (hT.1.mul_inv_toRightFun_mem (t * FreeGroup.of x))
101 simpa [MonoidHom.comp_apply, MonoidHom.map_mul, MonoidHom.map_inv] using hrel
102 have hqnext :
103 (φ (FreeGroup.of x))⁻¹ • (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) =
104 Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := by
105 calc
106 (φ (FreeGroup.of x))⁻¹ • (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))
107 = Quotient.mk'' (φ t * φ (FreeGroup.of x)) := by
108 rw [rightCosetMulAction_inv_mk_smul (H := Hc) (φ (FreeGroup.of x)) (φ t)]
109 _ = Quotient.mk'' (φ (t * FreeGroup.of x)) := by
110 simp only [MonoidHom.map_mul]
111 _ = Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := (Quotient.sound' hrep_rel).symm
112 have hτnext :
113 τ (Quotient.mk'' (φ t * φ (FreeGroup.of x))) =
114 φ ((rep : T) : FreeGroup X) := by
115 have hqnext' :
116 (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
117 Quotient (QuotientGroup.rightRel Hc)) =
118 Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := by
119 calc
120 (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
121 Quotient (QuotientGroup.rightRel Hc))
122 = Quotient.mk'' (φ (t * FreeGroup.of x)) := by
123 simp only [MonoidHom.map_mul]
124 _ = Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := (Quotient.sound' hrep_rel).symm
125 rw [hqnext']
126 exact
127 rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT rep.2
128 have hτrep :
129 τ ((φ (FreeGroup.of x))⁻¹ •
130 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))) =
131 φ ((rep : T) : FreeGroup X) := by
132 have hrep_sec :
133 τ (Quotient.mk'' (φ ((rep : T) : FreeGroup X))) =
134 φ ((rep : T) : FreeGroup X) :=
135 rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT rep.2
136 exact hqnext ▸ hrep_sec
137 apply Subtype.ext
138 change
139 τ (Quotient.mk'' (φ t)) * φ (FreeGroup.of x) *
140 (τ ((φ (FreeGroup.of x))⁻¹ •
141 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))))⁻¹ =
142 φ ↑(schreierGenerator hT t x)
143 dsimp [rightQuotientSectionCocycle]
144 have hqnext'' :
145 (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
146 Quotient (QuotientGroup.rightRel Hc)) =
147 (φ (FreeGroup.of x))⁻¹ •
148 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) := by
150 have hqnext''' :
151 (Quotient.mk'' (φ t * (φ (FreeGroup.of x))⁻¹⁻¹) :
152 Quotient (QuotientGroup.rightRel Hc)) =
153 (φ (FreeGroup.of x))⁻¹ •
154 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) := by
156 rw [hτt, hqnext''', hτrep]
157 simp only [mul_assoc, schreierGenerator, MonoidHom.map_mul, MonoidHom.map_inv, rep]
159omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] in
160/-- On elements of the abstract Schreier transversal, the transported right Schreier cocycle in
161the ambient group is the image of the discrete Schreier generator. -/
163 [DecidableEq X]
164 {T : Set (FreeGroup X)}
165 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
166 (hβsurj : Function.Surjective (π.comp φ))
167 {t : FreeGroup X} (ht : t ∈ T) (x : X) :
168 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
169 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
171 rightQuotientSectionCocycle (H := Hc) τ hτ (φ (FreeGroup.of x))
172 (Quotient.mk'' (φ t)) =
173 ⟨φ (schreierGenerator (X := X) hT t x), by
174 change (π.comp φ) ↑(schreierGenerator (X := X) hT t x) ∈ K
175 exact (schreierGenerator (X := X) hT t x).2⟩ := by
176 simpa using map_schreierGenerator_eq_cocycle
179omit [TopologicalSpace X] in
180/-- The transported right Schreier cocycle topologically generates the ambient subgroup as soon as
181the dense abstract free subgroup remains dense after restricting to that subgroup. -/
183 [DecidableEq X]
184 {T : Set (FreeGroup X)}
185 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
186 (hβsurj : Function.Surjective (π.comp φ))
187 (hφdense :
188 DenseRange
189 ({ toFun := fun g : Subgroup.comap (π.comp φ) K => ⟨φ g.1, g.2⟩
191 map_mul' := by
192 intro a b
193 ext
196 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
197 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
198 let κ :
201 fun p =>
202 rightQuotientSectionCocycle (H := Subgroup.comap π K) τ hτ (φ (FreeGroup.of p.2)) p.1
203 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Subgroup.comap π K)) (Set.range κ) := by
204 classical
206 { toFun := fun g => ⟨φ g.1, g.2⟩
208 map_mul' := by
209 intro a b
210 ext
212 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
213 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
214 let κ :
217 fun p =>
218 rightQuotientSectionCocycle (H := Subgroup.comap π K) τ hτ (φ (FreeGroup.of p.2)) p.1
219 have hsubset :
220 φL '' (schreierGeneratorSet (X := X) hT : Set (Subgroup.comap (π.comp φ) K)) ⊆
221 Set.range κ := by
222 intro z hz
223 rcases hz with ⟨s, hs, rfl⟩
224 rcases hs with ⟨t, ht, x, rfl, _⟩
225 refine ⟨(Quotient.mk'' (φ t), x), ?_⟩
226 simpa [κ, φL] using
227 (map_schreierGenerator_eq_cocycle (X := X) (φ := φ) (π := π) (K := K)
228 hT hβsurj ht x)
229 have hmap :
230 Subgroup.closure
231 (φL '' (schreierGeneratorSet (X := X) hT :
232 Set (Subgroup.comap (π.comp φ) K))) =
233 φL.range := by
234 calc
235 Subgroup.closure
236 (φL '' (schreierGeneratorSet (X := X) hT :
237 Set (Subgroup.comap (π.comp φ) K)))
238 = (Subgroup.closure
239 (schreierGeneratorSet (X := X) hT :
240 Set (Subgroup.comap (π.comp φ) K))).map φL := by
241 symm
242 exact MonoidHom.map_closure φL _
243 _ = (⊤ : Subgroup (Subgroup.comap (π.comp φ) K)).map φL := by
244 rw [closure_schreierGeneratorSet_eq_top (X := X) hT]
245 _ = φL.range := by
246 rw [← MonoidHom.range_eq_map]
247 have hgenImg :
248 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Subgroup.comap π K))
249 (φL '' (schreierGeneratorSet (X := X) hT :
250 Set (Subgroup.comap (π.comp φ) K))) := by
252 rw [hmap]
253 simpa [DenseRange, MonoidHom.coe_range] using hφdense
254 exact ProCGroups.Generation.topologicallyGenerates_mono (G := ↥(Subgroup.comap π K))
255 hgenImg hsubset
257end ExactRightSchreierGeneration
259section WreathTargetClosures
261variable {Y : Type u} [TopologicalSpace Y]
262variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
264omit [TopologicalSpace Y] in
265/-- The topological closure of the subgroup generated by the range of a map is itself
266topologically generated by that range, viewed inside the closed subgroup. -/
268 (ξ : Y → G) :
269 let W : Subgroup G := (Subgroup.closure (Set.range ξ)).topologicalClosure
270 let ξW : Y → W := fun y =>
271 ⟨ξ y, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨y, rfl⟩)⟩
272 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range ξW) := by
273 classical
274 let A : Subgroup G := Subgroup.closure (Set.range ξ)
275 let W : Subgroup G := A.topologicalClosure
276 let ξW : Y → W := fun y =>
277 ⟨ξ y, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨y, rfl⟩)⟩
279 let B : Subgroup W := Subgroup.closure (Set.range ξW)
280 let i : W →* G := W.subtype
281 have hrange : i '' Set.range ξW = Set.range ξ := by
282 ext g
283 constructor
284 · rintro ⟨y, ⟨x, rfl⟩, rfl⟩
285 exact ⟨x, rfl⟩
286 · rintro ⟨y, rfl⟩
287 exact ⟨ξW y, ⟨y, rfl⟩, rfl⟩
288 have hmap : B.map i = A := by
289 calc
290 B.map i = Subgroup.closure (i '' Set.range ξW) := by
291 simpa [B] using (MonoidHom.map_closure i (Set.range ξW))
292 _ = A := by
293 simp only [hrange, A]
294 have himage : ((↑) : W → G) '' (B : Set W) = (A : Set G) := by
295 simpa using congrArg SetLike.coe hmap
296 have hsubset :
297 (W : Set G) ⊆ closure (((↑) : W → G) '' (B : Set W)) := by
298 rw [himage]
299 simp only [Subgroup.topologicalClosure_coe, subset_refl, W, A]
300 exact (Subtype.dense_iff).2 hsubset
302end WreathTargetClosures
304section UniquenessOnGeneratingRanges
306variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
307variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [T2Space A]
309omit [IsTopologicalGroup A] in
310/-- Continuous homomorphisms into a Hausdorff topological group are determined by their values on
311any topologically generating set. -/
313 {X : Set G}
314 (hX : ProCGroups.Generation.TopologicallyGenerates (G := G) X)
315 {f g : G →* A} (hf : Continuous f) (hg : Continuous g)
316 (hfg : Set.EqOn f g X) :
317 f = g := by
318 let E : Subgroup G :=
319 { carrier := {x | f x = g x}
321 mul_mem' := by
322 intro a b ha hb
323 calc
325 _ = g a * g b := by rw [ha, hb]
327 inv_mem' := by
328 intro a ha
329 simpa [ha] }
330 have hsub : X ⊆ (E : Set G) := by
331 intro x hx
332 exact hfg hx
333 have hclosure : Subgroup.closure X ≤ E :=
334 (Subgroup.closure_le (K := E)).2 hsub
335 let S : Subgroup G := Subgroup.closure X
336 have hDense : DenseRange (S.subtype : S → G) := by
337 have hDenseSet : Dense ((S : Subgroup G) : Set G) := by
338 simpa [S] using
339 (ProCGroups.Generation.topologicallyGenerates_iff_dense (G := G) (X := X)).1 hX
340 simpa [DenseRange] using hDenseSet
341 have hEq :
342 (fun s : S => f s.1) = fun s : S => g s.1 := by
343 funext s
344 exact hclosure s.2
345 have hfun :
346 (fun x : G => f x) = fun x : G => g x := by
347 apply DenseRange.equalizer (f := (S.subtype : S → G)) hDense
348 · exact hf
349 · exact hg
350 · simpa using hEq
351 ext x
352 exact congrArg (fun h : G → A => h x) hfun
354end UniquenessOnGeneratingRanges
356section TransportedSectionPurity
358variable {P : Type u} [Group P]
359variable {X : Type u} [DecidableEq X]
360variable {F : Type u} [Group F]
361variable {A : Type v} [Group A]
363variable {T : Set (FreeGroup X)}
365instance instMulActionRightCosetComap :
369/-- On a transported Schreier transversal, basepoint coordinates are trivial once every tree-edge
372 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
373 (ψ : F →* PermutationalWreathProduct A
375 (hψ :
376 (SemidirectProduct.rightHom :
379 MonoidHom.id F)
380 (hone :
381 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
382 schreierGenerator (X := X) hT t x = 1 →
384 (Quotient.mk'' (φ t) :
386 (φ (FreeGroup.of x)) = 1)
387 (t : FreeGroup X) (ht : t ∈ T) :
389 (Quotient.mk'' (1 : F) :
391 (φ t) = 1 := by
392 by_cases h1 : t = 1
393 · subst h1
394 simp only [wreathLeftCoordinate, map_one, SemidirectProduct.one_left, Pi.one_apply]
395 · rcases FreeGroup.lastLetter_cases_of_ne_one (X := X) h1 with ⟨x, hpos | hneg⟩
396 · rcases hpos with ⟨hw, hlast, hmul⟩
397 have hp : FreeGroup.prefixParent t ∈ T :=
398 prefixParent_mem_of_mem (X := X) hT ht
399 have hpure :
401 (Quotient.mk'' (1 : F) :
403 (φ (FreeGroup.prefixParent t)) = 1 :=
404 wreathLeftCoordinate_basepoint_of_transversalWord hT ψ hψ hone
405 (FreeGroup.prefixParent t) hp
406 have hcoord :
408 (Quotient.mk'' (φ (FreeGroup.prefixParent t)) :
410 (φ (FreeGroup.of x)) = 1 := by
411 exact hone hp x
412 (schreierGenerator_eq_one_of_prefixParent_last_pos (X := X) hT ht hw hlast)
413 have hq :
414 (φ (FreeGroup.prefixParent t))⁻¹ •
415 (Quotient.mk'' (1 : F) :
417 Quotient.mk'' (φ (FreeGroup.prefixParent t)) := by
418 rw [rightCosetMulAction_inv_mk_smul
420 simp only [one_mul]
421 have hmulφ :
422 φ (FreeGroup.prefixParent t) * φ (FreeGroup.of x) = φ t := by
423 simpa [MonoidHom.map_mul] using congrArg φ hmul
424 calc
426 (Quotient.mk'' (1 : F) :
428 (φ t)
429 =
431 (Quotient.mk'' (1 : F) :
433 (φ (FreeGroup.prefixParent t) * φ (FreeGroup.of x)) := by
434 rw [hmulφ]
435 _ =
437 (Quotient.mk'' (1 : F) :
439 (φ (FreeGroup.prefixParent t)) *
441 ((φ (FreeGroup.prefixParent t))⁻¹ •
442 (Quotient.mk'' (1 : F) :
444 (φ (FreeGroup.of x)) := by
445 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ]
446 _ = 1 * 1 := by rw [hpure, hq, hcoord]
447 _ = 1 := by simp only [mul_one]
448 · rcases hneg with ⟨hw, hlast, hmul⟩
449 have hp : FreeGroup.prefixParent t ∈ T :=
450 prefixParent_mem_of_mem (X := X) hT ht
451 have hpure :
453 (Quotient.mk'' (1 : F) :
455 (φ (FreeGroup.prefixParent t)) = 1 :=
456 wreathLeftCoordinate_basepoint_of_transversalWord hT ψ hψ hone
457 (FreeGroup.prefixParent t) hp
458 have hcoord :
460 (Quotient.mk'' (φ t) :
462 (φ (FreeGroup.of x)) = 1 := by
463 exact hone ht x
464 (schreierGenerator_eq_one_of_cancels (X := X) hT ht hw hlast)
465 have hq :
466 (φ t)⁻¹ •
467 (Quotient.mk'' (1 : F) :
469 Quotient.mk'' (φ t) := by
471 simp only [one_mul]
472 have hmulφ :
473 φ t * φ (FreeGroup.of x) = φ (FreeGroup.prefixParent t) := by
474 simpa [MonoidHom.map_mul] using congrArg φ hmul
475 have hstep :
477 (Quotient.mk'' (1 : F) :
479 (φ (FreeGroup.prefixParent t)) =
481 (Quotient.mk'' (1 : F) :
483 (φ t) := by
484 calc
486 (Quotient.mk'' (1 : F) :
488 (φ (FreeGroup.prefixParent t))
489 =
491 (Quotient.mk'' (1 : F) :
493 (φ t * φ (FreeGroup.of x)) := by
494 rw [hmulφ]
495 _ =
497 (Quotient.mk'' (1 : F) :
499 (φ t) *
501 ((φ t)⁻¹ •
502 (Quotient.mk'' (1 : F) :
504 (φ (FreeGroup.of x)) := by
505 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ]
506 _ = wreathLeftCoordinate ψ
507 (Quotient.mk'' (1 : F) :
509 (φ t) * 1 := by
510 rw [hq, hcoord]
511 _ = wreathLeftCoordinate ψ
512 (Quotient.mk'' (1 : F) :
514 (φ t) := by simp only [mul_one]
515 exact hstep.symm.trans hpure
516termination_by (FreeGroup.toWord t).length
517decreasing_by
518 all_goals
519 simpa [Internal.FreeGroupWord.FreeGroup.toWord_prefixParent] using
520 Internal.FreeGroupWord.FreeGroup.toWord_length_prefixParent_lt (t := t) h1
522/-- The transported Schreier section has trivial basepoint coordinate whenever the tree-edge
523generators do. -/
525 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
526 (hβsurj : Function.Surjective (π.comp φ))
527 (ψ : F →* PermutationalWreathProduct A
529 (hψ :
530 (SemidirectProduct.rightHom :
533 MonoidHom.id F)
534 (hone :
535 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
536 schreierGenerator (X := X) hT t x = 1 →
538 (Quotient.mk'' (φ t) :
540 (φ (FreeGroup.of x)) = 1)
543 (Quotient.mk'' (1 : F) :
545 (rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT q) = 1 := by
546 let e := rightQuotientEquivOfComap π φ (π.comp φ) K rfl hβsurj
547 let tT : T := hT.1.rightQuotientEquiv (e.symm q)
548 have htT : ((tT : T) : FreeGroup X) ∈ T := tT.2
549 have hsec :
550 rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT q =
551 φ ((tT : T) : FreeGroup X) := by
552 simp only [rightSchreierSectionOfComap, rightTransversalSection, tT, e]
553 rw [hsec]
554 exact wreathLeftCoordinate_basepoint_of_transversalWord hT ψ hψ hone
555 ((tT : T) : FreeGroup X) htT
557end TransportedSectionPurity
559section FiniteQuotientLift
561open FreeGroup
563/-- Concrete finite-quotient lift for the dense abstract Schreier subgroup
564`comap (FreeGroup.lift ι) H → H`. -/
566 (C : ProCGroups.FiniteGroupClass.{u})
567 (hForm : ProCGroups.FiniteGroupClass.Formation C)
568 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
569 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
570 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
571 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
572 {X : Type u} [Finite X]
573 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
574 {ι : X → F}
576 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
577 (H : OpenSubgroup F)
578 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
579 [Finite Q] [DiscreteTopology Q]
580 (hQ : C Q)
581 (ψ : Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) →* Q) :
582 ∃ ψBar : ↥(H : Subgroup F) →* Q,
583 Continuous ψBar ∧
584 ψBar.comp
585 ({ toFun := fun g : Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) =>
586 ⟨(FreeGroup.lift ι) g.1, g.2⟩
588 map_mul' := by
589 intro a b
590 ext
592 Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) →* ↥(H : Subgroup F)) = ψ := by
593 classical
594 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
595 letI : T2Space F := IsProCGroup.t2Space hF.isProC
596 letI : TotallyDisconnectedSpace F :=
597 IsProCGroup.totallyDisconnectedSpace hF.isProC
598 let n : ℕ := Nat.card (F ⧸ (H : Subgroup F))
599 let P := openSubgroupIndexActionRange (G := F) H
600 (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl)
601 let ρ : F →ₜ* P :=
602 openSubgroupIndexActionRangeContinuousHom (G := F) H
603 (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl)
604 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
605 let K : Subgroup P := MulAction.stabilizer P q0
606 let βF : FreeGroup X →* F := FreeGroup.lift ι
607 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
608 let Lk : Subgroup (FreeGroup X) := Subgroup.comap β K
609 let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
610 letI : TopologicalSpace (FreeGroup X) := ⊥
611 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
612 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
613 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
614 ext g
615 constructor
616 · intro hg
617 change ρ g • q0 = q0 at hg
619 (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl) g] at hg
620 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
621 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
622 simpa [QuotientGroup.eq] using hg
623 · intro hg
624 change ρ g • q0 = q0
626 (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl) hg
627 have hLk : Lk = L := by
628 ext w
629 change β w ∈ K ↔ βF w ∈ (H : Subgroup F)
630 change βF w ∈ Subgroup.comap ρ.toMonoidHom K ↔ βF w ∈ (H : Subgroup F)
631 rw [hcomap]
632 let Hc : OpenSubgroup F :=
633 { toSubgroup := Subgroup.comap ρ.toMonoidHom K
634 isOpen' := by
635 rw [hcomap]
636 exact H.isOpen' }
637 have hHc : Hc = H := by
638 ext g
639 simpa [Hc] using congrArg (fun S : Subgroup F => g ∈ S) hcomap
640 let toK : L →* Lk :=
641 { toFun := fun g => ⟨g.1, by
642 have hgL : βF g.1 ∈ (H : Subgroup F) := g.2
643 have hgComap : βF g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
644 exact (congrArg (fun S : Subgroup F => βF g.1 ∈ S) hcomap).mpr hgL
645 change ρ (βF g.1) ∈ K
646 exact hgComap⟩
647 map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
648 map_mul' := by
649 intro a b
650 ext
651 simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
652 let fromK : Lk →* L :=
653 { toFun := fun g => ⟨g.1, by
654 have hgLk : β g.1 ∈ K := g.2
655 have hgComap : βF g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
656 change ρ (βF g.1) ∈ K
657 simpa [β] using hgLk
658 have hgH : βF g.1 ∈ (H : Subgroup F) := by
659 exact (congrArg (fun S : Subgroup F => βF g.1 ∈ S) hcomap).mp hgComap
660 change βF g.1 ∈ (H : Subgroup F)
661 exact hgH⟩
662 map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
663 map_mul' := by
664 intro a b
665 ext
666 simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
667 let φOrig : L →* ↥(H : Subgroup F) :=
668 { toFun := fun g => ⟨βF g.1, g.2⟩
670 map_mul' := by
671 intro a b
672 ext
674 let φK : Lk →* ↥(Hc : Subgroup F) :=
675 { toFun := fun g => ⟨βF g.1, by
676 have hgLk : β g.1 ∈ K := g.2
677 change ρ (βF g.1) ∈ K
678 simpa [β] using hgLk⟩
680 map_mul' := by
681 intro a b
682 ext
684 let toHc : ↥(H : Subgroup F) →* ↥(Hc : Subgroup F) :=
685 { toFun := fun g => ⟨g.1, by
686 have hgH : g.1 ∈ (H : Subgroup F) := g.2
687 have hgComap : g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
688 exact (congrArg (fun S : Subgroup F => g.1 ∈ S) hcomap).mpr hgH
689 change ρ g.1 ∈ K
690 exact hgComap⟩
691 map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
692 map_mul' := by
693 intro a b
694 ext
695 simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
696 let ψK : Lk →* Q := ψ.comp fromK
697 letI : Finite (OpenSubgroupRightQuotient Hc) :=
698 finite_openSubgroupRightQuotient (F := F) Hc
699 letI : Fintype (OpenSubgroupRightQuotient Hc) :=
700 fintype_openSubgroupRightQuotient (F := F) Hc
701 letI : DiscreteTopology (OpenSubgroupRightQuotient Hc) :=
702 discreteTopology_openSubgroupRightQuotient (F := F) Hc
703 letI : MulAction F (OpenSubgroupRightQuotient Hc) :=
704 rightCosetMulAction (Hc : Subgroup F)
705 letI : ContinuousSMul F (OpenSubgroupRightQuotient Hc) := by
706 refine ContinuousSMul.mk ?_
707 refine (continuous_prod_of_discrete_right).2 ?_
708 intro q
709 convert
711 (G := F) (H := (Hc : Subgroup F)) Hc.isOpen' q).comp continuous_inv using 1
712 ext g
714 have hβFdense : DenseRange βF :=
716 (F := F) (X := X) hF.generates_range
717 have hρSurj : Function.Surjective ρ := by
718 intro p
719 rcases p.down.2 with ⟨g, hg⟩
720 refine ⟨g, ?_⟩
721 apply ULift.ext
722 apply Subtype.ext
723 exact hg
724 have hβDense : DenseRange β := by
725 simpa [β, MonoidHom.comp_apply] using
726 (Function.Surjective.denseRange hρSurj).comp hβFdense ρ.continuous_toFun
727 have hβSurj : Function.Surjective β :=
728 surjective_of_denseRange (F := FreeGroup X) (P := P) hβDense
729 obtain ⟨T, hTK⟩ := exists_rightSchreierTransversal (X := X) Lk
730 let eQuot :
731 Quotient (QuotientGroup.rightRel Lk) ≃ OpenSubgroupRightQuotient Hc := by
732 simpa [Hc, OpenSubgroupRightQuotient] using
733 (rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβSurj)
734 let tRep : OpenSubgroupRightQuotient Hc → T := fun q =>
735 hTK.1.rightQuotientEquiv (eQuot.symm q)
736 have htRep_eq_of_mem {t : FreeGroup X} (ht : t ∈ T) :
737 tRep (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) = ⟨t, ht⟩ := by
738 have hmk :
739 (rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβSurj)
740 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) =
741 (Quotient.mk'' (βF t) :
742 Quotient (QuotientGroup.rightRel (Subgroup.comap ρ.toMonoidHom K))) := by
743 exact rightQuotientEquivOfComap_mk ρ.toMonoidHom βF β K rfl hβSurj t
744 have hEq :
745 eQuot.symm (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) =
746 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) := by
747 exact eQuot.symm_apply_eq.mpr (by simpa [eQuot, Hc, OpenSubgroupRightQuotient] using hmk)
748 apply hTK.1.rightQuotientEquiv.symm.injective
749 simpa [tRep] using hEq
750 let ν :
751 X → PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F := fun x =>
752 ⟨fun q => ψK (schreierGenerator (X := X) hTK ((tRep q : T) : FreeGroup X) x), ι x⟩
753 have hQproC : IsProCGroup C Q := by
754 exact IsProCGroup.of_finite_discrete (C := C) (G := Q) hQuot hQ
755 have hWreath :
756 IsProCGroup C
757 (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F) := by
758 exact
760 (C := C) hForm hIso hExt hQproC hF.isProC
761 let W : Subgroup (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F) :=
762 (Subgroup.closure (Set.range ν)).topologicalClosure
763 have hWproC : IsProCGroup C W := by
764 exact
765 IsProCGroup.of_isClosed_subgroup
766 (C := C) (G := PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F)
767 hIso hSub hQuot hWreath W (Subgroup.isClosed_topologicalClosure _)
768 let νW : X → W := fun x =>
769 ⟨ν x, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩)⟩
770 have hνWconv : FamilyConvergesToOne (G := W) νW := by
771 exact FamilyConvergesToOne.of_finite_domain (G := W) νW
772 have hνWgen :
773 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range νW) := by
774 simpa [W, νW] using topologicallyGenerates_topologicalClosure_of_range ν
775 rcases hF.existsUnique_lift hWproC νW hνWconv hνWgen with
776 ⟨ηW, hηW, _⟩
777 let η : F →* PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F :=
778 W.subtype.comp ηW
779 have hηCont : Continuous η := by
780 simpa [η] using (continuous_subtype_val.comp hηW.1)
781 have hηOnGen : ∀ x : X, η (ι x) = ν x := by
782 intro x
783 simpa [η, νW] using congrArg Subtype.val (hηW.2 x)
784 have hηRight :
785 (SemidirectProduct.rightHom :
786 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η =
787 MonoidHom.id F := by
788 rcases hF.existsUnique_lift hF.isProC ι hF.convergesToOne hF.generates_range with
789 ⟨u, hu, huuniq⟩
790 have hu_id : MonoidHom.id F = u := by
791 exact
792 huuniq (MonoidHom.id F)
793 ⟨by simpa using (continuous_id : Continuous fun x : F => x), by intro x; rfl⟩
794 have hu_η :
795 (SemidirectProduct.rightHom :
796 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η = u := by
797 let v : F →* F :=
798 (SemidirectProduct.rightHom :
799 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η
800 have hv_on_gen : ∀ x : X, v (ι x) = ι x := by
801 intro x
802 have hx := congrArg
803 (fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F => z.right)
804 (hηOnGen x)
805 simpa [v, ν, MonoidHom.comp_apply] using hx
806 exact huuniq v ⟨continuous_permutationalWreathProduct_right.comp hηCont, hv_on_gen⟩
807 calc
808 (SemidirectProduct.rightHom :
809 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η = u := hu_η
810 _ = MonoidHom.id F := hu_id.symm
811 have hηCoord :
812 ∀ q : OpenSubgroupRightQuotient Hc, ∀ x : X,
813 wreathLeftCoordinate η q (βF (FreeGroup.of x)) =
814 ψK (schreierGenerator (X := X) hTK ((tRep q : T) : FreeGroup X) x) := by
815 intro q x
816 simpa [wreathLeftCoordinate, βF, ν] using
817 congrArg
818 (fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F => z.left q)
819 (hηOnGen x)
820 have hηOne :
821 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
822 schreierGenerator (X := X) hTK t x = 1 →
824 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
825 (βF (FreeGroup.of x)) = 1 := by
826 intro t ht x hsg
827 rw [hηCoord]
828 rw [htRep_eq_of_mem (t := t) ht]
830 have htPure :
831 ∀ q : OpenSubgroupRightQuotient Hc,
833 (Quotient.mk'' (1 : F) : OpenSubgroupRightQuotient Hc)
834 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK q) = 1 := by
835 intro q
836 simpa [Hc, OpenSubgroupRightQuotient] using
839 hTK hβSurj η hηRight hηOne q)
840 let ψBarK : ↥(Hc : Subgroup F) →* Q :=
841 rightQuotientBasepointProjectionHom (H := (Hc : Subgroup F)) η hηRight
842 have hψBarKCont : Continuous ψBarK := by
843 simpa [ψBarK, rightQuotientBasepointProjectionHom, wreathLeftCoordinate] using
845 (S := OpenSubgroupRightQuotient Hc) (G := F)
846 (Quotient.mk'' (1 : F) : OpenSubgroupRightQuotient Hc)).comp
847 (hηCont.comp continuous_subtype_val)
848 have hψBarKOnSchreier :
849 ∀ s : ↥(schreierGeneratorSet (X := X) hTK),
850 ψBarK (φK s) = ψK s := by
851 rintro ⟨s, hs⟩
852 rcases hs with ⟨t, ht, x, rfl, _hne⟩
853 have hmap :
854 φK (schreierGenerator (X := X) hTK t x) =
856 (H := (Hc : Subgroup F))
857 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
858 (rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβSurj hTK)
859 (βF (FreeGroup.of x))
860 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) := by
861 simpa [φK, Hc, β, βF] using
864 calc
865 ψBarK (φK (schreierGenerator (X := X) hTK t x)) =
866 ψBarK
868 (H := (Hc : Subgroup F))
869 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
871 ρ.toMonoidHom βF β K rfl hβSurj hTK)
872 (βF (FreeGroup.of x))
873 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)) := by
874 rw [hmap]
875 _ =
877 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
878 (βF (FreeGroup.of x)) := by
879 simpa [ψBarK, Hc, OpenSubgroupRightQuotient] using
881 (H := (Hc : Subgroup F))
882 (τ := rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
884 ρ.toMonoidHom βF β K rfl hβSurj hTK)
885 (ψ := η) hηRight htPure
886 (βF (FreeGroup.of x))
887 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc))
888 _ = ψK (schreierGenerator (X := X) hTK t x) := by
889 rw [hηCoord]
890 rw [htRep_eq_of_mem (t := t) ht]
891 have hψBarKFac : ψBarK.comp φK = ψK := by
892 letI : T2Space Q := inferInstance
893 have hSchGen :
895 (G := Lk) (schreierGeneratorSet (X := X) hTK : Set Lk) := by
897 rw [closure_schreierGeneratorSet_eq_top (X := X) hTK]
898 exact dense_univ
900 (G := Lk) (A := Q) hSchGen
901 (continuous_of_discreteTopology : Continuous (ψBarK.comp φK))
902 (continuous_of_discreteTopology : Continuous ψK)
903 intro h hh
904 exact hψBarKOnSchreier ⟨h, hh⟩
905 let ψBar : ↥(H : Subgroup F) →* Q := ψBarK.comp toHc
906 have htoHcCont : Continuous toHc :=
907 Continuous.subtype_mk continuous_subtype_val (by
908 intro x
909 exact (congrArg (fun S : Subgroup F => x.1 ∈ S) hcomap).mpr x.2)
910 have hψBarCont : Continuous ψBar := hψBarKCont.comp htoHcCont
911 refine ⟨ψBar, hψBarCont, ?_⟩
912 apply MonoidHom.ext
913 intro l
914 have hto :
915 toHc (φOrig l) = φK (toK l) := by
916 ext
917 rfl
918 have hfrom :
919 fromK (toK l) = l := by
920 ext
921 rfl
922 have hfacK := congrArg (fun f : Lk →* Q => f (toK l)) hψBarKFac
923 calc
924 ψBar (φOrig l) = ψBarK (φK (toK l)) := by
925 simpa [ψBar, MonoidHom.comp_apply] using congrArg ψBarK hto
926 _ = ψK (toK l) := hfacK
927 _ = ψ (fromK (toK l)) := rfl
928 _ = ψ l := by rw [hfrom]
930end FiniteQuotientLift
932section ExactPointedRightSchreierGeneration
934open ProCGroups.ProC
936/-- An open subgroup of a pointed free pro-`C` group admits a compact right
938pointed free pro-`C` basis of the open subgroup. -/
940 {C : ProCGroups.FiniteGroupClass.{u}}
941 (hForm : ProCGroups.FiniteGroupClass.Formation C)
942 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
943 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
944 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
945 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
946 {X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
947 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
948 {ι : X → F}
949 (hF : IsPointedFreeProCGroupOn
950 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X x0 F ι)
951 (H : OpenSubgroup F) :
952 ∃ κ : OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F),
953 Continuous κ ∧
954 (∀ q : OpenSubgroupRightQuotient H, κ (q, x0) = 1) ∧
955 κ (openSubgroupRightCoset H (1 : F), x0) = 1 ∧
957 IsClosed (Set.range κ) ∧
959 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
960 (Set.range κ)
961 ⟨κ (openSubgroupRightCoset H (1 : F), x0),
962 ⟨(openSubgroupRightCoset H (1 : F), x0), rfl⟩⟩
963 ↥(H : Subgroup F) Subtype.val := by
964 classical
965 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
966 letI : T2Space F := IsProCGroup.t2Space hF.isProC
967 letI : TotallyDisconnectedSpace F := IsProCGroup.totallyDisconnectedSpace hF.isProC
968 let n : ℕ := Nat.card (F ⧸ (H : Subgroup F))
969 let hn : Nat.card (F ⧸ (H : Subgroup F)) = n := rfl
970 let P := openSubgroupIndexActionRange (G := F) H hn
971 let ρ : F →ₜ* P := openSubgroupIndexActionRangeContinuousHom (G := F) H hn
972 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
973 let K : Subgroup P := MulAction.stabilizer P q0
974 let βF : FreeGroup X →* F := FreeGroup.lift ι
975 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
976 letI : TopologicalSpace (FreeGroup X) := ⊥
977 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
978 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
979 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
980 ext g
981 constructor
982 · intro hg
983 change ρ g • q0 = q0 at hg
984 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := F) H hn g] at hg
985 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
986 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
987 simpa [QuotientGroup.eq] using hg
988 · intro hg
989 change ρ g • q0 = q0
990 exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem (G := F) H hn hg
991 have hβFdense : DenseRange βF :=
992 denseRange_freeGroupLift_of_topologicallyGenerates (F := F) (X := X) hF.generates_range
993 have hρsurj : Function.Surjective ρ := by
994 intro p
995 rcases p.down.2 with ⟨g, hg⟩
996 refine ⟨g, ?_⟩
997 apply ULift.ext
998 apply Subtype.ext
999 exact hg
1000 have hβdense : DenseRange β := by
1001 simpa [β, MonoidHom.comp_apply] using
1002 (Function.Surjective.denseRange hρsurj).comp hβFdense ρ.continuous_toFun
1003 have hβsurj : Function.Surjective β :=
1004 surjective_of_denseRange (F := FreeGroup X) (P := P) hβdense
1005 obtain ⟨T, hT⟩ := exists_rightSchreierTransversal (X := X) (Subgroup.comap β K)
1006 have hβFcomapDense :
1007 DenseRange
1008 ({ toFun := fun g : Subgroup.comap β K => ⟨βF g.1, g.2⟩
1009 map_one' := by simp only [ContinuousMonoidHom.coe_toMonoidHom, OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
1010 map_mul' := by
1011 intro a b
1012 ext
1014 Subgroup.comap β K →* ↥(Subgroup.comap ρ.toMonoidHom K)) := by
1015 have hρKopen : IsOpen ((Subgroup.comap ρ.toMonoidHom K : Subgroup F) : Set F) := by
1016 rw [hcomap]
1017 exact H.isOpen'
1019 (φ := βF) hβFdense (U := Subgroup.comap ρ.toMonoidHom K) hρKopen
1020 let Hc : OpenSubgroup F :=
1021 { toSubgroup := Subgroup.comap ρ.toMonoidHom K
1022 isOpen' := by
1023 rw [hcomap]
1024 exact H.isOpen' }
1025 have hHc : Hc = H := by
1026 ext g
1027 simpa [Hc] using congrArg (fun S : Subgroup F => g ∈ S) hcomap
1028 have hκgenPre :
1029 let τ := rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT
1030 let hτ := rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT
1031 let κ :
1032 Quotient (QuotientGroup.rightRel (Subgroup.comap ρ.toMonoidHom K)) × X →
1033 ↥(Subgroup.comap ρ.toMonoidHom K) :=
1034 fun p =>
1036 (H := Subgroup.comap ρ.toMonoidHom K) τ hτ (βF (FreeGroup.of p.2)) p.1
1038 (G := ↥(Subgroup.comap ρ.toMonoidHom K)) (Set.range κ) := by
1041 let GoalProp : OpenSubgroup F → Prop := fun J =>
1042 ∃ κ : OpenSubgroupRightQuotient J × X → ↥(J : Subgroup F),
1043 Continuous κ ∧
1044 (∀ q : OpenSubgroupRightQuotient J, κ (q, x0) = 1) ∧
1045 κ (openSubgroupRightCoset J (1 : F), x0) = 1 ∧
1047 IsClosed (Set.range κ) ∧
1049 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
1050 (Set.range κ)
1051 ⟨κ (openSubgroupRightCoset J (1 : F), x0),
1052 ⟨(openSubgroupRightCoset J (1 : F), x0), rfl⟩⟩
1053 ↥(J : Subgroup F) Subtype.val
1054 have hMain : GoalProp Hc := by
1055 letI : Finite (OpenSubgroupRightQuotient Hc) :=
1056 finite_openSubgroupRightQuotient (F := F) Hc
1057 letI : Fintype (OpenSubgroupRightQuotient Hc) :=
1058 fintype_openSubgroupRightQuotient (F := F) Hc
1059 letI : DiscreteTopology (OpenSubgroupRightQuotient Hc) :=
1060 discreteTopology_openSubgroupRightQuotient (F := F) Hc
1061 letI : MulAction F (OpenSubgroupRightQuotient Hc) :=
1062 rightCosetMulAction (Hc : Subgroup F)
1063 letI : ContinuousSMul F (OpenSubgroupRightQuotient Hc) := by
1064 refine ContinuousSMul.mk ?_
1065 refine (continuous_prod_of_discrete_right).2 ?_
1066 intro q
1067 convert
1069 (G := F) (H := (Hc : Subgroup F)) Hc.isOpen' q).comp continuous_inv using 1
1070 ext g
1072 let q1 : OpenSubgroupRightQuotient Hc := openSubgroupRightCoset Hc (1 : F)
1073 let τ : OpenSubgroupRightQuotient Hc → F := by
1074 simpa [Hc, OpenSubgroupRightQuotient] using
1075 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT)
1076 have hτ : ∀ q : OpenSubgroupRightQuotient Hc, Quotient.mk'' (τ q) = q := by
1077 intro q
1078 change
1079 Quotient.mk'' ((rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT) q) = q
1080 exact rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT q
1081 let κ : OpenSubgroupRightQuotient Hc × X → ↥(Hc : Subgroup F) :=
1082 fun p =>
1083 rightQuotientSectionCocycle (H := (Hc : Subgroup F)) τ hτ (βF (FreeGroup.of p.2)) p.1
1084 have hκgen :
1085 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Hc : Subgroup F)) (Set.range κ) := by
1086 simpa [κ, τ, Hc, OpenSubgroupRightQuotient, βF] using hκgenPre
1087 have hτcont : Continuous τ := continuous_of_discreteTopology
1088 have hκcont : Continuous κ := by
1089 simpa [κ, τ, Hc, OpenSubgroupRightQuotient, βF] using
1091 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) hτcont hF.continuous_ι)
1092 have hκ1 : κ (q1, x0) = 1 := by
1093 simpa [κ, rightSchreierGenerator, βF] using
1095 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q1) (x := x0) hF.map_base)
1096 have hκbase : ∀ q : OpenSubgroupRightQuotient Hc, κ (q, x0) = 1 := by
1097 intro q
1098 simpa [κ, rightSchreierGenerator, βF] using
1100 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0) hF.map_base)
1101 refine ⟨κ, hκcont, hκbase, hκ1, isCompact_range hκcont, (isCompact_range hκcont).isClosed, ?_⟩
1102 refine ⟨?_, continuous_subtype_val, ?_, ?_, ?_⟩
1103 · exact
1104 IsProCGroup.of_isClosed_subgroup
1105 (C := C) (G := F) hIso hSub hQuot hF.isProC (Hc : Subgroup F)
1106 (Subgroup.isClosed_of_isOpen (Hc : Subgroup F) Hc.isOpen')
1107 · simpa [hκ1]
1108 · have hrange :
1109 Set.range (Subtype.val : Set.range κ → ↥(Hc : Subgroup F)) = Set.range κ := by
1110 ext h
1111 constructor
1112 · rintro ⟨x, rfl⟩
1113 exact x.2
1114 · intro hh
1115 exact ⟨⟨h, hh⟩, rfl⟩
1116 simpa [hrange] using hκgen
1117 · intro B _ _ _ hB φB hφB hφB0 hgenB
1118 letI : T2Space B := IsProCGroup.t2Space hB
1119 letI : CompactSpace B := IsProCGroup.compactSpace hB
1120 letI : TotallyDisconnectedSpace B := IsProCGroup.totallyDisconnectedSpace hB
1121 let ξ : X → PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1122 fun x => ⟨fun q => φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩, ι x⟩
1123 have hξcont : Continuous ξ := by
1124 refine continuous_induced_rng.2 ?_
1125 change Continuous fun x : X => ((ξ x).left, (ξ x).right)
1126 have hleft : Continuous fun x : X => (ξ x).left := by
1127 refine continuous_pi ?_
1128 intro q
1129 have hqcont : Continuous fun x : X => κ (q, x) := by
1130 simpa using hκcont.comp (continuous_const.prodMk continuous_id)
1131 have hsub :
1132 Continuous fun x : X => (⟨κ (q, x), ⟨(q, x), rfl⟩⟩ : Set.range κ) :=
1133 Continuous.subtype_mk hqcont (by
1134 intro x
1135 exact ⟨(q, x), rfl⟩)
1136 simpa [ξ] using hφB.comp hsub
1137 have hright : Continuous fun x : X => (ξ x).right := by
1138 simpa [ξ] using hF.continuous_ι
1139 exact hleft.prodMk hright
1140 have hξ0 : ξ x0 = 1 := by
1141 apply SemidirectProduct.ext
1142 · funext q
1143 have hq1 : κ (q, x0) = 1 := by
1144 simpa [κ, rightSchreierGenerator, βF] using
1146 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0)
1147 hF.map_base)
1148 have hsrc :
1149 (⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ : Set.range κ) =
1150 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1151 apply Subtype.ext
1152 exact hq1.trans hκ1.symm
1153 calc
1154 (ξ x0).left q = φB ⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ := rfl
1155 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1156 _ = 1 := hφB0
1157 · simp only [hF.map_base, SemidirectProduct.one_right, ξ]
1158 let W : Subgroup (PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F) :=
1159 (Subgroup.closure (Set.range ξ)).topologicalClosure
1160 have hWreath :
1161 IsProCGroup C (PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F) := by
1162 exact
1164 (C := C) hForm hIso hExt hB hF.isProC
1165 have hWproC : IsProCGroup C W := by
1166 exact
1167 IsProCGroup.of_isClosed_subgroup
1168 (C := C) (G := PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F)
1169 hIso hSub hQuot hWreath W (Subgroup.isClosed_topologicalClosure _)
1170 let ξW : X → W := fun x =>
1171 ⟨ξ x, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩)⟩
1172 have hξWcont : Continuous ξW :=
1173 Continuous.subtype_mk hξcont (by
1174 intro x
1175 exact Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩))
1176 have hξW0 : ξW x0 = 1 := by
1177 apply Subtype.ext
1178 exact hξ0
1179 have hξWgen :
1180 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range ξW) := by
1181 simpa [W, ξW] using
1183 rcases hF.existsUnique_lift hWproC ξW hξWcont hξW0 hξWgen with
1184 ⟨ηW, hηW, _⟩
1185 let η : F →* PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1186 W.subtype.comp ηW
1187 have hηcont : Continuous η := by
1188 simpa [η] using (continuous_subtype_val.comp hηW.1)
1189 have hηgen : ∀ x : X, η (ι x) = ξ x := by
1190 intro x
1191 simpa [η, ξW] using congrArg Subtype.val (hηW.2 x)
1192 have hηright :
1193 (SemidirectProduct.rightHom :
1194 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1195 MonoidHom.id F := by
1196 rcases
1197 hF.existsUnique_lift hF.isProC ι hF.continuous_ι hF.map_base hF.generates_range with
1198 ⟨u, hu, huuniq⟩
1199 have hu_id : MonoidHom.id F = u := by
1200 exact
1201 huuniq (MonoidHom.id F)
1202 ⟨by simpa using (continuous_id : Continuous fun x : F => x), by intro x; rfl⟩
1203 have hu_η :
1204 (SemidirectProduct.rightHom :
1205 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1206 u := by
1207 let v : F →* F :=
1208 (SemidirectProduct.rightHom :
1209 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η
1210 have hη_on_gen :
1211 ∀ x : X, v (ι x) = ι x := by
1212 intro x
1213 have hx := congrArg
1214 (fun z : PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F => z.right)
1215 (hηgen x)
1216 simpa [v, MonoidHom.comp_apply, ξ] using hx
1217 have hvu : v = u := by
1218 exact huuniq v ⟨continuous_permutationalWreathProduct_right.comp hηcont, hη_on_gen⟩
1219 simpa [v] using hvu
1220 calc
1221 (SemidirectProduct.rightHom :
1222 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η = u :=
1223 hu_η
1224 _ = MonoidHom.id F := hu_id.symm
1225 have hηcoord :
1226 ∀ q : OpenSubgroupRightQuotient Hc, ∀ x : X,
1227 wreathLeftCoordinate η q (ι x) =
1228 φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩ := by
1229 intro q x
1230 change (η (ι x)).left q = _
1231 rw [hηgen]
1232 have hηone :
1233 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
1234 schreierGenerator (X := X) hT t x = 1 →
1236 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1237 (βF (FreeGroup.of x)) = 1 := by
1238 intro t ht x hsg
1239 have hmap :
1240 κ (Quotient.mk'' (βF t), x) = 1 := by
1241 simpa [κ, τ, βF, hsg] using
1244 have hsrc :
1245 (⟨κ (Quotient.mk'' (βF t), x), ⟨(Quotient.mk'' (βF t), x), rfl⟩⟩ : Set.range κ) =
1246 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1247 apply Subtype.ext
1248 exact hmap.trans hκ1.symm
1249 calc
1251 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1252 (βF (FreeGroup.of x))
1253 =
1255 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) (ι x) := by
1256 simp only [FreeGroup.lift_apply_of, βF]
1257 _ = φB ⟨κ (Quotient.mk'' (βF t), x), ⟨(Quotient.mk'' (βF t), x), rfl⟩⟩ :=
1258 hηcoord _ _
1259 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1260 _ = 1 := hφB0
1261 have hτpure :
1262 ∀ q : OpenSubgroupRightQuotient Hc,
1263 wreathLeftCoordinate η q1 (τ q) = 1 := by
1264 intro q
1265 simpa [q1, τ, Hc, OpenSubgroupRightQuotient, βF] using
1268 (hone := hηone) q)
1269 let g : ↥(Hc : Subgroup F) →* B :=
1270 rightQuotientBasepointProjectionHom (H := (Hc : Subgroup F)) η hηright
1271 have hgcont : Continuous g := by
1272 simpa [g, rightQuotientBasepointProjectionHom, wreathLeftCoordinate] using
1274 (S := OpenSubgroupRightQuotient Hc) (G := F) q1).comp
1275 (hηcont.comp continuous_subtype_val)
1276 have hgfac : ∀ y : Set.range κ, g y.1 = φB y := by
1277 rintro ⟨y, ⟨⟨q, x⟩, hy⟩⟩
1278 subst y
1279 change g (κ (q, x)) = φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩
1280 calc
1281 g (κ (q, x)) = wreathLeftCoordinate η q (βF (FreeGroup.of x)) := by
1282 simpa [g, κ, τ, βF] using
1284 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) η hηright hτpure q x)
1285 _ = wreathLeftCoordinate η q (ι x) := by simp only [FreeGroup.lift_apply_of, βF]
1286 _ = φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩ := hηcoord q x
1287 refine ⟨g, ⟨hgcont, hgfac⟩, ?_⟩
1288 intro g' hg'
1289 symm
1291 (G := ↥(Hc : Subgroup F)) (A := B) hκgen hgcont hg'.1
1292 intro h hh
1293 exact (hgfac ⟨h, hh⟩).trans (hg'.2 ⟨h, hh⟩).symm
1294 exact cast (congrArg GoalProp hHc) hMain
1296end ExactPointedRightSchreierGeneration
1301 {C : ProCGroups.FiniteGroupClass.{u}}
1302 (hForm : ProCGroups.FiniteGroupClass.Formation C)
1303 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
1304 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
1305 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
1306 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
1307 {X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
1308 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1309 {ι : X → F}
1310 (hF : IsPointedFreeProCGroupOn
1311 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X x0 F ι)
1312 (H : OpenSubgroup F) (x : X) {N : ℕ}
1313 (hN : 0 < N)
1314 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
1315 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
1316 ∃ κ : OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F),
1317 Continuous κ ∧
1318 (∀ q : OpenSubgroupRightQuotient H, κ (q, x0) = 1) ∧
1319 κ (openSubgroupRightCoset H (1 : F), x0) = 1 ∧
1320 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈ Set.range κ ∧
1322 IsClosed (Set.range κ) ∧
1324 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
1325 (Set.range κ)
1326 ⟨κ (openSubgroupRightCoset H (1 : F), x0),
1327 ⟨(openSubgroupRightCoset H (1 : F), x0), rfl⟩⟩
1328 ↥(H : Subgroup F) Subtype.val := by
1329 classical
1330 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
1331 letI : T2Space F := IsProCGroup.t2Space hF.isProC
1332 letI : TotallyDisconnectedSpace F := IsProCGroup.totallyDisconnectedSpace hF.isProC
1333 let n : ℕ := Nat.card (F ⧸ (H : Subgroup F))
1334 let hn : Nat.card (F ⧸ (H : Subgroup F)) = n := rfl
1335 let P := openSubgroupIndexActionRange (G := F) H hn
1336 let ρ : F →ₜ* P := openSubgroupIndexActionRangeContinuousHom (G := F) H hn
1337 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
1338 let K : Subgroup P := MulAction.stabilizer P q0
1339 let βF : FreeGroup X →* F := FreeGroup.lift ι
1340 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
1341 let βc : Subgroup.comap β K →* ↥(Subgroup.comap ρ.toMonoidHom K) :=
1342 { toFun := fun g => ⟨βF g.1, g.2⟩
1343 map_one' := by simp only [ContinuousMonoidHom.coe_toMonoidHom, OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
1344 map_mul' := by
1345 intro a b
1346 ext
1348 letI : TopologicalSpace (FreeGroup X) := ⊥
1349 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
1350 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
1351 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
1352 ext g
1353 constructor
1354 · intro hg
1355 change ρ g • q0 = q0 at hg
1356 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := F) H hn g] at hg
1357 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
1358 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
1359 simpa [QuotientGroup.eq] using hg
1360 · intro hg
1361 change ρ g • q0 = q0
1362 exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem (G := F) H hn hg
1363 have hβFdense : DenseRange βF :=
1364 denseRange_freeGroupLift_of_topologicallyGenerates (F := F) (X := X) hF.generates_range
1365 have hρsurj : Function.Surjective ρ := by
1366 intro p
1367 rcases p.down.2 with ⟨g, hg⟩
1368 refine ⟨g, ?_⟩
1369 apply ULift.ext
1370 apply Subtype.ext
1371 exact hg
1372 have hβdense : DenseRange β := by
1373 simpa [β, MonoidHom.comp_apply] using
1374 (Function.Surjective.denseRange hρsurj).comp hβFdense ρ.continuous_toFun
1375 have hβsurj : Function.Surjective β :=
1376 surjective_of_denseRange (F := FreeGroup X) (P := P) hβdense
1377 have hpowβ : (FreeGroup.of x) ^ N ∈ Subgroup.comap β K := by
1378 change βF ((FreeGroup.of x) ^ N) ∈ Subgroup.comap ρ.toMonoidHom K
1379 rw [hcomap]
1380 simpa [βF, MonoidHom.map_pow] using hpow
1381 have hminβ :
1382 ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ Subgroup.comap β K := by
1383 intro m hm0 hmN hm
1384 apply hmin m hm0 hmN
1385 change βF ((FreeGroup.of x) ^ m) ∈ Subgroup.comap ρ.toMonoidHom K at hm
1386 rw [hcomap] at hm
1387 simpa [βF, MonoidHom.map_pow] using hm
1388 obtain ⟨T, hT, hpred, hsg⟩ :=
1390 (X := X) (L := Subgroup.comap β K) x hN hpowβ hminβ
1391 have hβFcomapDense : DenseRange βc := by
1392 have hρKopen : IsOpen ((Subgroup.comap ρ.toMonoidHom K : Subgroup F) : Set F) := by
1393 rw [hcomap]
1394 exact H.isOpen'
1395 simpa [βc] using
1397 (φ := βF) hβFdense (U := Subgroup.comap ρ.toMonoidHom K) hρKopen)
1398 let Hc : OpenSubgroup F :=
1399 { toSubgroup := Subgroup.comap ρ.toMonoidHom K
1400 isOpen' := by
1401 rw [hcomap]
1402 exact H.isOpen' }
1403 have hHc : Hc = H := by
1404 ext g
1405 simpa [Hc] using congrArg (fun S : Subgroup F => g ∈ S) hcomap
1406 have hκgenPre :
1407 let τ := rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT
1408 let hτ := rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT
1409 let κ :
1410 Quotient (QuotientGroup.rightRel (Subgroup.comap ρ.toMonoidHom K)) × X →
1411 ↥(Subgroup.comap ρ.toMonoidHom K) :=
1412 fun p =>
1414 (H := Subgroup.comap ρ.toMonoidHom K) τ hτ (βF (FreeGroup.of p.2)) p.1
1416 (G := ↥(Subgroup.comap ρ.toMonoidHom K)) (Set.range κ) := by
1419 let GoalProp : OpenSubgroup F → Prop := fun J =>
1420 ∃ κ : OpenSubgroupRightQuotient J × X → ↥(J : Subgroup F),
1421 Continuous κ ∧
1422 (∀ q : OpenSubgroupRightQuotient J, κ (q, x0) = 1) ∧
1423 κ (openSubgroupRightCoset J (1 : F), x0) = 1 ∧
1424 (∃ hpowJ : (ι x) ^ N ∈ (J : Subgroup F),
1425 (⟨(ι x) ^ N, hpowJ⟩ : ↥(J : Subgroup F)) ∈ Set.range κ) ∧
1427 IsClosed (Set.range κ) ∧
1429 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
1430 (Set.range κ)
1431 ⟨κ (openSubgroupRightCoset J (1 : F), x0),
1432 ⟨(openSubgroupRightCoset J (1 : F), x0), rfl⟩⟩
1433 ↥(J : Subgroup F) Subtype.val
1434 have hMain : GoalProp Hc := by
1435 letI : Finite (OpenSubgroupRightQuotient Hc) :=
1436 finite_openSubgroupRightQuotient (F := F) Hc
1437 letI : Fintype (OpenSubgroupRightQuotient Hc) :=
1438 fintype_openSubgroupRightQuotient (F := F) Hc
1439 letI : DiscreteTopology (OpenSubgroupRightQuotient Hc) :=
1440 discreteTopology_openSubgroupRightQuotient (F := F) Hc
1441 letI : MulAction F (OpenSubgroupRightQuotient Hc) :=
1442 rightCosetMulAction (Hc : Subgroup F)
1443 letI : ContinuousSMul F (OpenSubgroupRightQuotient Hc) := by
1444 refine ContinuousSMul.mk ?_
1445 refine (continuous_prod_of_discrete_right).2 ?_
1446 intro q
1447 convert
1449 (G := F) (H := (Hc : Subgroup F)) Hc.isOpen' q).comp continuous_inv using 1
1450 ext g
1452 let q1 : OpenSubgroupRightQuotient Hc := openSubgroupRightCoset Hc (1 : F)
1453 let τ : OpenSubgroupRightQuotient Hc → F := by
1454 simpa [Hc, OpenSubgroupRightQuotient] using
1455 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT)
1456 have hτ : ∀ q : OpenSubgroupRightQuotient Hc, Quotient.mk'' (τ q) = q := by
1457 intro q
1458 change
1459 Quotient.mk'' ((rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT) q) = q
1460 exact rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT q
1461 let κ : OpenSubgroupRightQuotient Hc × X → ↥(Hc : Subgroup F) :=
1462 fun p =>
1463 rightQuotientSectionCocycle (H := (Hc : Subgroup F)) τ hτ (βF (FreeGroup.of p.2)) p.1
1464 have hκgen :
1465 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Hc : Subgroup F)) (Set.range κ) := by
1466 simpa [κ, τ, Hc, OpenSubgroupRightQuotient, βF] using hκgenPre
1467 have hτcont : Continuous τ := continuous_of_discreteTopology
1468 have hκcont : Continuous κ := by
1469 simpa [κ, τ, Hc, OpenSubgroupRightQuotient, βF] using
1471 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) hτcont hF.continuous_ι)
1472 have hκ1 : κ (q1, x0) = 1 := by
1473 simpa [κ, rightSchreierGenerator, βF] using
1475 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q1) (x := x0) hF.map_base)
1476 have hκbase : ∀ q : OpenSubgroupRightQuotient Hc, κ (q, x0) = 1 := by
1477 intro q
1478 simpa [κ, rightSchreierGenerator, βF] using
1480 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0) hF.map_base)
1481 have hpowHc : (ι x) ^ N ∈ (Hc : Subgroup F) := by
1482 change (ι x) ^ N ∈ Subgroup.comap ρ.toMonoidHom K
1483 rw [hcomap]
1484 exact hpow
1485 have hxNrange : (⟨(ι x) ^ N, hpowHc⟩ : ↥(Hc : Subgroup F)) ∈ Set.range κ := by
1486 have hmap :
1487 κ ((Quotient.mk'' (βF ((FreeGroup.of x) ^ (N - 1))) : OpenSubgroupRightQuotient Hc), x) =
1488 βc (schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x) := by
1489 simpa [βc, κ, τ, Hc, OpenSubgroupRightQuotient, βF] using
1492 have hβc_pow : βc ⟨(FreeGroup.of x) ^ N, hpowβ⟩ = ⟨(ι x) ^ N, hpowHc⟩ := by
1493 apply Subtype.ext
1494 simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_mk, OneHom.coe_mk, MonoidHom.map_pow,
1495 FreeGroup.lift_apply_of, βc, βF]
1496 refine
1497 ⟨((Quotient.mk'' (βF ((FreeGroup.of x) ^ (N - 1))) :
1498 OpenSubgroupRightQuotient Hc), x), ?_⟩
1499 calc
1500 κ ((Quotient.mk'' (βF ((FreeGroup.of x) ^ (N - 1))) : OpenSubgroupRightQuotient Hc), x) =
1501 βc (schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x) := hmap
1502 _ = βc ⟨(FreeGroup.of x) ^ N, hpowβ⟩ := by rw [hsg]
1503 _ = ⟨(ι x) ^ N, hpowHc⟩ := hβc_pow
1504 refine ⟨κ, hκcont, hκbase, hκ1, ⟨hpowHc, hxNrange⟩,
1505 isCompact_range hκcont, (isCompact_range hκcont).isClosed, ?_⟩
1506 refine ⟨?_, continuous_subtype_val, ?_, ?_, ?_⟩
1507 · exact
1508 IsProCGroup.of_isClosed_subgroup
1509 (C := C) (G := F) hIso hSub hQuot hF.isProC (Hc : Subgroup F)
1510 (Subgroup.isClosed_of_isOpen (Hc : Subgroup F) Hc.isOpen')
1511 · simpa [hκ1]
1512 · have hrange :
1513 Set.range (Subtype.val : Set.range κ → ↥(Hc : Subgroup F)) = Set.range κ := by
1514 ext h
1515 constructor
1516 · rintro ⟨x, rfl⟩
1517 exact x.2
1518 · intro hh
1519 exact ⟨⟨h, hh⟩, rfl⟩
1520 simpa [hrange] using hκgen
1521 · intro B _ _ _ hB φB hφB hφB0 hgenB
1522 letI : T2Space B := IsProCGroup.t2Space hB
1523 letI : CompactSpace B := IsProCGroup.compactSpace hB
1524 letI : TotallyDisconnectedSpace B := IsProCGroup.totallyDisconnectedSpace hB
1525 let ξ : X → PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1526 fun x => ⟨fun q => φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩, ι x⟩
1527 have hξcont : Continuous ξ := by
1528 refine continuous_induced_rng.2 ?_
1529 change Continuous fun x : X => ((ξ x).left, (ξ x).right)
1530 have hleft : Continuous fun x : X => (ξ x).left := by
1531 refine continuous_pi ?_
1532 intro q
1533 have hqcont : Continuous fun x : X => κ (q, x) := by
1534 simpa using hκcont.comp (continuous_const.prodMk continuous_id)
1535 have hsub :
1536 Continuous fun x : X => (⟨κ (q, x), ⟨(q, x), rfl⟩⟩ : Set.range κ) :=
1537 Continuous.subtype_mk hqcont (by
1538 intro x
1539 exact ⟨(q, x), rfl⟩)
1540 simpa [ξ] using hφB.comp hsub
1541 have hright : Continuous fun x : X => (ξ x).right := by
1542 simpa [ξ] using hF.continuous_ι
1543 exact hleft.prodMk hright
1544 have hξ0 : ξ x0 = 1 := by
1545 apply SemidirectProduct.ext
1546 · funext q
1547 have hq1 : κ (q, x0) = 1 := by
1548 simpa [κ, rightSchreierGenerator, βF] using
1550 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0)
1551 hF.map_base)
1552 have hsrc :
1553 (⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ : Set.range κ) =
1554 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1555 apply Subtype.ext
1556 exact hq1.trans hκ1.symm
1557 calc
1558 (ξ x0).left q = φB ⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ := rfl
1559 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1560 _ = 1 := hφB0
1561 · simp only [hF.map_base, SemidirectProduct.one_right, ξ]
1562 let W : Subgroup (PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F) :=
1563 (Subgroup.closure (Set.range ξ)).topologicalClosure
1564 have hWreath :
1565 IsProCGroup C (PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F) := by
1566 exact
1568 (C := C) hForm hIso hExt hB hF.isProC
1569 have hWproC : IsProCGroup C W := by
1570 exact
1571 IsProCGroup.of_isClosed_subgroup
1572 (C := C) (G := PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F)
1573 hIso hSub hQuot hWreath W (Subgroup.isClosed_topologicalClosure _)
1574 let ξW : X → W := fun x =>
1575 ⟨ξ x, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩)⟩
1576 have hξWcont : Continuous ξW :=
1577 Continuous.subtype_mk hξcont (by
1578 intro x
1579 exact Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩))
1580 have hξW0 : ξW x0 = 1 := by
1581 apply Subtype.ext
1582 exact hξ0
1583 have hξWgen :
1584 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range ξW) := by
1585 simpa [W, ξW] using
1587 rcases hF.existsUnique_lift hWproC ξW hξWcont hξW0 hξWgen with
1588 ⟨ηW, hηW, _⟩
1589 let η : F →* PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1590 W.subtype.comp ηW
1591 have hηcont : Continuous η := by
1592 simpa [η] using (continuous_subtype_val.comp hηW.1)
1593 have hηgen : ∀ x : X, η (ι x) = ξ x := by
1594 intro x
1595 simpa [η, ξW] using congrArg Subtype.val (hηW.2 x)
1596 have hηright :
1597 (SemidirectProduct.rightHom :
1598 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1599 MonoidHom.id F := by
1600 rcases
1601 hF.existsUnique_lift hF.isProC ι hF.continuous_ι hF.map_base hF.generates_range with
1602 ⟨u, hu, huuniq⟩
1603 have hu_id : MonoidHom.id F = u := by
1604 exact
1605 huuniq (MonoidHom.id F)
1606 ⟨by simpa using (continuous_id : Continuous fun x : F => x), by intro x; rfl⟩
1607 have hu_η :
1608 (SemidirectProduct.rightHom :
1609 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1610 u := by
1611 let v : F →* F :=
1612 (SemidirectProduct.rightHom :
1613 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η
1614 have hη_on_gen :
1615 ∀ x : X, v (ι x) = ι x := by
1616 intro x
1617 have hx := congrArg
1618 (fun z : PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F => z.right)
1619 (hηgen x)
1620 simpa [v, MonoidHom.comp_apply, ξ] using hx
1621 have hvu : v = u := by
1622 exact huuniq v ⟨continuous_permutationalWreathProduct_right.comp hηcont, hη_on_gen⟩
1623 simpa [v] using hvu
1624 calc
1625 (SemidirectProduct.rightHom :
1626 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η = u :=
1627 hu_η
1628 _ = MonoidHom.id F := hu_id.symm
1629 have hηcoord :
1630 ∀ q : OpenSubgroupRightQuotient Hc, ∀ x : X,
1631 wreathLeftCoordinate η q (ι x) =
1632 φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩ := by
1633 intro q x
1634 change (η (ι x)).left q = _
1635 rw [hηgen]
1636 have hηone :
1637 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
1638 schreierGenerator (X := X) hT t x = 1 →
1640 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1641 (βF (FreeGroup.of x)) = 1 := by
1642 intro t ht x' hsg'
1643 have hmap :
1644 κ (Quotient.mk'' (βF t), x') = 1 := by
1645 simpa [κ, τ, βF, hsg'] using
1648 have hsrc :
1649 (⟨κ (Quotient.mk'' (βF t), x'), ⟨(Quotient.mk'' (βF t), x'), rfl⟩⟩ : Set.range κ) =
1650 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1651 apply Subtype.ext
1652 exact hmap.trans hκ1.symm
1653 calc
1655 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1656 (βF (FreeGroup.of x'))
1657 =
1659 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) (ι x') := by
1660 simp only [FreeGroup.lift_apply_of, βF]
1661 _ = φB ⟨κ (Quotient.mk'' (βF t), x'), ⟨(Quotient.mk'' (βF t), x'), rfl⟩⟩ :=
1662 hηcoord _ _
1663 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1664 _ = 1 := hφB0
1665 have hτpure :
1666 ∀ q : OpenSubgroupRightQuotient Hc,
1667 wreathLeftCoordinate η q1 (τ q) = 1 := by
1668 intro q
1669 simpa [q1, τ, Hc, OpenSubgroupRightQuotient, βF] using
1672 (hone := hηone) q)
1673 let g : ↥(Hc : Subgroup F) →* B :=
1674 rightQuotientBasepointProjectionHom (H := (Hc : Subgroup F)) η hηright
1675 have hgcont : Continuous g := by
1676 simpa [g, rightQuotientBasepointProjectionHom, wreathLeftCoordinate] using
1678 (S := OpenSubgroupRightQuotient Hc) (G := F) q1).comp
1679 (hηcont.comp continuous_subtype_val)
1680 have hgfac : ∀ y : Set.range κ, g y.1 = φB y := by
1681 rintro ⟨y, ⟨⟨q, x'⟩, hy⟩⟩
1682 subst y
1683 change g (κ (q, x')) = φB ⟨κ (q, x'), ⟨(q, x'), rfl⟩⟩
1684 calc
1685 g (κ (q, x')) = wreathLeftCoordinate η q (βF (FreeGroup.of x')) := by
1686 simpa [g, κ, τ, βF] using
1688 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) η hηright hτpure q x')
1689 _ = wreathLeftCoordinate η q (ι x') := by simp only [FreeGroup.lift_apply_of, βF]
1690 _ = φB ⟨κ (q, x'), ⟨(q, x'), rfl⟩⟩ := hηcoord q x'
1691 refine ⟨g, ⟨hgcont, hgfac⟩, ?_⟩
1692 intro g' hg'
1693 symm
1695 (G := ↥(Hc : Subgroup F)) (A := B) hκgen hgcont hg'.1
1696 intro h hh
1697 exact (hgfac ⟨h, hh⟩).trans (hg'.2 ⟨h, hh⟩).symm
1698 rcases cast (congrArg GoalProp hHc) hMain with
1699 ⟨κ, hκcont, hκbase, hκ1, hpowRange, hκcompact, hκclosed, hκfree⟩
1700 rcases hpowRange with ⟨hpowH, hxNrange⟩
1701 refine ⟨κ, hκcont, hκbase, hκ1, ?_, hκcompact, hκclosed, hκfree⟩
1702 simpa using hxNrange
1706end Profinite
1707end ReidemeisterSchreier