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

Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.ExactRightSchreierGeneration

1import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel
2import ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals
4/-!
5# Exact right-Schreier generation
7Using a transported right-coset section and the wreath-product embedding, this
8module identifies the concrete right-Schreier cocycles that topologically
9generate an open subgroup. It also proves the finite-quotient lifting
10statements used to recognize the resulting dense abstract free group as the
11required pro-\(C\) completion.
12-/
14open Set
15open scoped Topology Pointwise
17namespace ReidemeisterSchreier
18namespace Profinite
20open ProCGroups
21open ProCGroups.FreeProC
22open ProCGroups.ProC
23open ProCGroups.WreathProducts
24open ReidemeisterSchreier.Discrete
25open ReidemeisterSchreier.Discrete.OpenSubgroups
27universe u v
29section ExactRightSchreierGeneration
31open FreeGroup
33variable {X : Type u} [TopologicalSpace X]
34variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
35 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
36variable {P : Type u} [Group P]
37variable {ι : X → F}
38variable {φ : FreeGroup X →* F}
39variable {π : F →* P}
40variable {K : Subgroup P}
42omit [TopologicalSpace X] [Group F] [TopologicalSpace F] [IsTopologicalGroup F] ι φ π in
43/--
44The distinguished profinite minimal-power Schreier generator agrees with the generator supplied
45by the discrete minimal-power Schreier-transversal theorem for the finite quotient/comap
46subgroup.
47-/
48theorem profinite_minimalPower_schreierGenerator_lifts_discrete
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
60 exists_rightSchreierTransversal_of_minimalGeneratorPower
61 (X := X) (L := Subgroup.comap β K) x hN hpow hmin
63omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] in
64/--
65On elements of the abstract Schreier transversal, the transported cocycle in the ambient group
66matches the image of the discrete Schreier generator.
67-/
68theorem map_schreierGenerator_eq_cocycle
69 [DecidableEq X]
70 {T : Set (FreeGroup X)}
71 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
72 (hβsurj : Function.Surjective (π.comp φ))
73 {t : FreeGroup X} (ht : t ∈ T) (x : X) :
74 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
75 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
76 let Hc : Subgroup F := Subgroup.comap π K
77 rightQuotientSectionCocycle (H := Hc) τ hτ (φ (FreeGroup.of x))
78 (Quotient.mk'' (φ t)) =
79 ⟨φ (schreierGenerator (X := X) hT t x), by
80 change (π.comp φ) ↑(schreierGenerator (X := X) hT t x) ∈ K
81 exact (schreierGenerator (X := X) hT t x).2⟩ := by
82 classical
83 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
84 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
85 let Hc : Subgroup F := Subgroup.comap π K
86 letI : MulAction F (Quotient (QuotientGroup.rightRel Hc)) :=
87 rightCosetMulAction Hc
88 let rep := schreierRepresentative (X := X) hT (t * FreeGroup.of x)
89 have hτt :
90 τ (Quotient.mk'' (φ t)) = φ t := by
91 simpa [τ] using
92 (rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT ht)
93 have hrep_rel :
94 QuotientGroup.rightRel Hc (φ ((rep : T) : FreeGroup X)) (φ (t * FreeGroup.of x)) := by
95 rw [QuotientGroup.rightRel_apply]
96 dsimp [Hc]
97 change π (φ (t * FreeGroup.of x) * (φ ((rep : T) : FreeGroup X))⁻¹) ∈ K
98 have hrel :
99 t * FreeGroup.of x * (((rep : T) : FreeGroup X))⁻¹ ∈
100 Subgroup.comap (π.comp φ) K := by
101 exact hT.1.mul_inv_toRightFun_mem (t * FreeGroup.of x)
102 simpa [MonoidHom.comp_apply, MonoidHom.map_mul, MonoidHom.map_inv] using hrel
103 have hqnext :
104 (φ (FreeGroup.of x))⁻¹ • (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) =
105 Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := by
106 calc
107 (φ (FreeGroup.of x))⁻¹ • (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))
108 = Quotient.mk'' (φ t * φ (FreeGroup.of x)) := by
109 rw [rightCosetMulAction_inv_mk_smul (H := Hc) (φ (FreeGroup.of x)) (φ t)]
110 _ = Quotient.mk'' (φ (t * FreeGroup.of x)) := by
111 simp only [MonoidHom.map_mul]
112 _ = Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := (Quotient.sound' hrep_rel).symm
113 have hτnext :
114 τ (Quotient.mk'' (φ t * φ (FreeGroup.of x))) =
115 φ ((rep : T) : FreeGroup X) := by
116 have hqnext' :
117 (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
118 Quotient (QuotientGroup.rightRel Hc)) =
119 Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := by
120 calc
121 (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
122 Quotient (QuotientGroup.rightRel Hc))
123 = Quotient.mk'' (φ (t * FreeGroup.of x)) := by
124 simp only [MonoidHom.map_mul]
125 _ = Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := (Quotient.sound' hrep_rel).symm
126 rw [hqnext']
127 exact
128 rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT rep.2
129 have hτrep :
130 τ ((φ (FreeGroup.of x))⁻¹ •
131 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))) =
132 φ ((rep : T) : FreeGroup X) := by
133 have hrep_sec :
134 τ (Quotient.mk'' (φ ((rep : T) : FreeGroup X))) =
135 φ ((rep : T) : FreeGroup X) :=
136 rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT rep.2
137 exact hqnext ▸ hrep_sec
138 apply Subtype.ext
139 change
140 τ (Quotient.mk'' (φ t)) * φ (FreeGroup.of x) *
141 (τ ((φ (FreeGroup.of x))⁻¹ •
142 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))))⁻¹ =
143 φ ↑(schreierGenerator hT t x)
144 dsimp [rightQuotientSectionCocycle]
145 have hqnext'' :
146 (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
147 Quotient (QuotientGroup.rightRel Hc)) =
148 (φ (FreeGroup.of x))⁻¹ •
149 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) := by
150 simp only [rightCosetMulAction_mk_smul, inv_inv] at hqnext ⊢
151 have hqnext''' :
152 (Quotient.mk'' (φ t * (φ (FreeGroup.of x))⁻¹⁻¹) :
153 Quotient (QuotientGroup.rightRel Hc)) =
154 (φ (FreeGroup.of x))⁻¹ •
155 (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) := by
156 simpa only [inv_inv] using hqnext''
157 rw [hτt, hqnext''', hτrep]
158 simp only [mul_assoc, schreierGenerator, MonoidHom.map_mul, MonoidHom.map_inv, rep]
160omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] in
161/--
162On elements of the abstract Schreier transversal, the transported right Schreier cocycle in the
163ambient group is the image of the discrete Schreier generator.
164-/
165theorem rightQuotientSectionCocycle_eq_map_schreierGenerator_of_comap
166 [DecidableEq X]
167 {T : Set (FreeGroup X)}
168 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
169 (hβsurj : Function.Surjective (π.comp φ))
170 {t : FreeGroup X} (ht : t ∈ T) (x : X) :
171 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
172 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
173 let Hc : Subgroup F := Subgroup.comap π K
174 rightQuotientSectionCocycle (H := Hc) τ hτ (φ (FreeGroup.of x))
175 (Quotient.mk'' (φ t)) =
176 ⟨φ (schreierGenerator (X := X) hT t x), by
177 change (π.comp φ) ↑(schreierGenerator (X := X) hT t x) ∈ K
178 exact (schreierGenerator (X := X) hT t x).2⟩ := by
179 simpa using map_schreierGenerator_eq_cocycle
180 (X := X) (φ := φ) (π := π) (K := K) hT hβsurj ht x
182omit [TopologicalSpace X] [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
183/--
184The transported right Schreier cocycle topologically generates the ambient subgroup as soon as
185the dense abstract free subgroup remains dense after restricting to that subgroup.
186-/
187theorem topologicallyGenerates_range_transportedCocycle
188 [DecidableEq X]
189 {T : Set (FreeGroup X)}
190 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
191 (hβsurj : Function.Surjective (π.comp φ))
192 (hφdense :
193 DenseRange
194 ({ toFun := fun g : Subgroup.comap (π.comp φ) K => ⟨φ g.1, g.2⟩
195 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
196 map_mul' := by
197 intro a b
198 ext
199 simp only [Subgroup.coe_mul, map_mul]} :
200 Subgroup.comap (π.comp φ) K →* ↥(Subgroup.comap π K))) :
201 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
202 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
203 let κ :
204 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) × X →
205 ↥(Subgroup.comap π K) :=
206 fun p =>
207 rightQuotientSectionCocycle (H := Subgroup.comap π K) τ hτ (φ (FreeGroup.of p.2)) p.1
208 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Subgroup.comap π K)) (Set.range κ) := by
209 classical
210 let φL : Subgroup.comap (π.comp φ) K →* ↥(Subgroup.comap π K) :=
211 { toFun := fun g => ⟨φ g.1, g.2⟩
212 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
213 map_mul' := by
214 intro a b
215 ext
216 simp only [Subgroup.coe_mul, map_mul]}
217 let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
218 let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
219 let κ :
220 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) × X →
221 ↥(Subgroup.comap π K) :=
222 fun p =>
223 rightQuotientSectionCocycle (H := Subgroup.comap π K) τ hτ (φ (FreeGroup.of p.2)) p.1
224 have hsubset :
225 φL '' (schreierGeneratorSet (X := X) hT : Set (Subgroup.comap (π.comp φ) K)) ⊆
226 Set.range κ := by
227 intro z hz
228 rcases hz with ⟨s, hs, rfl⟩
229 rcases hs with ⟨t, ht, x, rfl, _⟩
230 refine ⟨(Quotient.mk'' (φ t), x), ?_⟩
231 simpa [κ, φL] using
232 (map_schreierGenerator_eq_cocycle (X := X) (φ := φ) (π := π) (K := K)
233 hT hβsurj ht x)
234 have hmap :
235 Subgroup.closure
236 (φL '' (schreierGeneratorSet (X := X) hT :
237 Set (Subgroup.comap (π.comp φ) K))) =
238 φL.range := by
239 calc
240 Subgroup.closure
241 (φL '' (schreierGeneratorSet (X := X) hT :
242 Set (Subgroup.comap (π.comp φ) K)))
243 = (Subgroup.closure
244 (schreierGeneratorSet (X := X) hT :
245 Set (Subgroup.comap (π.comp φ) K))).map φL := by
246 symm
247 exact MonoidHom.map_closure φL _
248 _ = (⊤ : Subgroup (Subgroup.comap (π.comp φ) K)).map φL := by
249 rw [closure_schreierGeneratorSet_eq_top (X := X) hT]
250 _ = φL.range := by
251 rw [← MonoidHom.range_eq_map]
252 have hgenImg :
253 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Subgroup.comap π K))
254 (φL '' (schreierGeneratorSet (X := X) hT :
255 Set (Subgroup.comap (π.comp φ) K))) := by
257 rw [hmap]
258 change Dense (Set.range φL)
259 exact hφdense
260 exact ProCGroups.Generation.topologicallyGenerates_mono (G := ↥(Subgroup.comap π K))
261 hgenImg hsubset
263end ExactRightSchreierGeneration
265section WreathTargetClosures
267variable {Y : Type u} [TopologicalSpace Y]
268variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
270omit [TopologicalSpace Y] in
271/--
272The topological closure of the subgroup generated by the range of a map is itself topologically
273generated by that range, viewed inside the closed subgroup.
274-/
275theorem topologicallyGenerates_topologicalClosure_of_range
276 (ξ : Y → G) :
277 let W : Subgroup G := (Subgroup.closure (Set.range ξ)).topologicalClosure
278 let ξW : Y → W := fun y =>
279 ⟨ξ y, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨y, rfl⟩)⟩
280 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range ξW) := by
281 classical
282 let A : Subgroup G := Subgroup.closure (Set.range ξ)
283 let W : Subgroup G := A.topologicalClosure
284 let ξW : Y → W := fun y =>
285 ⟨ξ y, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨y, rfl⟩)⟩
287 let B : Subgroup W := Subgroup.closure (Set.range ξW)
288 let i : W →* G := W.subtype
289 have hrange : i '' Set.range ξW = Set.range ξ := by
290 ext g
291 constructor
292 · rintro ⟨y, ⟨x, rfl⟩, rfl⟩
293 exact ⟨x, rfl⟩
294 · rintro ⟨y, rfl⟩
295 exact ⟨ξW y, ⟨y, rfl⟩, rfl⟩
296 have hmap : B.map i = A := by
297 calc
298 B.map i = Subgroup.closure (i '' Set.range ξW) := by
299 simpa [B] using (MonoidHom.map_closure i (Set.range ξW))
300 _ = A := by
301 simp only [hrange, A]
302 have himage : ((↑) : W → G) '' (B : Set W) = (A : Set G) := by
303 change i '' (B : Set W) = (A : Set G)
304 exact congrArg SetLike.coe hmap
305 have hsubset :
306 (W : Set G) ⊆ closure (((↑) : W → G) '' (B : Set W)) := by
307 rw [himage]
308 simp only [Subgroup.topologicalClosure_coe, subset_refl, W, A]
309 exact (Subtype.dense_iff).2 hsubset
311end WreathTargetClosures
313section UniquenessOnGeneratingRanges
315variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
316variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [T2Space A]
318omit [IsTopologicalGroup A] in
319/--
320Continuous homomorphisms into a Hausdorff topological group are determined by their values on
321any topologically generating set. It is a continuity claim, checked through the topology
322generated by finite-stage projections.
323-/
324theorem continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
325 {X : Set G}
327 {f g : G →* A} (hf : Continuous f) (hg : Continuous g)
328 (hfg : Set.EqOn f g X) :
329 f = g := by
330 let E : Subgroup G :=
331 { carrier := {x | f x = g x}
332 one_mem' := by simp only [mem_setOf_eq, map_one]
333 mul_mem' := by
334 intro a b ha hb
335 calc
336 f (a * b) = f a * f b := by simp only [map_mul]
337 _ = g a * g b := by rw [ha, hb]
338 _ = g (a * b) := by simp only [map_mul]
339 inv_mem' := by
340 intro a ha
341 simpa [ha] }
342 have hsub : X ⊆ (E : Set G) := by
343 intro x hx
344 exact hfg hx
345 have hclosure : Subgroup.closure X ≤ E :=
346 (Subgroup.closure_le (K := E)).2 hsub
347 let S : Subgroup G := Subgroup.closure X
348 have hDense : DenseRange (S.subtype : S → G) := by
349 have hDenseSet : Dense ((S : Subgroup G) : Set G) := by
350 simpa [S] using
352 simpa [DenseRange] using hDenseSet
353 have hEq :
354 (fun s : S => f s.1) = fun s : S => g s.1 := by
355 funext s
356 exact hclosure s.2
357 have hfun :
358 (fun x : G => f x) = fun x : G => g x := by
359 apply DenseRange.equalizer (f := (S.subtype : S → G)) hDense
360 · exact hf
361 · exact hg
362 · change (fun s : S => f s.1) = fun s : S => g s.1
363 exact hEq
364 ext x
365 exact congrArg (fun h : G → A => h x) hfun
367end UniquenessOnGeneratingRanges
369section TransportedSectionPurity
371variable {P : Type u} [Group P]
372variable {X : Type u} [DecidableEq X]
373variable {F : Type u} [Group F]
374variable {A : Type v} [Group A]
375variable {φ : FreeGroup X →* F} {π : F →* P} {K : Subgroup P}
376variable {T : Set (FreeGroup X)}
378/-- The right-coset comap carries the natural multiplication action induced by the subgroup map. -/
379instance instMulActionRightCosetComap :
380 MulAction F (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) :=
381 rightCosetMulAction (Subgroup.comap π K)
383/--
384On a transported Schreier transversal, basepoint coordinates are trivial once every tree-edge
385Schreier generator maps to \(1\).
386-/
387theorem wreathLeftCoordinate_basepoint_of_transversalWord
388 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
389 (ψ : F →* PermutationalWreathProduct A
390 (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F)
391 (hψ :
392 (SemidirectProduct.rightHom :
393 PermutationalWreathProduct A
394 (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F →* F).comp ψ =
395 MonoidHom.id F)
396 (hone :
397 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
398 schreierGenerator (X := X) hT t x = 1 →
399 wreathLeftCoordinate ψ
400 (Quotient.mk'' (φ t) :
401 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
402 (φ (FreeGroup.of x)) = 1)
403 (t : FreeGroup X) (ht : t ∈ T) :
404 wreathLeftCoordinate ψ
405 (Quotient.mk'' (1 : F) :
406 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
407 (φ t) = 1 := by
408 by_cases h1 : t = 1
409 · subst h1
410 simp only [wreathLeftCoordinate, map_one, SemidirectProduct.one_left, Pi.one_apply]
411 · rcases FreeGroup.lastLetter_cases_of_ne_one (X := X) h1 with ⟨x, hpos | hneg⟩
412 · rcases hpos with ⟨hw, hlast, hmul⟩
413 have hp : FreeGroup.prefixParent t ∈ T :=
414 prefixParent_mem_of_mem (X := X) hT ht
415 have hpure :
416 wreathLeftCoordinate ψ
417 (Quotient.mk'' (1 : F) :
418 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
419 (φ (FreeGroup.prefixParent t)) = 1 :=
420 wreathLeftCoordinate_basepoint_of_transversalWord hT ψ hψ hone
421 (FreeGroup.prefixParent t) hp
422 have hcoord :
423 wreathLeftCoordinate ψ
424 (Quotient.mk'' (φ (FreeGroup.prefixParent t)) :
425 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
426 (φ (FreeGroup.of x)) = 1 := by
427 exact hone hp x
428 (schreierGenerator_eq_one_of_prefixParent_last_pos (X := X) hT ht hw hlast)
429 have hq :
430 (φ (FreeGroup.prefixParent t))⁻¹ •
431 (Quotient.mk'' (1 : F) :
432 Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) =
433 Quotient.mk'' (φ (FreeGroup.prefixParent t)) := by
434 rw [rightCosetMulAction_inv_mk_smul
435 (H := Subgroup.comap π K) (φ (FreeGroup.prefixParent t)) 1]
436 simp only [one_mul]
437 have hmulφ :
438 φ (FreeGroup.prefixParent t) * φ (FreeGroup.of x) = φ t := by
439 simpa [MonoidHom.map_mul] using congrArg φ hmul
440 calc
441 wreathLeftCoordinate ψ
442 (Quotient.mk'' (1 : F) :
443 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
444 (φ t)
445 =
446 wreathLeftCoordinate ψ
447 (Quotient.mk'' (1 : F) :
448 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
449 (φ (FreeGroup.prefixParent t) * φ (FreeGroup.of x)) := by
450 rw [hmulφ]
451 _ =
452 wreathLeftCoordinate ψ
453 (Quotient.mk'' (1 : F) :
454 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
455 (φ (FreeGroup.prefixParent t)) *
456 wreathLeftCoordinate ψ
457 ((φ (FreeGroup.prefixParent t))⁻¹ •
458 (Quotient.mk'' (1 : F) :
459 Quotient (QuotientGroup.rightRel (Subgroup.comap π K))))
460 (φ (FreeGroup.of x)) := by
461 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ]
462 _ = 1 * 1 := by rw [hpure, hq, hcoord]
463 _ = 1 := by simp only [mul_one]
464 · rcases hneg with ⟨hw, hlast, hmul⟩
465 have hp : FreeGroup.prefixParent t ∈ T :=
466 prefixParent_mem_of_mem (X := X) hT ht
467 have hpure :
468 wreathLeftCoordinate ψ
469 (Quotient.mk'' (1 : F) :
470 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
471 (φ (FreeGroup.prefixParent t)) = 1 :=
472 wreathLeftCoordinate_basepoint_of_transversalWord hT ψ hψ hone
473 (FreeGroup.prefixParent t) hp
474 have hcoord :
475 wreathLeftCoordinate ψ
476 (Quotient.mk'' (φ t) :
477 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
478 (φ (FreeGroup.of x)) = 1 := by
479 exact hone ht x
480 (schreierGenerator_eq_one_of_cancels (X := X) hT ht hw hlast)
481 have hq :
482 (φ t)⁻¹ •
483 (Quotient.mk'' (1 : F) :
484 Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) =
485 Quotient.mk'' (φ t) := by
486 rw [rightCosetMulAction_inv_mk_smul (H := Subgroup.comap π K) (φ t) 1]
487 simp only [one_mul]
488 have hmulφ :
489 φ t * φ (FreeGroup.of x) = φ (FreeGroup.prefixParent t) := by
490 simpa [MonoidHom.map_mul] using congrArg φ hmul
491 have hstep :
492 wreathLeftCoordinate ψ
493 (Quotient.mk'' (1 : F) :
494 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
495 (φ (FreeGroup.prefixParent t)) =
496 wreathLeftCoordinate ψ
497 (Quotient.mk'' (1 : F) :
498 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
499 (φ t) := by
500 calc
501 wreathLeftCoordinate ψ
502 (Quotient.mk'' (1 : F) :
503 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
504 (φ (FreeGroup.prefixParent t))
505 =
506 wreathLeftCoordinate ψ
507 (Quotient.mk'' (1 : F) :
508 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
509 (φ t * φ (FreeGroup.of x)) := by
510 rw [hmulφ]
511 _ =
512 wreathLeftCoordinate ψ
513 (Quotient.mk'' (1 : F) :
514 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
515 (φ t) *
516 wreathLeftCoordinate ψ
517 ((φ t)⁻¹ •
518 (Quotient.mk'' (1 : F) :
519 Quotient (QuotientGroup.rightRel (Subgroup.comap π K))))
520 (φ (FreeGroup.of x)) := by
521 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ]
522 _ = wreathLeftCoordinate ψ
523 (Quotient.mk'' (1 : F) :
524 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
525 (φ t) * 1 := by
526 rw [hq, hcoord]
527 _ = wreathLeftCoordinate ψ
528 (Quotient.mk'' (1 : F) :
529 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
530 (φ t) := by simp only [mul_one]
531 exact hstep.symm.trans hpure
532termination_by (FreeGroup.toWord t).length
533decreasing_by
534 all_goals
535 simpa [Internal.FreeGroupWord.FreeGroup.toWord_prefixParent] using
536 Internal.FreeGroupWord.FreeGroup.toWord_length_prefixParent_lt (t := t) h1
538/--
539The transported Schreier section has trivial basepoint coordinate whenever the tree-edge
540generators do.
541-/
542theorem wreathLeftCoordinate_basepoint_of_rightSchreierSectionOfComap
543 (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
544 (hβsurj : Function.Surjective (π.comp φ))
545 (ψ : F →* PermutationalWreathProduct A
546 (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F)
547 (hψ :
548 (SemidirectProduct.rightHom :
549 PermutationalWreathProduct A
550 (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F →* F).comp ψ =
551 MonoidHom.id F)
552 (hone :
553 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
554 schreierGenerator (X := X) hT t x = 1 →
555 wreathLeftCoordinate ψ
556 (Quotient.mk'' (φ t) :
557 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
558 (φ (FreeGroup.of x)) = 1)
559 (q : Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) :
560 wreathLeftCoordinate ψ
561 (Quotient.mk'' (1 : F) :
562 Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
563 (rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT q) = 1 := by
564 let e := rightQuotientEquivOfComap π φ (π.comp φ) K rfl hβsurj
565 let tT : T := hT.1.rightQuotientEquiv (e.symm q)
566 have htT : ((tT : T) : FreeGroup X) ∈ T := tT.2
567 have hsec :
568 rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT q =
569 φ ((tT : T) : FreeGroup X) := by
570 simp only [rightSchreierSectionOfComap, rightTransversalSection, tT, e]
571 rw [hsec]
572 exact wreathLeftCoordinate_basepoint_of_transversalWord hT ψ hψ hone
573 ((tT : T) : FreeGroup X) htT
575end TransportedSectionPurity
577section FiniteQuotientLift
579open FreeGroup
581/--
582Concrete finite-quotient lift for the dense abstract Schreier subgroup comap (free group lift
583\(\iota\)) to \(H\). It is a continuity claim, checked through the topology generated by
584finite-stage projections.
585-/
586theorem exists_continuousFiniteQuotientLift_of_comap_freeGroupLift
587 (C : ProCGroups.FiniteGroupClass.{u})
593 {X : Type u} [Finite X]
594 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
595 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
596 {ι : X → F}
597 (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
598 (C := C) X F ι)
599 (H : OpenSubgroup F)
600 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
601 [Finite Q] [DiscreteTopology Q]
602 (hQ : C Q)
603 (ψ : Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) →* Q) :
604 ∃ ψBar : ↥(H : Subgroup F) →* Q,
605 Continuous ψBar ∧
606 ψBar.comp
607 ({ toFun := fun g : Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) =>
608 ⟨(FreeGroup.lift ι) g.1, g.2⟩
609 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
610 map_mul' := by
611 intro a b
612 ext
613 simp only [Subgroup.coe_mul, map_mul]} :
614 Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) →* ↥(H : Subgroup F)) = ψ := by
615 classical
616 let n : ℕ := Nat.card (F ⧸ (H : Subgroup F))
617 let P := openSubgroupIndexActionRange (G := F) H
618 (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl)
619 let ρ : F →ₜ* P :=
620 openSubgroupIndexActionRangeContinuousHom (G := F) H
621 (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl)
622 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
623 let K : Subgroup P := MulAction.stabilizer P q0
624 let βF : FreeGroup X →* F := FreeGroup.lift ι
625 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
626 let Lk : Subgroup (FreeGroup X) := Subgroup.comap β K
627 let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
628 letI : TopologicalSpace (FreeGroup X) := ⊥
629 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
630 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
631 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
632 ext g
633 constructor
634 · intro hg
635 change ρ g • q0 = q0 at hg
636 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint
637 (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl) g] at hg
638 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
639 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
640 simpa [QuotientGroup.eq] using hg
641 · intro hg
642 change ρ g • q0 = q0
643 exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem
644 (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl) hg
645 have hLk : Lk = L := by
646 ext w
647 change β w ∈ K ↔ βF w ∈ (H : Subgroup F)
648 change βF w ∈ Subgroup.comap ρ.toMonoidHom K ↔ βF w ∈ (H : Subgroup F)
649 rw [hcomap]
650 let Hc : OpenSubgroup F :=
651 { toSubgroup := Subgroup.comap ρ.toMonoidHom K
652 isOpen' := by
653 rw [hcomap]
654 exact H.isOpen' }
655 have hHc : Hc = H := by
656 ext g
657 change g ∈ Subgroup.comap ρ.toMonoidHom K ↔ g ∈ (H : Subgroup F)
658 rw [hcomap]
659 let toK : L →* Lk :=
660 { toFun := fun g => ⟨g.1, by
661 have hgL : βF g.1 ∈ (H : Subgroup F) := g.2
662 have hgComap : βF g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
663 exact (congrArg (fun S : Subgroup F => βF g.1 ∈ S) hcomap).mpr hgL
664 change ρ (βF g.1) ∈ K
665 exact hgComap⟩
666 map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
667 map_mul' := by
668 intro a b
669 ext
670 simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
671 let fromK : Lk →* L :=
672 { toFun := fun g => ⟨g.1, by
673 have hgLk : β g.1 ∈ K := g.2
674 have hgComap : βF g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
675 change ρ (βF g.1) ∈ K
676 simpa [β] using hgLk
677 have hgH : βF g.1 ∈ (H : Subgroup F) := by
678 exact (congrArg (fun S : Subgroup F => βF g.1 ∈ S) hcomap).mp hgComap
679 change βF g.1 ∈ (H : Subgroup F)
680 exact hgH⟩
681 map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
682 map_mul' := by
683 intro a b
684 ext
685 simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
686 let φOrig : L →* ↥(H : Subgroup F) :=
687 { toFun := fun g => ⟨βF g.1, g.2⟩
688 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
689 map_mul' := by
690 intro a b
691 ext
692 simp only [Subgroup.coe_mul, map_mul]}
693 let φK : Lk →* ↥(Hc : Subgroup F) :=
694 { toFun := fun g => ⟨βF g.1, by
695 have hgLk : β g.1 ∈ K := g.2
696 change ρ (βF g.1) ∈ K
697 simpa [β] using hgLk⟩
698 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
699 map_mul' := by
700 intro a b
701 ext
702 simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}
703 let toHc : ↥(H : Subgroup F) →* ↥(Hc : Subgroup F) :=
704 { toFun := fun g => ⟨g.1, by
705 have hgH : g.1 ∈ (H : Subgroup F) := g.2
706 have hgComap : g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
707 exact (congrArg (fun S : Subgroup F => g.1 ∈ S) hcomap).mpr hgH
708 change ρ g.1 ∈ K
709 exact hgComap⟩
710 map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
711 map_mul' := by
712 intro a b
713 ext
714 simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
715 let ψK : Lk →* Q := ψ.comp fromK
716 letI : Finite (OpenSubgroupRightQuotient Hc) :=
717 finite_openSubgroupRightQuotient (F := F) Hc
718 letI : Fintype (OpenSubgroupRightQuotient Hc) :=
719 fintype_openSubgroupRightQuotient (F := F) Hc
720 letI : DiscreteTopology (OpenSubgroupRightQuotient Hc) :=
721 discreteTopology_openSubgroupRightQuotient (F := F) Hc
722 letI : MulAction F (OpenSubgroupRightQuotient Hc) :=
723 rightCosetMulAction (Hc : Subgroup F)
724 letI : ContinuousSMul F (OpenSubgroupRightQuotient Hc) := by
725 refine ContinuousSMul.mk ?_
726 refine (continuous_prod_of_discrete_right).2 ?_
727 intro q
728 convert
729 (continuous_rightCosetMulAction_inv_smul_of_open
730 (G := F) (H := (Hc : Subgroup F)) Hc.isOpen' q).comp continuous_inv using 1
731 ext g
732 simp only [Function.comp_apply, inv_inv]
733 have hβFdense : DenseRange βF :=
734 denseRange_freeGroupLift_of_topologicallyGenerates
735 (F := F) (X := X) hF.generates_range
736 have hρSurj : Function.Surjective ρ := by
737 intro p
738 rcases p.down.2 with ⟨g, hg⟩
739 refine ⟨g, ?_⟩
740 apply ULift.ext
741 apply Subtype.ext
742 exact hg
743 have hβDense : DenseRange β := by
744 simpa [β, MonoidHom.comp_apply] using
745 (Function.Surjective.denseRange hρSurj).comp hβFdense ρ.continuous_toFun
746 have hβSurj : Function.Surjective β :=
747 surjective_of_denseRange (F := FreeGroup X) (P := P) hβDense
748 obtain ⟨T, hTK⟩ := exists_rightSchreierTransversal (X := X) Lk
749 let eQuot :
750 Quotient (QuotientGroup.rightRel Lk) ≃ OpenSubgroupRightQuotient Hc := by
751 simpa [Hc, OpenSubgroupRightQuotient] using
752 (rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβSurj)
753 let tRep : OpenSubgroupRightQuotient Hc → T := fun q =>
754 hTK.1.rightQuotientEquiv (eQuot.symm q)
755 have htRep_eq_of_mem {t : FreeGroup X} (ht : t ∈ T) :
756 tRep (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) = ⟨t, ht⟩ := by
757 have hmk :
758 (rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβSurj)
759 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) =
760 (Quotient.mk'' (βF t) :
761 Quotient (QuotientGroup.rightRel (Subgroup.comap ρ.toMonoidHom K))) := by
762 exact rightQuotientEquivOfComap_mk ρ.toMonoidHom βF β K rfl hβSurj t
763 have hEq :
764 eQuot.symm (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) =
765 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) := by
766 exact eQuot.symm_apply_eq.mpr
767 (by simpa [eQuot, Hc, OpenSubgroupRightQuotient] using hmk.symm)
768 apply hTK.1.rightQuotientEquiv.symm.injective
769 have hqt :
770 (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) =
771 hTK.1.rightQuotientEquiv.symm ⟨t, ht⟩ := by
772 simpa using
773 hTK.1.mk''_rightQuotientEquiv
774 (hTK.1.rightQuotientEquiv.symm ⟨t, ht⟩)
775 simpa only [tRep, Equiv.symm_apply_apply] using hEq.trans hqt
776 let ν :
777 X → PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F := fun x =>
778 ⟨fun q => ψK (schreierGenerator (X := X) hTK ((tRep q : T) : FreeGroup X) x), ι x⟩
779 have hQproC : HasOpenNormalBasisInClass C Q := by
780 exact HasOpenNormalBasisInClass.of_finite_discrete (C := C) (G := Q) hQuot hQ
781 have hWreath :
782 HasOpenNormalBasisInClass C
783 (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F) := by
784 exact
785 hasOpenNormalBasisInClass_permutationalWreathProduct
786 (C := C) hForm hIso hExt hQproC hF.hasOpenNormalBasisInClass
787 let W : Subgroup (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F) :=
788 (Subgroup.closure (Set.range ν)).topologicalClosure
789 have hWproC : HasOpenNormalBasisInClass C W := by
790 exact
791 HasOpenNormalBasisInClass.of_isClosed_subgroup
792 (C := C) (G := PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F)
793 hIso hSub hWreath W (Subgroup.isClosed_topologicalClosure _)
794 let hWclosed : IsClosed (W : Set (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc)
795 F)) := by
796 simp [W]
797 letI : CompactSpace W := hWclosed.isClosedEmbedding_subtypeVal.compactSpace
798 let νW : X → W := fun x =>
799 ⟨ν x, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩)⟩
800 have hνWconv : FamilyConvergesToOneAlongOpenSubgroups (G := W) νW := by
801 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := W) νW
802 have hνWgen :
803 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range νW) := by
804 simpa [W, νW] using topologicallyGenerates_topologicalClosure_of_range ν
805 rcases hF.existsUnique_lift hWproC νW hνWconv hνWgen with
806 ⟨ηW, hηW, _⟩
807 let η : F →* PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F :=
808 W.subtype.comp ηW
809 have hηCont : Continuous η := by
810 simpa [η] using (continuous_subtype_val.comp hηW.1)
811 have hηOnGen : ∀ x : X, η (ι x) = ν x := by
812 intro x
813 simpa [η, νW] using congrArg Subtype.val (hηW.2 x)
814 have hηRight :
815 (SemidirectProduct.rightHom :
816 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η =
817 MonoidHom.id F := by
818 rcases hF.existsUnique_lift hF.hasOpenNormalBasisInClass ι
819 hF.convergesToOneAlongOpenSubgroups hF.generates_range with
820 ⟨u, hu, huuniq⟩
821 have hu_id : MonoidHom.id F = u := by
822 exact
823 huuniq (MonoidHom.id F)
824 ⟨by simpa using (continuous_id : Continuous fun x : F => x), by intro x; rfl⟩
825 have hu_η :
826 (SemidirectProduct.rightHom :
827 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η = u := by
828 let v : F →* F :=
829 (SemidirectProduct.rightHom :
830 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η
831 have hv_on_gen : ∀ x : X, v (ι x) = ι x := by
832 intro x
833 have hx := congrArg
834 (fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F => z.right)
835 (hηOnGen x)
836 simpa [v, ν, MonoidHom.comp_apply] using hx
837 exact huuniq v ⟨continuous_permutationalWreathProduct_right.comp hηCont, hv_on_gen⟩
838 calc
839 (SemidirectProduct.rightHom :
840 PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η = u := hu_η
841 _ = MonoidHom.id F := hu_id.symm
842 have hηCoord :
843 ∀ q : OpenSubgroupRightQuotient Hc, ∀ x : X,
844 wreathLeftCoordinate η q (βF (FreeGroup.of x)) =
845 ψK (schreierGenerator (X := X) hTK ((tRep q : T) : FreeGroup X) x) := by
846 intro q x
847 simpa [wreathLeftCoordinate, βF, ν] using
848 congrArg
849 (fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F => z.left q)
850 (hηOnGen x)
851 have hηOne :
852 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
853 schreierGenerator (X := X) hTK t x = 1 →
854 wreathLeftCoordinate η
855 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
856 (βF (FreeGroup.of x)) = 1 := by
857 intro t ht x hsg
858 rw [hηCoord]
859 rw [htRep_eq_of_mem (t := t) ht]
860 simp only [hsg, map_one, ψK]
861 have htPure :
862 ∀ q : OpenSubgroupRightQuotient Hc,
863 wreathLeftCoordinate η
864 (Quotient.mk'' (1 : F) : OpenSubgroupRightQuotient Hc)
865 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK q) = 1 := by
866 intro q
867 simpa [Hc, OpenSubgroupRightQuotient, β] using
868 (wreathLeftCoordinate_basepoint_of_rightSchreierSectionOfComap
869 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) (T := T)
870 hTK hβSurj η hηRight hηOne q)
871 let ψBarK : ↥(Hc : Subgroup F) →* Q :=
872 rightQuotientBasepointProjectionHom (H := (Hc : Subgroup F)) η hηRight
873 have hψBarKCont : Continuous ψBarK := by
874 change Continuous
875 ((fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F =>
876 z.left (Quotient.mk'' (1 : F))) ∘ η ∘ Subtype.val)
877 exact
878 (continuous_permutationalWreathProduct_left_apply (A := Q)
879 (S := OpenSubgroupRightQuotient Hc) (G := F)
880 (Quotient.mk'' (1 : F) : OpenSubgroupRightQuotient Hc)).comp
881 (hηCont.comp continuous_subtype_val)
882 have hψBarKOnSchreier :
883 ∀ s : ↥(schreierGeneratorSet (X := X) hTK),
884 ψBarK (φK s) = ψK s := by
885 rintro ⟨s, hs⟩
886 rcases hs with ⟨t, ht, x, rfl, _hne⟩
887 have hmap :
888 φK (schreierGenerator (X := X) hTK t x) =
889 rightQuotientSectionCocycle
890 (H := (Hc : Subgroup F))
891 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
892 (rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβSurj hTK)
893 (βF (FreeGroup.of x))
894 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) := by
895 apply Subtype.ext
896 have hcocycle :=
897 congrArg Subtype.val
898 (map_schreierGenerator_eq_cocycle
899 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hTK hβSurj ht x).symm
900 change βF ↑(schreierGenerator (X := X) hTK t x) =
901 ↑(rightQuotientSectionCocycle
902 (H := (Hc : Subgroup F))
903 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
904 (rightSchreierSectionOfComap_spec
905 ρ.toMonoidHom βF β K rfl hβSurj hTK)
906 (βF (FreeGroup.of x))
907 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc))
908 convert hcocycle using 1
909 calc
910 ψBarK (φK (schreierGenerator (X := X) hTK t x)) =
911 ψBarK
912 (rightQuotientSectionCocycle
913 (H := (Hc : Subgroup F))
914 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
915 (rightSchreierSectionOfComap_spec
916 ρ.toMonoidHom βF β K rfl hβSurj hTK)
917 (βF (FreeGroup.of x))
918 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)) := by
919 rw [hmap]
920 _ =
921 wreathLeftCoordinate η
922 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
923 (βF (FreeGroup.of x)) := by
924 simpa [ψBarK, Hc, OpenSubgroupRightQuotient] using
925 (rightQuotientBasepointProjectionHom_apply_cocycle
926 (H := (Hc : Subgroup F))
927 (τ := rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
928 (hτ := rightSchreierSectionOfComap_spec
929 ρ.toMonoidHom βF β K rfl hβSurj hTK)
930 (ψ := η) hηRight htPure
931 (βF (FreeGroup.of x))
932 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc))
933 _ = ψK (schreierGenerator (X := X) hTK t x) := by
934 rw [hηCoord]
935 rw [htRep_eq_of_mem (t := t) ht]
936 have hψBarKFac : ψBarK.comp φK = ψK := by
937 letI : T2Space Q := inferInstance
938 have hSchGen :
940 (G := Lk) (schreierGeneratorSet (X := X) hTK : Set Lk) := by
942 rw [closure_schreierGeneratorSet_eq_top (X := X) hTK]
943 exact dense_univ
944 apply continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
945 (G := Lk) (A := Q) hSchGen
946 (continuous_of_discreteTopology : Continuous (ψBarK.comp φK))
947 (continuous_of_discreteTopology : Continuous ψK)
948 intro h hh
949 exact hψBarKOnSchreier ⟨h, hh⟩
950 let ψBar : ↥(H : Subgroup F) →* Q := ψBarK.comp toHc
951 have htoHcCont : Continuous toHc :=
952 Continuous.subtype_mk continuous_subtype_val (by
953 intro x
954 exact (congrArg (fun S : Subgroup F => x.1 ∈ S) hcomap).mpr x.2)
955 have hψBarCont : Continuous ψBar := hψBarKCont.comp htoHcCont
956 refine ⟨ψBar, hψBarCont, ?_⟩
957 apply MonoidHom.ext
958 intro l
959 have hto :
960 toHc (φOrig l) = φK (toK l) := by
961 ext
962 rfl
963 have hfrom :
964 fromK (toK l) = l := by
965 ext
966 rfl
967 have hfacK := congrArg (fun f : Lk →* Q => f (toK l)) hψBarKFac
968 calc
969 ψBar (φOrig l) = ψBarK (φK (toK l)) := by
970 simpa [ψBar, MonoidHom.comp_apply] using congrArg ψBarK hto
971 _ = ψK (toK l) := hfacK
972 _ = ψ (fromK (toK l)) := rfl
973 _ = ψ l := by rw [hfrom]
975end FiniteQuotientLift
977section ExactPointedRightSchreierGeneration
979open ProCGroups.ProC
981/--
982An open subgroup of a pointed free pro-\(C\) group admits a compact right Schreier generator
983family whose image, pointed at the distinguished generator 1, is itself a pointed free pro-\(C\)
984basis of the open subgroup.
985-/
986theorem exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup
987 {C : ProCGroups.FiniteGroupClass.{u}}
992 {X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
993 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
994 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
995 {ι : X → F}
996 (hF : IsEpimorphicallyPointedFreeProCGroupOn
997 (C := C) X x0 F ι)
998 (H : OpenSubgroup F) :
999 ∃ κ : OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F),
1000 Continuous κ ∧
1001 (∀ q : OpenSubgroupRightQuotient H, κ (q, x0) = 1) ∧
1002 κ (openSubgroupRightCoset H (1 : F), x0) = 1 ∧
1003 IsCompact (Set.range κ) ∧
1004 IsClosed (Set.range κ) ∧
1005 IsEpimorphicallyPointedFreeProCGroupOn
1006 (C := C)
1007 (Set.range κ)
1008 ⟨κ (openSubgroupRightCoset H (1 : F), x0),
1009 ⟨(openSubgroupRightCoset H (1 : F), x0), rfl⟩⟩
1010 ↥(H : Subgroup F) Subtype.val := by
1011 classical
1012 let n : ℕ := Nat.card (F ⧸ (H : Subgroup F))
1013 let hn : Nat.card (F ⧸ (H : Subgroup F)) = n := rfl
1014 let P := openSubgroupIndexActionRange (G := F) H hn
1015 let ρ : F →ₜ* P := openSubgroupIndexActionRangeContinuousHom (G := F) H hn
1016 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
1017 let K : Subgroup P := MulAction.stabilizer P q0
1018 let βF : FreeGroup X →* F := FreeGroup.lift ι
1019 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
1020 letI : TopologicalSpace (FreeGroup X) := ⊥
1021 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
1022 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
1023 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
1024 ext g
1025 constructor
1026 · intro hg
1027 change ρ g • q0 = q0 at hg
1028 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := F) H hn g] at hg
1029 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
1030 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
1031 simpa [QuotientGroup.eq] using hg
1032 · intro hg
1033 change ρ g • q0 = q0
1034 exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem (G := F) H hn hg
1035 have hβFdense : DenseRange βF :=
1036 denseRange_freeGroupLift_of_topologicallyGenerates (F := F) (X := X) hF.generates_range
1037 have hρsurj : Function.Surjective ρ := by
1038 intro p
1039 rcases p.down.2 with ⟨g, hg⟩
1040 refine ⟨g, ?_⟩
1041 apply ULift.ext
1042 apply Subtype.ext
1043 exact hg
1044 have hβdense : DenseRange β := by
1045 simpa [β, MonoidHom.comp_apply] using
1046 (Function.Surjective.denseRange hρsurj).comp hβFdense ρ.continuous_toFun
1047 have hβsurj : Function.Surjective β :=
1048 surjective_of_denseRange (F := FreeGroup X) (P := P) hβdense
1049 obtain ⟨T, hT⟩ := exists_rightSchreierTransversal (X := X) (Subgroup.comap β K)
1050 have hβFcomapDense :
1051 DenseRange
1052 ({ toFun := fun g : Subgroup.comap β K => ⟨βF g.1, g.2⟩
1053 map_one' := by
1054 apply Subtype.ext
1055 exact βF.map_one
1056 map_mul' := by
1057 intro a b
1058 apply Subtype.ext
1059 exact βF.map_mul a b} :
1060 Subgroup.comap β K →* ↥(Subgroup.comap ρ.toMonoidHom K)) := by
1061 have hρKopen : IsOpen ((Subgroup.comap ρ.toMonoidHom K : Subgroup F) : Set F) := by
1062 rw [hcomap]
1063 exact H.isOpen'
1064 exact denseRange_comapMap_of_openSubgroup
1065 (φ := βF) hβFdense (U := Subgroup.comap ρ.toMonoidHom K) hρKopen
1066 let Hc : OpenSubgroup F :=
1067 { toSubgroup := Subgroup.comap ρ.toMonoidHom K
1068 isOpen' := by
1069 rw [hcomap]
1070 exact H.isOpen' }
1071 letI : CompactSpace ↥(Hc : Subgroup F) :=
1072 compactSpace_openSubgroupSubtype Hc
1073 have hHc : Hc = H := by
1074 ext g
1075 change g ∈ Subgroup.comap ρ.toMonoidHom K ↔ g ∈ (H : Subgroup F)
1076 rw [hcomap]
1077 have hκgenPre :
1078 let τ := rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT
1079 let hτ := rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT
1080 let κ :
1081 Quotient (QuotientGroup.rightRel (Subgroup.comap ρ.toMonoidHom K)) × X →
1082 ↥(Subgroup.comap ρ.toMonoidHom K) :=
1083 fun p =>
1084 rightQuotientSectionCocycle
1085 (H := Subgroup.comap ρ.toMonoidHom K) τ hτ (βF (FreeGroup.of p.2)) p.1
1087 (G := ↥(Subgroup.comap ρ.toMonoidHom K)) (Set.range κ) := by
1088 exact topologicallyGenerates_range_transportedCocycle
1089 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hT hβsurj hβFcomapDense
1090 let GoalProp : OpenSubgroup F → Prop := fun J =>
1091 ∃ κ : OpenSubgroupRightQuotient J × X → ↥(J : Subgroup F),
1092 Continuous κ ∧
1093 (∀ q : OpenSubgroupRightQuotient J, κ (q, x0) = 1) ∧
1094 κ (openSubgroupRightCoset J (1 : F), x0) = 1 ∧
1095 IsCompact (Set.range κ) ∧
1096 IsClosed (Set.range κ) ∧
1097 IsEpimorphicallyPointedFreeProCGroupOn
1098 (C := C)
1099 (Set.range κ)
1100 ⟨κ (openSubgroupRightCoset J (1 : F), x0),
1101 ⟨(openSubgroupRightCoset J (1 : F), x0), rfl⟩⟩
1102 ↥(J : Subgroup F) Subtype.val
1103 have hMain : GoalProp Hc := by
1104 letI : Finite (OpenSubgroupRightQuotient Hc) :=
1105 finite_openSubgroupRightQuotient (F := F) Hc
1106 letI : Fintype (OpenSubgroupRightQuotient Hc) :=
1107 fintype_openSubgroupRightQuotient (F := F) Hc
1108 letI : DiscreteTopology (OpenSubgroupRightQuotient Hc) :=
1109 discreteTopology_openSubgroupRightQuotient (F := F) Hc
1110 letI : MulAction F (OpenSubgroupRightQuotient Hc) :=
1111 rightCosetMulAction (Hc : Subgroup F)
1112 letI : ContinuousSMul F (OpenSubgroupRightQuotient Hc) := by
1113 refine ContinuousSMul.mk ?_
1114 refine (continuous_prod_of_discrete_right).2 ?_
1115 intro q
1116 convert
1117 (continuous_rightCosetMulAction_inv_smul_of_open
1118 (G := F) (H := (Hc : Subgroup F)) Hc.isOpen' q).comp continuous_inv using 1
1119 ext g
1120 simp only [Function.comp_apply, inv_inv]
1121 let q1 : OpenSubgroupRightQuotient Hc := openSubgroupRightCoset Hc (1 : F)
1122 let τ : OpenSubgroupRightQuotient Hc → F := by
1123 simpa [Hc, OpenSubgroupRightQuotient] using
1124 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT)
1125 have hτ : ∀ q : OpenSubgroupRightQuotient Hc, Quotient.mk'' (τ q) = q := by
1126 intro q
1127 change
1128 Quotient.mk'' ((rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT) q) = q
1129 exact rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT q
1130 let κ : OpenSubgroupRightQuotient Hc × X → ↥(Hc : Subgroup F) :=
1131 fun p =>
1132 rightSchreierGenerator
1133 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2
1134 have hκgen :
1135 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Hc : Subgroup F)) (Set.range κ) := by
1136 simpa [κ, rightSchreierGenerator, τ, Hc, OpenSubgroupRightQuotient, βF] using hκgenPre
1137 have hτcont : Continuous τ := continuous_of_discreteTopology
1138 have hκcont : Continuous κ := by
1139 exact continuous_rightSchreierGenerator
1140 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) hτcont hF.continuous_ι
1141 have hκ1 : κ (q1, x0) = 1 := by
1142 simpa [κ, rightSchreierGenerator, βF] using
1143 (rightSchreierGenerator_eq_one
1144 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q1) (x := x0) hF.map_base)
1145 have hκbase : ∀ q : OpenSubgroupRightQuotient Hc, κ (q, x0) = 1 := by
1146 intro q
1147 simpa [κ, rightSchreierGenerator, βF] using
1148 (rightSchreierGenerator_eq_one
1149 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0) hF.map_base)
1150 refine ⟨κ, hκcont, hκbase, hκ1, isCompact_range hκcont, (isCompact_range hκcont).isClosed, ?_⟩
1151 refine ⟨?_, continuous_subtype_val, ?_, ?_, ?_⟩
1152 · exact
1153 HasOpenNormalBasisInClass.of_isClosed_subgroup
1154 (C := C) (G := F) hIso hSub hF.hasOpenNormalBasisInClass (Hc : Subgroup F)
1155 (Subgroup.isClosed_of_isOpen (Hc : Subgroup F) Hc.isOpen')
1156 · simpa [hκ1]
1157 · have hrange :
1158 Set.range (Subtype.val : Set.range κ → ↥(Hc : Subgroup F)) = Set.range κ := by
1159 ext h
1160 constructor
1161 · rintro ⟨x, rfl⟩
1162 exact x.2
1163 · intro hh
1164 exact ⟨⟨h, hh⟩, rfl⟩
1165 simpa [hrange] using hκgen
1166 · intro B _ _ _ _ _ _ hB φB hφB hφB0 hgenB
1167 let ξ : X → PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1168 fun x => ⟨fun q => φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩, ι x⟩
1169 have hξcont : Continuous ξ := by
1170 refine continuous_induced_rng.2 ?_
1171 change Continuous fun x : X => ((ξ x).left, (ξ x).right)
1172 have hleft : Continuous fun x : X => (ξ x).left := by
1173 refine continuous_pi ?_
1174 intro q
1175 have hqcont : Continuous fun x : X => κ (q, x) := by
1176 change Continuous (κ ∘ fun x : X => (q, x))
1177 exact hκcont.comp (continuous_const.prodMk continuous_id)
1178 have hsub :
1179 Continuous fun x : X => (⟨κ (q, x), ⟨(q, x), rfl⟩⟩ : Set.range κ) :=
1180 Continuous.subtype_mk hqcont (by
1181 intro x
1182 exact ⟨(q, x), rfl⟩)
1183 change Continuous (φB ∘ fun x : X =>
1184 (⟨κ (q, x), ⟨(q, x), rfl⟩⟩ : Set.range κ))
1185 exact hφB.comp hsub
1186 have hright : Continuous fun x : X => (ξ x).right := by
1187 simpa [ξ] using hF.continuous_ι
1188 exact hleft.prodMk hright
1189 have hξ0 : ξ x0 = 1 := by
1190 apply SemidirectProduct.ext
1191 · funext q
1192 have hq1 : κ (q, x0) = 1 := by
1193 simpa [κ, rightSchreierGenerator, βF] using
1194 (rightSchreierGenerator_eq_one
1195 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0)
1196 hF.map_base)
1197 have hsrc :
1198 (⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ : Set.range κ) =
1199 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1200 apply Subtype.ext
1201 exact hq1.trans hκ1.symm
1202 calc
1203 (ξ x0).left q = φB ⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ := rfl
1204 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1205 _ = 1 := hφB0
1206 · simp only [hF.map_base, SemidirectProduct.one_right, ξ]
1207 let W : Subgroup (PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F) :=
1208 (Subgroup.closure (Set.range ξ)).topologicalClosure
1209 have hWreath :
1210 HasOpenNormalBasisInClass C (PermutationalWreathProduct B (OpenSubgroupRightQuotient
1211 Hc) F) := by
1212 exact
1213 hasOpenNormalBasisInClass_permutationalWreathProduct
1214 (C := C) hForm hIso hExt hB hF.hasOpenNormalBasisInClass
1215 have hWproC : HasOpenNormalBasisInClass C W := by
1216 exact
1217 HasOpenNormalBasisInClass.of_isClosed_subgroup
1218 (C := C) (G := PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F)
1219 hIso hSub hWreath W (Subgroup.isClosed_topologicalClosure _)
1220 let hWclosed : IsClosed (W : Set (PermutationalWreathProduct B (OpenSubgroupRightQuotient
1221 Hc) F)) := by
1222 simp [W]
1223 letI : CompactSpace W := hWclosed.isClosedEmbedding_subtypeVal.compactSpace
1224 let ξW : X → W := fun x =>
1225 ⟨ξ x, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩)⟩
1226 have hξWcont : Continuous ξW :=
1227 Continuous.subtype_mk hξcont (by
1228 intro x
1229 exact Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩))
1230 have hξW0 : ξW x0 = 1 := by
1231 apply Subtype.ext
1232 exact hξ0
1233 have hξWgen :
1234 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range ξW) := by
1235 simpa [W, ξW] using
1236 topologicallyGenerates_topologicalClosure_of_range (ξ := ξ)
1237 rcases hF.existsUnique_lift hWproC ξW hξWcont hξW0 hξWgen with
1238 ⟨ηW, hηW, _⟩
1239 let η : F →* PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1240 W.subtype.comp ηW
1241 have hηcont : Continuous η := by
1242 simpa [η] using (continuous_subtype_val.comp hηW.1)
1243 have hηgen : ∀ x : X, η (ι x) = ξ x := by
1244 intro x
1245 simpa [η, ξW] using congrArg Subtype.val (hηW.2 x)
1246 have hηright :
1247 (SemidirectProduct.rightHom :
1248 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1249 MonoidHom.id F := by
1250 rcases
1251 hF.existsUnique_lift hF.hasOpenNormalBasisInClass ι hF.continuous_ι hF.map_base
1252 hF.generates_range with
1253 ⟨u, hu, huuniq⟩
1254 have hu_id : MonoidHom.id F = u := by
1255 exact
1256 huuniq (MonoidHom.id F)
1257 ⟨by simpa using (continuous_id : Continuous fun x : F => x), by intro x; rfl⟩
1258 have hu_η :
1259 (SemidirectProduct.rightHom :
1260 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1261 u := by
1262 let v : F →* F :=
1263 (SemidirectProduct.rightHom :
1264 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η
1265 have hη_on_gen :
1266 ∀ x : X, v (ι x) = ι x := by
1267 intro x
1268 have hx := congrArg
1269 (fun z : PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F => z.right)
1270 (hηgen x)
1271 simpa [v, MonoidHom.comp_apply, ξ] using hx
1272 have hvu : v = u := by
1273 exact huuniq v ⟨continuous_permutationalWreathProduct_right.comp hηcont, hη_on_gen⟩
1274 simpa [v] using hvu
1275 calc
1276 (SemidirectProduct.rightHom :
1277 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η = u :=
1278 hu_η
1279 _ = MonoidHom.id F := hu_id.symm
1280 have hηcoord :
1281 ∀ q : OpenSubgroupRightQuotient Hc, ∀ x : X,
1282 wreathLeftCoordinate η q (ι x) =
1283 φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩ := by
1284 intro q x
1285 change (η (ι x)).left q = _
1286 rw [hηgen]
1287 have hηone :
1288 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
1289 schreierGenerator (X := X) hT t x = 1 →
1290 wreathLeftCoordinate η
1291 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1292 (βF (FreeGroup.of x)) = 1 := by
1293 intro t ht x hsg
1294 have hmap :
1295 κ (Quotient.mk'' (βF t), x) = 1 := by
1296 apply Subtype.ext
1297 have hcocycle :=
1298 congrArg Subtype.val
1299 (map_schreierGenerator_eq_cocycle
1300 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hT hβsurj ht x)
1301 change (↑(κ (Quotient.mk'' (βF t), x)) : F) = 1
1302 calc
1303 (↑(κ (Quotient.mk'' (βF t), x)) : F) =
1304 βF ↑(schreierGenerator (X := X) hT t x) := by
1305 simpa [κ, rightSchreierGenerator, τ, Hc,
1306 OpenSubgroupRightQuotient, β, βF] using hcocycle
1307 _ = 1 := by rw [hsg]; exact βF.map_one
1308 have hsrc :
1309 (⟨κ (Quotient.mk'' (βF t), x), ⟨(Quotient.mk'' (βF t), x), rfl⟩⟩ : Set.range κ) =
1310 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1311 apply Subtype.ext
1312 exact hmap.trans hκ1.symm
1313 calc
1314 wreathLeftCoordinate η
1315 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1316 (βF (FreeGroup.of x))
1318 wreathLeftCoordinate η
1319 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) (ι x) := by
1320 simp only [FreeGroup.lift_apply_of, βF]
1321 _ = φB ⟨κ (Quotient.mk'' (βF t), x), ⟨(Quotient.mk'' (βF t), x), rfl⟩⟩ :=
1322 hηcoord _ _
1323 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1324 _ = 1 := hφB0
1325 have hτpure :
1326 ∀ q : OpenSubgroupRightQuotient Hc,
1327 wreathLeftCoordinate η q1 (τ q) = 1 := by
1328 intro q
1329 simpa [q1, τ, Hc, OpenSubgroupRightQuotient, openSubgroupRightCoset,
1330 rightCoset, β, βF] using
1331 (wreathLeftCoordinate_basepoint_of_rightSchreierSectionOfComap
1332 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hT hβsurj η hηright
1333 (hone := hηone) q)
1334 let g : ↥(Hc : Subgroup F) →* B :=
1335 rightQuotientBasepointProjectionHom (H := (Hc : Subgroup F)) η hηright
1336 have hgcont : Continuous g := by
1337 change Continuous
1338 ((fun z : PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F =>
1339 z.left q1) ∘ η ∘ Subtype.val)
1340 exact
1341 (continuous_permutationalWreathProduct_left_apply (A := B)
1342 (S := OpenSubgroupRightQuotient Hc) (G := F) q1).comp
1343 (hηcont.comp continuous_subtype_val)
1344 have hgfac : ∀ y : Set.range κ, g y.1 = φB y := by
1345 rintro ⟨y, ⟨⟨q, x⟩, hy⟩⟩
1346 subst y
1347 change g (κ (q, x)) = φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩
1348 calc
1349 g (κ (q, x)) = wreathLeftCoordinate η q (βF (FreeGroup.of x)) := by
1350 simpa [g, κ, τ, βF] using
1351 (rightQuotientBasepointProjectionHom_rightSchreierGenerator
1352 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) η hηright hτpure q x)
1353 _ = wreathLeftCoordinate η q (ι x) := by simp only [FreeGroup.lift_apply_of, βF]
1354 _ = φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩ := hηcoord q x
1355 refine ⟨g, ⟨hgcont, hgfac⟩, ?_⟩
1356 intro g' hg'
1357 symm
1358 apply continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
1359 (G := ↥(Hc : Subgroup F)) (A := B) hκgen hgcont hg'.1
1360 intro h hh
1361 exact (hgfac ⟨h, hh⟩).trans (hg'.2 ⟨h, hh⟩).symm
1362 exact cast (congrArg GoalProp hHc) hMain
1364end ExactPointedRightSchreierGeneration
1368/--
1369There exists a pointed free right-Schreier generator family for the open subgroup under the
1370minimal generator-power hypothesis.
1372theorem exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup_of_minimalGeneratorPower
1373 {C : ProCGroups.FiniteGroupClass.{u}}
1378 {X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
1379 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
1380 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
1381 {ι : X → F}
1382 (hF : IsEpimorphicallyPointedFreeProCGroupOn
1383 (C := C) X x0 F ι)
1384 (H : OpenSubgroup F) (x : X) {N : ℕ}
1385 (hN : 0 < N)
1386 (hpow : (ι x) ^ N ∈ (H : Subgroup F))
1387 (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
1388 ∃ κ : OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F),
1389 Continuous κ ∧
1390 (∀ q : OpenSubgroupRightQuotient H, κ (q, x0) = 1) ∧
1391 κ (openSubgroupRightCoset H (1 : F), x0) = 1 ∧
1392 (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈ Set.range κ ∧
1393 IsCompact (Set.range κ) ∧
1394 IsClosed (Set.range κ) ∧
1395 IsEpimorphicallyPointedFreeProCGroupOn
1396 (C := C)
1397 (Set.range κ)
1398 ⟨κ (openSubgroupRightCoset H (1 : F), x0),
1399 ⟨(openSubgroupRightCoset H (1 : F), x0), rfl⟩⟩
1400 ↥(H : Subgroup F) Subtype.val := by
1401 classical
1402 let n : ℕ := Nat.card (F ⧸ (H : Subgroup F))
1403 let hn : Nat.card (F ⧸ (H : Subgroup F)) = n := rfl
1404 let P := openSubgroupIndexActionRange (G := F) H hn
1405 let ρ : F →ₜ* P := openSubgroupIndexActionRangeContinuousHom (G := F) H hn
1406 let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
1407 let K : Subgroup P := MulAction.stabilizer P q0
1408 let βF : FreeGroup X →* F := FreeGroup.lift ι
1409 let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
1410 let βc : Subgroup.comap β K →* ↥(Subgroup.comap ρ.toMonoidHom K) :=
1411 { toFun := fun g => ⟨βF g.1, g.2⟩
1412 map_one' := by
1413 apply Subtype.ext
1414 exact βF.map_one
1415 map_mul' := by
1416 intro a b
1417 apply Subtype.ext
1418 exact βF.map_mul a b}
1419 letI : TopologicalSpace (FreeGroup X) := ⊥
1420 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
1421 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
1422 have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
1423 ext g
1424 constructor
1425 · intro hg
1426 change ρ g • q0 = q0 at hg
1427 rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := F) H hn g] at hg
1428 change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
1429 QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
1430 simpa [QuotientGroup.eq] using hg
1431 · intro hg
1432 change ρ g • q0 = q0
1433 exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem (G := F) H hn hg
1434 have hβFdense : DenseRange βF :=
1435 denseRange_freeGroupLift_of_topologicallyGenerates (F := F) (X := X) hF.generates_range
1436 have hρsurj : Function.Surjective ρ := by
1437 intro p
1438 rcases p.down.2 with ⟨g, hg⟩
1439 refine ⟨g, ?_⟩
1440 apply ULift.ext
1441 apply Subtype.ext
1442 exact hg
1443 have hβdense : DenseRange β := by
1444 simpa [β, MonoidHom.comp_apply] using
1445 (Function.Surjective.denseRange hρsurj).comp hβFdense ρ.continuous_toFun
1446 have hβsurj : Function.Surjective β :=
1447 surjective_of_denseRange (F := FreeGroup X) (P := P) hβdense
1448 have hpowβ : (FreeGroup.of x) ^ N ∈ Subgroup.comap β K := by
1449 change βF ((FreeGroup.of x) ^ N) ∈ Subgroup.comap ρ.toMonoidHom K
1450 rw [hcomap]
1451 simpa [βF, MonoidHom.map_pow] using hpow
1452 have hminβ :
1453 ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ Subgroup.comap β K := by
1454 intro m hm0 hmN hm
1455 apply hmin m hm0 hmN
1456 change βF ((FreeGroup.of x) ^ m) ∈ Subgroup.comap ρ.toMonoidHom K at hm
1457 rw [hcomap] at hm
1458 simpa [βF, MonoidHom.map_pow] using hm
1459 obtain ⟨T, hT, hpred, hsg⟩ :=
1460 exists_rightSchreierTransversal_of_minimalGeneratorPower
1461 (X := X) (L := Subgroup.comap β K) x hN hpowβ hminβ
1462 have hβFcomapDense : DenseRange βc := by
1463 have hρKopen : IsOpen ((Subgroup.comap ρ.toMonoidHom K : Subgroup F) : Set F) := by
1464 rw [hcomap]
1465 exact H.isOpen'
1466 change DenseRange (fun g : Subgroup.comap β K =>
1467 (⟨βF g.1, g.2⟩ : ↥(Subgroup.comap ρ.toMonoidHom K)))
1468 have hdense := denseRange_comapMap_of_openSubgroup
1469 (φ := βF) hβFdense (U := Subgroup.comap ρ.toMonoidHom K) hρKopen
1470 change DenseRange (fun g : Subgroup.comap βF (Subgroup.comap ρ.toMonoidHom K) =>
1471 (⟨βF g.1, g.2⟩ : ↥(Subgroup.comap ρ.toMonoidHom K))) at hdense
1472 simpa [β, Subgroup.comap_comap] using hdense
1473 let Hc : OpenSubgroup F :=
1474 { toSubgroup := Subgroup.comap ρ.toMonoidHom K
1475 isOpen' := by
1476 rw [hcomap]
1477 exact H.isOpen' }
1478 letI : CompactSpace ↥(Hc : Subgroup F) :=
1479 compactSpace_openSubgroupSubtype Hc
1480 have hHc : Hc = H := by
1481 ext g
1482 change g ∈ Subgroup.comap ρ.toMonoidHom K ↔ g ∈ (H : Subgroup F)
1483 rw [hcomap]
1484 have hκgenPre :
1485 let τ := rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT
1486 let hτ := rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT
1487 let κ :
1488 Quotient (QuotientGroup.rightRel (Subgroup.comap ρ.toMonoidHom K)) × X →
1489 ↥(Subgroup.comap ρ.toMonoidHom K) :=
1490 fun p =>
1491 rightQuotientSectionCocycle
1492 (H := Subgroup.comap ρ.toMonoidHom K) τ hτ (βF (FreeGroup.of p.2)) p.1
1494 (G := ↥(Subgroup.comap ρ.toMonoidHom K)) (Set.range κ) := by
1495 exact topologicallyGenerates_range_transportedCocycle
1496 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hT hβsurj hβFcomapDense
1497 let GoalProp : OpenSubgroup F → Prop := fun J =>
1498 ∃ κ : OpenSubgroupRightQuotient J × X → ↥(J : Subgroup F),
1499 Continuous κ ∧
1500 (∀ q : OpenSubgroupRightQuotient J, κ (q, x0) = 1) ∧
1501 κ (openSubgroupRightCoset J (1 : F), x0) = 1 ∧
1502 (∃ hpowJ : (ι x) ^ N ∈ (J : Subgroup F),
1503 (⟨(ι x) ^ N, hpowJ⟩ : ↥(J : Subgroup F)) ∈ Set.range κ) ∧
1504 IsCompact (Set.range κ) ∧
1505 IsClosed (Set.range κ) ∧
1506 IsEpimorphicallyPointedFreeProCGroupOn
1507 (C := C)
1508 (Set.range κ)
1509 ⟨κ (openSubgroupRightCoset J (1 : F), x0),
1510 ⟨(openSubgroupRightCoset J (1 : F), x0), rfl⟩⟩
1511 ↥(J : Subgroup F) Subtype.val
1512 have hMain : GoalProp Hc := by
1513 letI : Finite (OpenSubgroupRightQuotient Hc) :=
1514 finite_openSubgroupRightQuotient (F := F) Hc
1515 letI : Fintype (OpenSubgroupRightQuotient Hc) :=
1516 fintype_openSubgroupRightQuotient (F := F) Hc
1517 letI : DiscreteTopology (OpenSubgroupRightQuotient Hc) :=
1518 discreteTopology_openSubgroupRightQuotient (F := F) Hc
1519 letI : MulAction F (OpenSubgroupRightQuotient Hc) :=
1520 rightCosetMulAction (Hc : Subgroup F)
1521 letI : ContinuousSMul F (OpenSubgroupRightQuotient Hc) := by
1522 refine ContinuousSMul.mk ?_
1523 refine (continuous_prod_of_discrete_right).2 ?_
1524 intro q
1525 convert
1526 (continuous_rightCosetMulAction_inv_smul_of_open
1527 (G := F) (H := (Hc : Subgroup F)) Hc.isOpen' q).comp continuous_inv using 1
1528 ext g
1529 simp only [Function.comp_apply, inv_inv]
1530 let q1 : OpenSubgroupRightQuotient Hc := openSubgroupRightCoset Hc (1 : F)
1531 let τ : OpenSubgroupRightQuotient Hc → F := by
1532 simpa [Hc, OpenSubgroupRightQuotient] using
1533 (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT)
1534 have hτ : ∀ q : OpenSubgroupRightQuotient Hc, Quotient.mk'' (τ q) = q := by
1535 intro q
1536 change
1537 Quotient.mk'' ((rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβsurj hT) q) = q
1538 exact rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβsurj hT q
1539 let κ : OpenSubgroupRightQuotient Hc × X → ↥(Hc : Subgroup F) :=
1540 fun p =>
1541 rightSchreierGenerator
1542 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2
1543 have hκgen :
1544 ProCGroups.Generation.TopologicallyGenerates (G := ↥(Hc : Subgroup F)) (Set.range κ) := by
1545 simpa [κ, rightSchreierGenerator, τ, Hc, OpenSubgroupRightQuotient, βF] using hκgenPre
1546 have hτcont : Continuous τ := continuous_of_discreteTopology
1547 have hκcont : Continuous κ := by
1548 exact continuous_rightSchreierGenerator
1549 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) hτcont hF.continuous_ι
1550 have hκ1 : κ (q1, x0) = 1 := by
1551 simpa [κ, rightSchreierGenerator, βF] using
1552 (rightSchreierGenerator_eq_one
1553 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q1) (x := x0) hF.map_base)
1554 have hκbase : ∀ q : OpenSubgroupRightQuotient Hc, κ (q, x0) = 1 := by
1555 intro q
1556 simpa [κ, rightSchreierGenerator, βF] using
1557 (rightSchreierGenerator_eq_one
1558 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0) hF.map_base)
1559 have hpowHc : (ι x) ^ N ∈ (Hc : Subgroup F) := by
1560 change (ι x) ^ N ∈ Subgroup.comap ρ.toMonoidHom K
1561 rw [hcomap]
1562 exact hpow
1563 have hxNrange : (⟨(ι x) ^ N, hpowHc⟩ : ↥(Hc : Subgroup F)) ∈ Set.range κ := by
1564 have hmap :
1565 κ ((Quotient.mk'' (βF ((FreeGroup.of x) ^ (N - 1))) : OpenSubgroupRightQuotient Hc), x) =
1566 βc (schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x) := by
1567 apply Subtype.ext
1568 have hcocycle :=
1569 congrArg Subtype.val
1570 (map_schreierGenerator_eq_cocycle
1571 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hT hβsurj hpred x)
1572 change (↑(κ
1573 ((Quotient.mk'' (βF ((FreeGroup.of x) ^ (N - 1))) :
1574 OpenSubgroupRightQuotient Hc), x)) : F) =
1575 βF ↑(schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x)
1576 simpa [βc, κ, rightSchreierGenerator, τ, Hc,
1577 OpenSubgroupRightQuotient, β, βF] using hcocycle
1578 have hβc_pow : βc ⟨(FreeGroup.of x) ^ N, hpowβ⟩ = ⟨(ι x) ^ N, hpowHc⟩ := by
1579 apply Subtype.ext
1580 change βF (FreeGroup.of x ^ N) = ι x ^ N
1581 rw [map_pow]
1582 simp only [FreeGroup.lift_apply_of, βF]
1583 refine
1584 ⟨((Quotient.mk'' (βF ((FreeGroup.of x) ^ (N - 1))) :
1585 OpenSubgroupRightQuotient Hc), x), ?_⟩
1586 calc
1587 κ ((Quotient.mk'' (βF ((FreeGroup.of x) ^ (N - 1))) : OpenSubgroupRightQuotient Hc), x) =
1588 βc (schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x) := hmap
1589 _ = βc ⟨(FreeGroup.of x) ^ N, hpowβ⟩ := by rw [hsg]
1590 _ = ⟨(ι x) ^ N, hpowHc⟩ := hβc_pow
1591 refine ⟨κ, hκcont, hκbase, hκ1, ⟨hpowHc, hxNrange⟩,
1592 isCompact_range hκcont, (isCompact_range hκcont).isClosed, ?_⟩
1593 refine ⟨?_, continuous_subtype_val, ?_, ?_, ?_⟩
1594 · exact
1595 HasOpenNormalBasisInClass.of_isClosed_subgroup
1596 (C := C) (G := F) hIso hSub hF.hasOpenNormalBasisInClass (Hc : Subgroup F)
1597 (Subgroup.isClosed_of_isOpen (Hc : Subgroup F) Hc.isOpen')
1598 · simpa [hκ1]
1599 · have hrange :
1600 Set.range (Subtype.val : Set.range κ → ↥(Hc : Subgroup F)) = Set.range κ := by
1601 ext h
1602 constructor
1603 · rintro ⟨x, rfl⟩
1604 exact x.2
1605 · intro hh
1606 exact ⟨⟨h, hh⟩, rfl⟩
1607 simpa [hrange] using hκgen
1608 · intro B _ _ _ _ _ _ hB φB hφB hφB0 hgenB
1609 let ξ : X → PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1610 fun x => ⟨fun q => φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩, ι x⟩
1611 have hξcont : Continuous ξ := by
1612 refine continuous_induced_rng.2 ?_
1613 change Continuous fun x : X => ((ξ x).left, (ξ x).right)
1614 have hleft : Continuous fun x : X => (ξ x).left := by
1615 refine continuous_pi ?_
1616 intro q
1617 have hqcont : Continuous fun x : X => κ (q, x) := by
1618 change Continuous (κ ∘ fun x : X => (q, x))
1619 exact hκcont.comp (continuous_const.prodMk continuous_id)
1620 have hsub :
1621 Continuous fun x : X => (⟨κ (q, x), ⟨(q, x), rfl⟩⟩ : Set.range κ) :=
1622 Continuous.subtype_mk hqcont (by
1623 intro x
1624 exact ⟨(q, x), rfl⟩)
1625 change Continuous (φB ∘ fun x : X =>
1626 (⟨κ (q, x), ⟨(q, x), rfl⟩⟩ : Set.range κ))
1627 exact hφB.comp hsub
1628 have hright : Continuous fun x : X => (ξ x).right := by
1629 simpa [ξ] using hF.continuous_ι
1630 exact hleft.prodMk hright
1631 have hξ0 : ξ x0 = 1 := by
1632 apply SemidirectProduct.ext
1633 · funext q
1634 have hq1 : κ (q, x0) = 1 := by
1635 simpa [κ, rightSchreierGenerator, βF] using
1636 (rightSchreierGenerator_eq_one
1637 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) (q := q) (x := x0)
1638 hF.map_base)
1639 have hsrc :
1640 (⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ : Set.range κ) =
1641 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1642 apply Subtype.ext
1643 exact hq1.trans hκ1.symm
1644 calc
1645 (ξ x0).left q = φB ⟨κ (q, x0), ⟨(q, x0), rfl⟩⟩ := rfl
1646 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1647 _ = 1 := hφB0
1648 · simp only [hF.map_base, SemidirectProduct.one_right, ξ]
1649 let W : Subgroup (PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F) :=
1650 (Subgroup.closure (Set.range ξ)).topologicalClosure
1651 have hWreath :
1652 HasOpenNormalBasisInClass C (PermutationalWreathProduct B (OpenSubgroupRightQuotient
1653 Hc) F) := by
1654 exact
1655 hasOpenNormalBasisInClass_permutationalWreathProduct
1656 (C := C) hForm hIso hExt hB hF.hasOpenNormalBasisInClass
1657 have hWproC : HasOpenNormalBasisInClass C W := by
1658 exact
1659 HasOpenNormalBasisInClass.of_isClosed_subgroup
1660 (C := C) (G := PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F)
1661 hIso hSub hWreath W (Subgroup.isClosed_topologicalClosure _)
1662 let hWclosed : IsClosed (W : Set (PermutationalWreathProduct B (OpenSubgroupRightQuotient
1663 Hc) F)) := by
1664 simp [W]
1665 letI : CompactSpace W := hWclosed.isClosedEmbedding_subtypeVal.compactSpace
1666 let ξW : X → W := fun x =>
1667 ⟨ξ x, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩)⟩
1668 have hξWcont : Continuous ξW :=
1669 Continuous.subtype_mk hξcont (by
1670 intro x
1671 exact Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩))
1672 have hξW0 : ξW x0 = 1 := by
1673 apply Subtype.ext
1674 exact hξ0
1675 have hξWgen :
1676 ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range ξW) := by
1677 simpa [W, ξW] using
1678 topologicallyGenerates_topologicalClosure_of_range (ξ := ξ)
1679 rcases hF.existsUnique_lift hWproC ξW hξWcont hξW0 hξWgen with
1680 ⟨ηW, hηW, _⟩
1681 let η : F →* PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F :=
1682 W.subtype.comp ηW
1683 have hηcont : Continuous η := by
1684 simpa [η] using (continuous_subtype_val.comp hηW.1)
1685 have hηgen : ∀ x : X, η (ι x) = ξ x := by
1686 intro x
1687 simpa [η, ξW] using congrArg Subtype.val (hηW.2 x)
1688 have hηright :
1689 (SemidirectProduct.rightHom :
1690 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1691 MonoidHom.id F := by
1692 rcases
1693 hF.existsUnique_lift hF.hasOpenNormalBasisInClass ι hF.continuous_ι hF.map_base
1694 hF.generates_range with
1695 ⟨u, hu, huuniq⟩
1696 have hu_id : MonoidHom.id F = u := by
1697 exact
1698 huuniq (MonoidHom.id F)
1699 ⟨by simpa using (continuous_id : Continuous fun x : F => x), by intro x; rfl⟩
1700 have hu_η :
1701 (SemidirectProduct.rightHom :
1702 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η =
1703 u := by
1704 let v : F →* F :=
1705 (SemidirectProduct.rightHom :
1706 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η
1707 have hη_on_gen :
1708 ∀ x : X, v (ι x) = ι x := by
1709 intro x
1710 have hx := congrArg
1711 (fun z : PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F => z.right)
1712 (hηgen x)
1713 simpa [v, MonoidHom.comp_apply, ξ] using hx
1714 have hvu : v = u := by
1715 exact huuniq v ⟨continuous_permutationalWreathProduct_right.comp hηcont, hη_on_gen⟩
1716 simpa [v] using hvu
1717 calc
1718 (SemidirectProduct.rightHom :
1719 PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F →* F).comp η = u :=
1720 hu_η
1721 _ = MonoidHom.id F := hu_id.symm
1722 have hηcoord :
1723 ∀ q : OpenSubgroupRightQuotient Hc, ∀ x : X,
1724 wreathLeftCoordinate η q (ι x) =
1725 φB ⟨κ (q, x), ⟨(q, x), rfl⟩⟩ := by
1726 intro q x
1727 change (η (ι x)).left q = _
1728 rw [hηgen]
1729 have hηone :
1730 ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
1731 schreierGenerator (X := X) hT t x = 1 →
1732 wreathLeftCoordinate η
1733 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1734 (βF (FreeGroup.of x)) = 1 := by
1735 intro t ht x' hsg'
1736 have hmap :
1737 κ (Quotient.mk'' (βF t), x') = 1 := by
1738 apply Subtype.ext
1739 have hcocycle :=
1740 congrArg Subtype.val
1741 (map_schreierGenerator_eq_cocycle
1742 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hT hβsurj ht x')
1743 change (↑(κ (Quotient.mk'' (βF t), x')) : F) = 1
1744 calc
1745 (↑(κ (Quotient.mk'' (βF t), x')) : F) =
1746 βF ↑(schreierGenerator (X := X) hT t x') := by
1747 simpa [κ, rightSchreierGenerator, τ, Hc,
1748 OpenSubgroupRightQuotient, β, βF] using hcocycle
1749 _ = 1 := by rw [hsg']; exact βF.map_one
1750 have hsrc :
1751 (⟨κ (Quotient.mk'' (βF t), x'), ⟨(Quotient.mk'' (βF t), x'), rfl⟩⟩ : Set.range κ) =
1752 ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by
1753 apply Subtype.ext
1754 exact hmap.trans hκ1.symm
1755 calc
1756 wreathLeftCoordinate η
1757 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
1758 (βF (FreeGroup.of x'))
1760 wreathLeftCoordinate η
1761 (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) (ι x') := by
1762 simp only [FreeGroup.lift_apply_of, βF]
1763 _ = φB ⟨κ (Quotient.mk'' (βF t), x'), ⟨(Quotient.mk'' (βF t), x'), rfl⟩⟩ :=
1764 hηcoord _ _
1765 _ = φB ⟨κ (q1, x0), ⟨(q1, x0), rfl⟩⟩ := by rw [hsrc]
1766 _ = 1 := hφB0
1767 have hτpure :
1768 ∀ q : OpenSubgroupRightQuotient Hc,
1769 wreathLeftCoordinate η q1 (τ q) = 1 := by
1770 intro q
1771 simpa [q1, τ, Hc, OpenSubgroupRightQuotient, openSubgroupRightCoset,
1772 rightCoset, β, βF] using
1773 (wreathLeftCoordinate_basepoint_of_rightSchreierSectionOfComap
1774 (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hT hβsurj η hηright
1775 (hone := hηone) q)
1776 let g : ↥(Hc : Subgroup F) →* B :=
1777 rightQuotientBasepointProjectionHom (H := (Hc : Subgroup F)) η hηright
1778 have hgcont : Continuous g := by
1779 change Continuous
1780 ((fun z : PermutationalWreathProduct B (OpenSubgroupRightQuotient Hc) F =>
1781 z.left q1) ∘ η ∘ Subtype.val)
1782 exact
1783 (continuous_permutationalWreathProduct_left_apply (A := B)
1784 (S := OpenSubgroupRightQuotient Hc) (G := F) q1).comp
1785 (hηcont.comp continuous_subtype_val)
1786 have hgfac : ∀ y : Set.range κ, g y.1 = φB y := by
1787 rintro ⟨y, ⟨⟨q, x'⟩, hy⟩⟩
1788 subst y
1789 change g (κ (q, x')) = φB ⟨κ (q, x'), ⟨(q, x'), rfl⟩⟩
1790 calc
1791 g (κ (q, x')) = wreathLeftCoordinate η q (βF (FreeGroup.of x')) := by
1792 simpa [g, κ, τ, βF] using
1793 (rightQuotientBasepointProjectionHom_rightSchreierGenerator
1794 (F := F) (H := Hc) (τ := τ) (hτ := hτ) (ι := ι) η hηright hτpure q x')
1795 _ = wreathLeftCoordinate η q (ι x') := by simp only [FreeGroup.lift_apply_of, βF]
1796 _ = φB ⟨κ (q, x'), ⟨(q, x'), rfl⟩⟩ := hηcoord q x'
1797 refine ⟨g, ⟨hgcont, hgfac⟩, ?_⟩
1798 intro g' hg'
1799 symm
1800 apply continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
1801 (G := ↥(Hc : Subgroup F)) (A := B) hκgen hgcont hg'.1
1802 intro h hh
1803 exact (hgfac ⟨h, hh⟩).trans (hg'.2 ⟨h, hh⟩).symm
1804 rcases cast (congrArg GoalProp hHc) hMain with
1805 ⟨κ, hκcont, hκbase, hκ1, hpowRange, hκcompact, hκclosed, hκfree⟩
1806 rcases hpowRange with ⟨hpowH, hxNrange⟩
1807 refine ⟨κ, hκcont, hκbase, hκ1, ?_, hκcompact, hκclosed, hκfree⟩
1808 simpa using hxNrange
1812end Profinite
1813end ReidemeisterSchreier