Source: ProCGroups.WreathProducts
1import Mathlib.GroupTheory.SemidirectProduct
2import ProCGroups.ProC.Subgroups.Products
4/-!
5# Pro C Groups / Wreath Products
7This module formalizes permutational wreath products.
8-/
10open scoped Pointwise
12namespace ProCGroups.WreathProducts
14universe u v w
16section RightCosets
18variable {G : Type u} [Group G]
20/-- Right multiplication on right cosets, expressed as a left action by
21`g • [a] = [a * g⁻¹]`. -/
22@[reducible]
23def rightCosetMulAction (H : Subgroup G) :
24 MulAction G (Quotient (QuotientGroup.rightRel H)) where
25 smul g :=
26 Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
27 rw [QuotientGroup.rightRel_apply] at hab ⊢
28 simpa [mul_assoc] using hab
29 one_smul q := by
30 refine Quotient.inductionOn' q ?_
31 intro a
32 apply Quotient.sound'
33 rw [QuotientGroup.rightRel_apply]
34 simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
35 mul_smul g h q := by
36 refine Quotient.inductionOn' q ?_
37 intro a
38 apply Quotient.sound'
39 rw [QuotientGroup.rightRel_apply]
40 simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]
42/-- Acting on a represented right coset multiplies its representative by the inverse on the
43right. -/
44@[simp 900] theorem rightCosetMulAction_mk_smul
45 (H : Subgroup G) (g a : G) :
46 letI := rightCosetMulAction H
47 g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
48 Quotient.mk'' (a * g⁻¹) :=
49 rfl
51/-- Acting by an inverse on a represented right coset multiplies its representative on the
52right. -/
53@[simp 900] theorem rightCosetMulAction_inv_mk_smul
54 (H : Subgroup G) (g a : G) :
55 letI := rightCosetMulAction H
56 g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
57 Quotient.mk'' (a * g) := by
58 rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ a]
59 simp only [inv_inv]
61end RightCosets
63section RightCosetTopology
65variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
67/-- For an open subgroup, the orbit map to the discrete right-coset space is continuous. -/
68theorem continuous_rightCosetMulAction_inv_smul_of_open
69 (H : Subgroup G) (hH : IsOpen (H : Set G))
70 [TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
71 [DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
72 (q : Quotient (QuotientGroup.rightRel H)) :
73 letI := rightCosetMulAction H
74 Continuous fun g : G => g⁻¹ • q := by
75 letI := rightCosetMulAction H
76 rw [continuous_discrete_rng]
77 intro q'
78 classical
79 let a : G := q.out
80 let b : G := q'.out
81 have hpre :
82 (fun g : G => g⁻¹ • q) ⁻¹' (Set.singleton q') =
83 (fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) := by
84 ext g
85 constructor
86 · intro hg
87 have hEq :
88 (Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H)) =
89 Quotient.mk'' b := by
90 calc
91 (Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H))
92 = g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
93 rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
94 _ = g⁻¹ • q := by rw [Quotient.out_eq' q]
95 _ = q' := by
96 change g⁻¹ • q = q' at hg
97 exact hg
98 _ = Quotient.mk'' b := by simp only [Quotient.out_eq, b]
99 have hrel : QuotientGroup.rightRel H (a * g) b := Quotient.eq''.mp hEq
100 simpa [mul_inv_rev, mul_assoc] using (QuotientGroup.rightRel_apply.mp hrel)
101 · intro hg
102 have hrel : QuotientGroup.rightRel H (a * g) b := by
103 rw [QuotientGroup.rightRel_apply]
104 simpa [mul_inv_rev, mul_assoc] using hg
105 calc
106 g⁻¹ • q = g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
107 rw [Quotient.out_eq' q]
108 _ = Quotient.mk'' (a * g) := by
109 rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
110 _ = Quotient.mk'' b := Quotient.eq''.mpr hrel
111 _ = q' := Quotient.out_eq' q'
112 change
113 (fun g : G => g⁻¹ • q) ⁻¹'
114 ({q'} : Set (Quotient (QuotientGroup.rightRel H))) =
115 (fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) at hpre
116 rw [hpre]
117 exact hH.preimage ((continuous_const.mul continuous_inv).mul continuous_const)
119end RightCosetTopology
121section BasicDefinitions
123variable (A : Type u) (S : Type v) (G : Type w)
124variable [Group A] [Group G] [MulAction G S]
126/-- The permutational wreath product attached to a `G`-set `Σ`. -/
127abbrev PermutationalWreathProduct :=
128 (S → A) ⋊[(mulAutArrow (G := G) (A := S) (M := A))] G
130end BasicDefinitions
132section Topology
134variable {A : Type u} {S : Type v} {G : Type w}
135variable [Group A] [Group G] [MulAction G S]
136variable [TopologicalSpace A] [TopologicalSpace G]
138/-- Give a permutational wreath product the topology transported from its product
139representation. -/
140instance instTopologicalSpacePermutationalWreathProduct :
141 TopologicalSpace (PermutationalWreathProduct A S G) :=
142 TopologicalSpace.induced
143 (SemidirectProduct.equivProd :
144 PermutationalWreathProduct A S G ≃ (S → A) × G)
145 inferInstance
147/-- The topology on a permutational wreath product is the one transported from the product of the
148function factor and the right factor. -/
149@[simps!]
150def permutationalWreathProductHomeomorphProd :
151 PermutationalWreathProduct A S G ≃ₜ (S → A) × G where
152 toEquiv := SemidirectProduct.equivProd
153 continuous_toFun := continuous_induced_dom
154 continuous_invFun := by
155 rw [continuous_induced_rng]
156 simpa using (continuous_id : Continuous fun x : (S → A) × G => x)
158/-- The canonical equivalence from a permutational wreath product to its two factors is
159continuous. -/
160@[continuity] theorem continuous_permutationalWreathProduct_equivProd :
161 Continuous
162 (SemidirectProduct.equivProd :
163 PermutationalWreathProduct A S G → (S → A) × G) :=
164 continuous_induced_dom
166/-- Projection to the function factor of a permutational wreath product is continuous. -/
167@[continuity] theorem continuous_permutationalWreathProduct_left :
168 Continuous (fun x : PermutationalWreathProduct A S G => x.left) :=
169 continuous_fst.comp continuous_permutationalWreathProduct_equivProd
171/-- Projection to the acting-group factor of a permutational wreath product is continuous. -/
172@[continuity] theorem continuous_permutationalWreathProduct_right :
173 Continuous (fun x : PermutationalWreathProduct A S G => x.right) :=
174 continuous_snd.comp continuous_permutationalWreathProduct_equivProd
176/-- Evaluation of the function factor at a fixed index is continuous. -/
177@[continuity] theorem continuous_permutationalWreathProduct_left_apply (s : S) :
178 Continuous (fun x : PermutationalWreathProduct A S G => x.left s) :=
179 (continuous_apply s).comp continuous_permutationalWreathProduct_left
181/-- A permutational wreath product is Hausdorff when both group factors are Hausdorff. -/
182instance instT2SpacePermutationalWreathProduct [T2Space A] [T2Space G] :
183 T2Space (PermutationalWreathProduct A S G) :=
184 (permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm.t2Space
186/-- A permutational wreath product is compact when both group factors are compact. -/
187instance instCompactSpacePermutationalWreathProduct [CompactSpace A] [CompactSpace G] :
188 CompactSpace (PermutationalWreathProduct A S G) :=
189 (permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm.compactSpace
191/-- A permutational wreath product is totally disconnected when both group factors are. -/
192instance instTotallyDisconnectedSpacePermutationalWreathProduct
193 [TotallyDisconnectedSpace A] [TotallyDisconnectedSpace G] :
194 TotallyDisconnectedSpace (PermutationalWreathProduct A S G) :=
195 Homeomorph.totallyDisconnectedSpace
196 ((permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm)
198/-- Precomposition by the inverse permutation coming from the `G`-action on `S`. This is the
199action appearing in `mulAutArrow`. -/
200def functionPrecomp (g : G) (f : S → A) : S → A :=
201 fun s => f (g⁻¹ • s)
203omit [Group A] [TopologicalSpace A] [TopologicalSpace G] in
204/-- Precomposition by the action evaluates at the inverse translate of the index. -/
205@[simp] theorem functionPrecomp_apply (g : G) (f : S → A) (s : S) :
206 functionPrecomp g f s = f (g⁻¹ • s) :=
207 rfl
209omit [TopologicalSpace A] [TopologicalSpace G] in
210/-- Mathlib's action on the function factor is precomposition by the inverse permutation. -/
211@[simp] theorem mulAutArrow_apply_eq_functionPrecomp (g : G) (f : S → A) :
212 mulAutArrow (G := G) (A := S) (M := A) g f = functionPrecomp g f :=
213 rfl
215section DiscreteIndex
217variable [TopologicalSpace S] [DiscreteTopology S]
218variable [ContinuousSMul G S] [ContinuousInv G]
220omit [Group A] in
221/-- Evaluation is jointly continuous on the product of a function space with a discrete index
222space. -/
223theorem continuous_eval_of_discreteIndex :
224 Continuous (fun p : (S → A) × S => p.1 p.2) := by
225 rw [continuous_iff_continuousAt]
226 intro p
227 have hs :
228 Prod.snd ⁻¹' ({p.2} : Set S) ∈ nhds p := by
229 refine IsOpen.mem_nhds ((isOpen_discrete ({p.2} : Set S)).preimage continuous_snd) ?_
230 simp only [Set.mem_preimage, Set.mem_singleton_iff]
231 have hEq :
232 (fun q : (S → A) × S => q.1 q.2) =ᶠ[nhds p] fun q => q.1 p.2 := by
233 refine Filter.eventuallyEq_iff_exists_mem.mpr ?_
234 refine ⟨Prod.snd ⁻¹' ({p.2} : Set S), hs, ?_⟩
235 intro q hq
236 simp only [Set.mem_preimage, Set.mem_singleton_iff] at hq
237 simp only [hq]
238 exact ContinuousAt.congr
239 (((continuous_apply p.2).comp continuous_fst).continuousAt) hEq.symm
241omit [Group A] in
242/-- The precomposition action on the function factor is continuous when the index space is
243discrete. -/
244theorem continuous_functionPrecomp :
245 Continuous (fun p : G × (S → A) => functionPrecomp p.1 p.2) := by
246 refine continuous_pi ?_
247 intro s
248 change Continuous (fun p : G × (S → A) => p.2 (p.1⁻¹ • s))
249 have h :=
250 (continuous_eval_of_discreteIndex (A := A) (S := S)).comp
251 (continuous_snd.prodMk
252 (((continuous_inv.comp continuous_fst).smul continuous_const) :
253 Continuous (fun p : G × (S → A) => p.1⁻¹ • s)))
254 change Continuous (fun p : G × (S → A) => p.2 (p.1⁻¹ • s)) at h
255 exact h
257omit [TopologicalSpace A] [TopologicalSpace G] [TopologicalSpace S] [DiscreteTopology S]
258 [ContinuousSMul G S] [ContinuousInv G] in
259/-- The function factor of a product is the first function times the translate of the second. -/
260@[simp 900] theorem permutationalWreathProduct_mul_left
261 (x y : PermutationalWreathProduct A S G) :
262 (x * y).left = x.left * functionPrecomp x.right y.left :=
263 rfl
265omit [TopologicalSpace A] [TopologicalSpace G] [TopologicalSpace S] [DiscreteTopology S]
266 [ContinuousSMul G S] [ContinuousInv G] in
267/-- The function factor of an inverse is the translated pointwise inverse. -/
268@[simp 900] theorem permutationalWreathProduct_inv_left
269 (x : PermutationalWreathProduct A S G) :
270 x⁻¹.left = functionPrecomp x.right⁻¹ x.left⁻¹ :=
271 rfl
273/-- Multiplication in the permutational wreath product is continuous for a discrete index
274space. -/
275instance instContinuousMulPermutationalWreathProduct
276 [ContinuousMul A] [ContinuousMul G] :
277 ContinuousMul (PermutationalWreathProduct A S G) where
278 continuous_mul := by
279 refine continuous_induced_rng.2 ?_
280 change Continuous
281 (fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
282 ((p.1 * p.2).left, (p.1 * p.2).right))
283 have hleft :
284 Continuous
285 (fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
286 p.1.left * functionPrecomp p.1.right p.2.left) :=
287 (continuous_permutationalWreathProduct_left.comp continuous_fst).mul
288 (continuous_functionPrecomp.comp
289 ((continuous_permutationalWreathProduct_right.comp continuous_fst).prodMk
290 (continuous_permutationalWreathProduct_left.comp continuous_snd)))
291 have hright :
292 Continuous
293 (fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
294 p.1.right * p.2.right) :=
295 (continuous_permutationalWreathProduct_right.comp continuous_fst).mul
296 (continuous_permutationalWreathProduct_right.comp continuous_snd)
297 simpa using hleft.prodMk hright
299/-- Inversion in the permutational wreath product is continuous for a discrete index space. -/
300instance instContinuousInvPermutationalWreathProduct
301 [ContinuousInv A] :
302 ContinuousInv (PermutationalWreathProduct A S G) where
303 continuous_inv := by
304 refine continuous_induced_rng.2 ?_
305 change Continuous
306 (fun x : PermutationalWreathProduct A S G => (x⁻¹.left, x⁻¹.right))
307 have hleft :
308 Continuous
309 (fun x : PermutationalWreathProduct A S G =>
310 functionPrecomp x.right⁻¹ x.left⁻¹) :=
311 continuous_functionPrecomp.comp
312 ((continuous_permutationalWreathProduct_right.inv).prodMk
313 (continuous_permutationalWreathProduct_left.inv))
314 have hright :
315 Continuous (fun x : PermutationalWreathProduct A S G => x.right⁻¹) :=
316 continuous_permutationalWreathProduct_right.inv
317 have hfun :
318 (fun x : PermutationalWreathProduct A S G => (x⁻¹.left, x⁻¹.right)) =
319 fun x => (functionPrecomp x.right⁻¹ x.left⁻¹, x.right⁻¹) := by
320 funext x
321 apply Prod.ext
322 · exact permutationalWreathProduct_inv_left x
323 · rfl
324 rw [hfun]
325 exact hleft.prodMk hright
327end DiscreteIndex
329/-- The transported topology makes the permutational wreath product a topological group. -/
330instance instIsTopologicalGroupPermutationalWreathProduct
331 [TopologicalSpace S] [DiscreteTopology S] [ContinuousSMul G S]
332 [IsTopologicalGroup A] [IsTopologicalGroup G] :
333 IsTopologicalGroup (PermutationalWreathProduct A S G) :=
334 { }
336/-- The canonical inclusion of the function factor is continuous. -/
337def permutationalWreathProductInlContinuousHom :
338 (S → A) →ₜ* PermutationalWreathProduct A S G where
339 toMonoidHom := SemidirectProduct.inl
340 continuous_toFun := by
341 refine continuous_induced_rng.2 ?_
342 change Continuous
343 (fun f : S → A =>
344 ((SemidirectProduct.inl f : PermutationalWreathProduct A S G).left,
345 (SemidirectProduct.inl f : PermutationalWreathProduct A S G).right))
346 simpa using (continuous_id.prodMk continuous_const)
348/-- The canonical inclusion of the right factor is continuous. -/
349def permutationalWreathProductInrContinuousHom :
350 G →ₜ* PermutationalWreathProduct A S G where
351 toMonoidHom := SemidirectProduct.inr
352 continuous_toFun := by
353 refine continuous_induced_rng.2 ?_
354 change Continuous
355 (fun g : G =>
356 ((SemidirectProduct.inr g : PermutationalWreathProduct A S G).left,
357 (SemidirectProduct.inr g : PermutationalWreathProduct A S G).right))
358 simpa using (continuous_const.prodMk continuous_id)
360/-- The projection to the right factor is a continuous homomorphism. -/
361def permutationalWreathProductRightContinuousHom :
362 PermutationalWreathProduct A S G →ₜ* G where
363 toMonoidHom := SemidirectProduct.rightHom
364 continuous_toFun := continuous_permutationalWreathProduct_right
366end Topology
368section ProCStructure
370open ProCGroups.ProC
372variable {C : FiniteGroupClass.{u}}
373variable {A : Type u} {S : Type u} {G : Type u}
374variable [Group A] [Group G] [MulAction G S] [Fintype S]
375variable [TopologicalSpace A] [TopologicalSpace S] [TopologicalSpace G]
376variable [IsTopologicalGroup A] [IsTopologicalGroup G]
377variable [ContinuousSMul G S]
379/-- The kernel of the right projection on a permutational wreath product. -/
380abbrev permutationalWreathProductRightKernel :
381 Subgroup (PermutationalWreathProduct A S G) :=
382 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).ker
384/-- The canonical inclusion of the function factor, with codomain restricted to the kernel of the
385right projection. -/
386def permutationalWreathProductInlToKernelContinuousHom :
387 (S → A) →ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G) where
388 toMonoidHom :=
389 { toFun := fun f => ⟨SemidirectProduct.inl f, by simp only
390 [permutationalWreathProductRightKernel, MonoidHom.mem_ker,
391 SemidirectProduct.rightHom_inl]⟩
392 map_one' := by
393 apply Subtype.ext
394 simp only [map_one, OneMemClass.coe_one]
395 map_mul' := by
396 intro f g
397 apply Subtype.ext
398 simp only [map_mul, MulMemClass.mk_mul_mk]}
399 continuous_toFun :=
400 by
401 exact Continuous.subtype_mk
402 (permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G)).continuous_toFun
403 (by
404 intro f
405 change (permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G) f).right = 1
406 rfl)
408omit [Fintype S] [TopologicalSpace S] [IsTopologicalGroup A] [IsTopologicalGroup G]
409 [ContinuousSMul G S] in
410/-- Inclusion of the function factor is a bijection onto the kernel of the right projection. -/
411theorem permutationalWreathProductInlToKernel_bijective :
412 Function.Bijective
413 ((permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G)) :
414 (S → A) → permutationalWreathProductRightKernel (A := A) (S := S) (G := G)) := by
415 constructor
416 · intro f g hfg
417 funext s
418 have hs := congrArg
419 (fun x : permutationalWreathProductRightKernel (A := A) (S := S) (G := G) =>
420 ((x : PermutationalWreathProduct A S G).left s)) hfg
421 change f s = g s at hs
422 exact hs
423 · intro x
424 refine ⟨x.1.left, ?_⟩
425 have hmem :
426 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G)
427 x.1 = 1 := by
428 exact x.2
429 have hright : x.1.right = 1 := by
430 simpa using hmem
431 apply Subtype.ext
432 apply SemidirectProduct.ext
433 · rfl
434 · change (SemidirectProduct.inl x.1.left : PermutationalWreathProduct A S G).right =
435 x.1.right
436 simp only [SemidirectProduct.right_inl, hright]
438/-- The kernel of the right projection is topologically isomorphic to the function factor. -/
439noncomputable def permutationalWreathProductInlKernelContinuousMulEquiv
440 [CompactSpace A] [T2Space A]
441 [T2Space G] :
442 (S → A) ≃ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G) :=
443 ContinuousMulEquiv.ofBijectiveCompactToT2
444 (permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G))
445 (permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G)).continuous_toFun
446 (permutationalWreathProductInlToKernel_bijective (A := A) (S := S) (G := G))
448omit [Fintype S] in
449/-- A permutational wreath product has an open-normal \(C\)-basis whenever both factors do and `C`
450is closed under finite products and extensions. -/
451theorem hasOpenNormalBasisInClass_permutationalWreathProduct
452 [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
453 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
454 (hForm : FiniteGroupClass.Formation C)
455 (hIso : FiniteGroupClass.IsomClosed C)
456 (hExt : FiniteGroupClass.ExtensionClosed C)
457 [DiscreteTopology S]
458 (hA : HasOpenNormalBasisInClass C A)
459 (hG : HasOpenNormalBasisInClass C G) :
460 HasOpenNormalBasisInClass C (PermutationalWreathProduct A S G) := by
461 let hFunc : HasOpenNormalBasisInClass C (S → A) :=
462 HasOpenNormalBasisInClass.pi (C := C) (α := S) (β := fun _ : S => A) hForm (fun _ => hA)
463 have hKernel :
464 HasOpenNormalBasisInClass C (permutationalWreathProductRightKernel (A := A) (S := S) (G :=
465 G)) := by
466 let e :=
467 permutationalWreathProductInlKernelContinuousMulEquiv (A := A) (S := S) (G := G)
468 exact HasOpenNormalBasisInClass.ofContinuousMulEquiv (C := C) hFunc e
469 have hQuot :
470 HasOpenNormalBasisInClass C
471 ((PermutationalWreathProduct A S G) ⧸
472 permutationalWreathProductRightKernel (A := A) (S := S) (G := G)) := by
473 let α : PermutationalWreathProduct A S G →* G :=
474 SemidirectProduct.rightHom
475 have hα : Continuous α := continuous_permutationalWreathProduct_right
476 have hαbar :
477 Continuous (QuotientGroup.kerLift α :
478 (PermutationalWreathProduct A S G) ⧸ α.ker →* G) := by
479 refine (QuotientGroup.isQuotientMap_mk α.ker).continuous_iff.2 ?_
480 change Continuous α
481 exact hα
482 let αbar : ((PermutationalWreathProduct A S G) ⧸ α.ker) →ₜ* G :=
483 { toMonoidHom := QuotientGroup.kerLift α
484 continuous_toFun := hαbar }
485 have hαbar_bij : Function.Bijective αbar := by
486 constructor
487 · exact QuotientGroup.kerLift_injective α
488 · intro g
489 rcases (SemidirectProduct.rightHom_surjective
490 (N := (S → A)) (G := G)
491 (φ := mulAutArrow (G := G) (A := S) (M := A)) g) with ⟨x, rfl⟩
492 refine ⟨QuotientGroup.mk' α.ker x, ?_⟩
493 change α x = x.right
494 rfl
495 let e : ((PermutationalWreathProduct A S G) ⧸ α.ker) ≃ₜ* G :=
496 ContinuousMulEquiv.ofBijectiveCompactToT2 αbar αbar.continuous_toFun hαbar_bij
497 exact HasOpenNormalBasisInClass.ofContinuousMulEquiv (C := C) hG e.symm
498 exact HasOpenNormalBasisInClass.extension (C := C) hIso hForm.quotientClosed hExt
499 (permutationalWreathProductRightKernel (A := A) (S := S) (G := G))
500 (ContinuousMonoidHom.isClosed_ker
501 (permutationalWreathProductRightContinuousHom (A := A) (S := S) (G := G)))
502 hKernel hQuot
504end ProCStructure
506section BasicLemmas
508variable {A : Type u} {S : Type v} {G : Type w}
509variable [Group A] [Group G] [MulAction G S]
511/-- Pointwise multiplication formula in the permutational wreath product. -/
512@[simp] theorem permutationalWreathProduct_mul_left_apply
513 (x y : PermutationalWreathProduct A S G) (s : S) :
514 (x * y).left s = x.left s * y.left (x.right⁻¹ • s) :=
515 rfl
517/-- Pointwise inversion formula in the permutational wreath product. -/
518@[simp] theorem permutationalWreathProduct_inv_left_apply
519 (x : PermutationalWreathProduct A S G) (s : S) :
520 x⁻¹.left s = (x.left (x.right • s))⁻¹ := by
521 change ((mulAutArrow (G := G) (A := S) (M := A) x.right⁻¹) (x.left⁻¹)) s =
522 (x.left (x.right • s))⁻¹
523 change x.left⁻¹ ((x.right⁻¹)⁻¹ • s) = (x.left (x.right • s))⁻¹
524 simp only [inv_inv, Pi.inv_apply]
526/-- The function coordinate of the left-factor inclusion is the included function. -/
527@[simp] theorem permutationalWreathProduct_inl_left_apply
528 (f : S → A) (s : S) :
529 (SemidirectProduct.inl f : PermutationalWreathProduct A S G).left s = f s :=
530 rfl
532/-- The function coordinate of the right-factor inclusion is constantly one. -/
533@[simp] theorem permutationalWreathProduct_inr_left_apply
534 (g : G) (s : S) :
535 (SemidirectProduct.inr g : PermutationalWreathProduct A S G).left s = 1 :=
536 rfl
538/-- The right projection is a retraction of the right-factor inclusion. -/
539@[simp] theorem permutationalWreathProduct_rightHom_comp_inr :
540 (SemidirectProduct.rightHom :
541 PermutationalWreathProduct A S G →* G).comp SemidirectProduct.inr =
542 MonoidHom.id G := by
543 ext g
544 rfl
546end BasicLemmas
548section LeftFactorFunctoriality
550variable {A : Type u} {B : Type v} {S : Type w} {G : Type*}
551variable [Group A] [Group B] [Group G] [MulAction G S]
553/-- Pointwise application of a group homomorphism to the function factor of a wreath product. -/
554def permutationalWreathProductMapFun (α : A →* B) : (S → A) →* (S → B) where
555 toFun f := α ∘ f
556 map_one' := by
557 funext s
558 simp only [Function.comp_apply, Pi.one_apply, map_one]
559 map_mul' f g := by
560 funext s
561 simp only [Function.comp_apply, Pi.mul_apply, map_mul]
563/-- Functoriality of the permutational wreath product in the left factor. -/
564def permutationalWreathProductMapLeft (α : A →* B) :
565 PermutationalWreathProduct A S G →* PermutationalWreathProduct B S G :=
566 SemidirectProduct.map (permutationalWreathProductMapFun (S := S) α) (MonoidHom.id G) fun g => by
567 ext f s
568 rfl
570/-- Mapping the left factor applies the given homomorphism pointwise to the function
571coordinate. -/
572@[simp] theorem permutationalWreathProductMapLeft_left_apply
573 (α : A →* B) (x : PermutationalWreathProduct A S G) (s : S) :
574 (permutationalWreathProductMapLeft (S := S) (G := G) α x).left s = α (x.left s) :=
575 rfl
577/-- Mapping the left factor leaves the acting-group coordinate unchanged. -/
578@[simp] theorem permutationalWreathProductMapLeft_right
579 (α : A →* B) (x : PermutationalWreathProduct A S G) :
580 (permutationalWreathProductMapLeft (S := S) (G := G) α x).right = x.right :=
581 rfl
583/-- Injectivity of the left-factor map is inherited by the wreath-product map. -/
584 theorem permutationalWreathProductMapLeft_injective
585 (α : A →* B) (hα : Function.Injective α) :
586 Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α) := by
587 intro x y hxy
588 ext s
589 · apply hα
590 simpa using congrArg (fun z : PermutationalWreathProduct B S G => z.left s) hxy
591 · simpa using congrArg (fun z : PermutationalWreathProduct B S G => z.right) hxy
593/-- Surjectivity of the left-factor map is inherited by the wreath-product map. -/
594theorem permutationalWreathProductMapLeft_surjective
595 (α : A →* B) (hα : Function.Surjective α) :
596 Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α) := by
597 classical
598 intro x
599 let f : S → A := fun s => Classical.choose (hα (x.left s))
600 refine ⟨⟨f, x.right⟩, ?_⟩
601 ext s
602 · exact Classical.choose_spec (hα (x.left s))
603 · rfl
605/-- If the wreath-product left-factor map is injective, then the original left-factor map is
606injective. A chosen point of `Σ` extracts the relevant coordinate. -/
607theorem injective_of_permutationalWreathProductMapLeft_injective
608 (α : A →* B) (s : S)
609 (hα : Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
610 Function.Injective α := by
611 intro a b hab
612 have hEq :
613 permutationalWreathProductMapLeft (S := S) (G := G) α
614 (SemidirectProduct.inl (fun _ : S => a) : PermutationalWreathProduct A S G) =
615 permutationalWreathProductMapLeft (S := S) (G := G) α
616 (SemidirectProduct.inl (fun _ : S => b) : PermutationalWreathProduct A S G) := by
617 ext t
618 · exact hab
619 · rfl
620 have hPre := hα hEq
621 have := congrArg (fun z : PermutationalWreathProduct A S G => z.left s) hPre
622 simpa using this
624/-- If the wreath-product left-factor map is surjective, then the original left-factor map is
625surjective. A chosen point of `Σ` extracts the relevant coordinate. -/
626theorem surjective_of_permutationalWreathProductMapLeft_surjective
627 (α : A →* B) (s : S)
628 (hα : Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
629 Function.Surjective α := by
630 intro b
631 obtain ⟨x, hx⟩ :=
632 hα (SemidirectProduct.inl (fun _ : S => b) : PermutationalWreathProduct B S G)
633 refine ⟨x.left s, ?_⟩
634 have := congrArg (fun z : PermutationalWreathProduct B S G => z.left s) hx
635 simpa using this
637end LeftFactorFunctoriality
639section LeftFactorFunctorialityTopological
641variable {A : Type u} {B : Type v} {S : Type w} {G : Type*}
642variable [Group A] [Group B] [Group G] [MulAction G S]
643variable [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace G]
645/-- Functoriality of the permutational wreath product in the left factor, upgraded to a continuous
646homomorphism. -/
647def permutationalWreathProductMapLeftContinuous
648 (α : A →ₜ* B) :
649 PermutationalWreathProduct A S G →ₜ* PermutationalWreathProduct B S G where
650 toMonoidHom := permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom
651 continuous_toFun := by
652 refine continuous_induced_rng.2 ?_
653 change Continuous
654 (fun x : PermutationalWreathProduct A S G =>
655 ((permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left,
656 (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right))
657 have hleft :
658 Continuous
659 (fun x : PermutationalWreathProduct A S G =>
660 (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left) := by
661 refine continuous_pi ?_
662 intro s
663 change Continuous (fun x : PermutationalWreathProduct A S G => α (x.left s))
664 have h := α.continuous_toFun.comp
665 (continuous_permutationalWreathProduct_left_apply
666 (A := A) (S := S) (G := G) s)
667 change Continuous (fun x : PermutationalWreathProduct A S G => α (x.left s)) at h
668 exact h
669 have hright :
670 Continuous
671 (fun x : PermutationalWreathProduct A S G =>
672 (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right) := by
673 simpa using continuous_permutationalWreathProduct_right
674 exact hleft.prodMk hright
676end LeftFactorFunctorialityTopological
678section StandardEmbedding
680variable {G : Type u} [Group G]
681variable (H : Subgroup G)
683/--
684The right-coset standard embedding carries the natural multiplication action used in the
685wreath-product construction.
686-/
687instance instMulActionRightCosetStandardEmbedding :
688 MulAction G (Quotient (QuotientGroup.rightRel H)) :=
689 rightCosetMulAction H
691/-- The underlying section attached to a right transversal. -/
692noncomputable def rightTransversalSection {T : Set G}
693 (hT : Subgroup.IsComplement (H : Set G) T) :
694 Quotient (QuotientGroup.rightRel H) → G :=
695 fun q => (hT.rightQuotientEquiv q : G)
697/-- The representative selected by a right transversal lies over the prescribed right coset. -/
698@[simp] theorem rightTransversalSection_spec {T : Set G}
699 (hT : Subgroup.IsComplement (H : Set G) T)
700 (q : Quotient (QuotientGroup.rightRel H)) :
701 Quotient.mk'' (rightTransversalSection (H := H) hT q) = q :=
702 hT.mk''_rightQuotientEquiv q
704/-- The cocycle attached to a section of the right quotient by `H`. -/
705noncomputable def rightQuotientSectionCocycle
706 (τ : Quotient (QuotientGroup.rightRel H) → G)
707 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
708 (g : G) :
709 Quotient (QuotientGroup.rightRel H) → H := by
710 letI := rightCosetMulAction H
711 intro q
712 refine ⟨τ q * g * (τ (g⁻¹ • q))⁻¹, ?_⟩
713 have hq :
714 Quotient.mk'' (τ q * g) = g⁻¹ • q := by
715 calc
716 Quotient.mk'' (τ q * g)
717 = g⁻¹ • (Quotient.mk'' (τ q) : Quotient (QuotientGroup.rightRel H)) := by
718 symm
719 rw [rightCosetMulAction_inv_mk_smul (H := H) g (τ q)]
720 _ = g⁻¹ • q := by rw [hτ q]
721 have hEq :
722 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H)) =
723 Quotient.mk'' (τ (g⁻¹ • q)) := by
724 calc
725 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H))
726 = g⁻¹ • q := hq
727 _ = Quotient.mk'' (τ (g⁻¹ • q)) := by symm; exact hτ (g⁻¹ • q)
728 have hrel : QuotientGroup.rightRel H (τ q * g) (τ (g⁻¹ • q)) := Quotient.exact' hEq
729 rw [QuotientGroup.rightRel_apply] at hrel
730 simpa [mul_inv_rev] using H.inv_mem hrel
732/-- The standard wreath-product embedding attached to a section of the right quotient by `H`. -/
733noncomputable def rightQuotientSectionEmbedding
734 (τ : Quotient (QuotientGroup.rightRel H) → G)
735 (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
736 G →* PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G where
737 toFun g := ⟨rightQuotientSectionCocycle (H := H) τ hτ g, g⟩
738 map_one' := by
739 apply SemidirectProduct.ext
740 · funext q
741 apply Subtype.ext
742 simp only [rightQuotientSectionCocycle, mul_one, inv_one, one_smul, mul_inv_cancel,
743 SemidirectProduct.one_left, Pi.one_apply, OneMemClass.coe_one]
744 · rfl
745 map_mul' g₁ g₂ := by
746 apply SemidirectProduct.ext
747 · funext q
748 apply Subtype.ext
749 simp only [rightQuotientSectionCocycle, mul_inv_rev, mul_smul, mul_assoc,
750 SemidirectProduct.mk_eq_inl_mul_inr,
751 permutationalWreathProduct_mul_left_apply, permutationalWreathProduct_inl_left_apply,
752 SemidirectProduct.right_inl,
753 inv_one, one_smul, permutationalWreathProduct_inr_left_apply, SemidirectProduct.right_inr,
754 mul_one, one_mul,
755 MulMemClass.mk_mul_mk, inv_mul_cancel_left]
756 · rfl
758/-- Pointwise formula for the standard wreath-product embedding attached to a right-quotient
759section. -/
760@[simp] theorem rightQuotientSectionEmbedding_left_apply
761 (τ : Quotient (QuotientGroup.rightRel H) → G)
762 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
763 (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
764 (rightQuotientSectionEmbedding (H := H) τ hτ g).left q =
765 rightQuotientSectionCocycle (H := H) τ hτ g q :=
766 rfl
768/-- The standard wreath-product embedding preserves the acting-group coordinate. -/
769@[simp] theorem rightQuotientSectionEmbedding_right
770 (τ : Quotient (QuotientGroup.rightRel H) → G)
771 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
772 (g : G) :
773 (rightQuotientSectionEmbedding (H := H) τ hτ g).right = g :=
774 rfl
776/-- The right projection is a retraction of the standard right-quotient embedding. -/
777@[simp] theorem rightQuotientSectionEmbedding_rightHom
778 (τ : Quotient (QuotientGroup.rightRel H) → G)
779 (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
780 (SemidirectProduct.rightHom :
781 PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G →* G).comp
782 (rightQuotientSectionEmbedding (H := H) τ hτ) = MonoidHom.id G := by
783 ext g
784 rfl
786/-- The standard embedding attached to a right-quotient section is injective. -/
787theorem rightQuotientSectionEmbedding_injective
788 (τ : Quotient (QuotientGroup.rightRel H) → G)
789 (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
790 Function.Injective (rightQuotientSectionEmbedding (H := H) τ hτ) := by
791 intro g₁ g₂ hEq
792 simpa using congrArg
793 (fun z :
794 PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G => z.right) hEq
796end StandardEmbedding
798section StandardEmbeddingTopological
800variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
801variable (H : Subgroup G)
803/--
804The topological right-coset standard embedding carries the natural multiplication action used in
805the wreath-product construction.
806-/
807instance instMulActionRightCosetStandardEmbeddingTopological :
808 MulAction G (Quotient (QuotientGroup.rightRel H)) :=
809 rightCosetMulAction H
811/-- A continuous right-quotient section gives a continuous standard wreath-product
812embedding. -/
813theorem continuous_rightQuotientSectionEmbedding
814 [TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
815 [DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
816 (hH : IsOpen (H : Set G))
817 (τ : Quotient (QuotientGroup.rightRel H) → G)
818 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
819 (hτcont : Continuous τ) :
820 Continuous
821 (rightQuotientSectionEmbedding (H := H) τ hτ :
822 G → PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G) := by
823 refine continuous_induced_rng.2 ?_
824 change Continuous fun g : G =>
825 ((rightQuotientSectionEmbedding (H := H) τ hτ g).left,
826 (rightQuotientSectionEmbedding (H := H) τ hτ g).right)
827 have hleft :
828 Continuous fun g : G =>
829 (rightQuotientSectionEmbedding (H := H) τ hτ g).left := by
830 refine continuous_pi ?_
831 intro q
832 refine Continuous.subtype_mk ?_ ?_
833 have hqcont :
834 Continuous fun g : G => (g⁻¹ • q : Quotient (QuotientGroup.rightRel H)) :=
835 continuous_rightCosetMulAction_inv_smul_of_open (G := G) H hH q
836 have hcont :
837 Continuous fun g : G => τ q * g * (τ (g⁻¹ • q))⁻¹ := by
838 exact (continuous_const.mul continuous_id).mul ((hτcont.comp hqcont).inv)
839 simpa [rightQuotientSectionEmbedding, rightQuotientSectionCocycle, mul_assoc] using hcont
840 have hright :
841 Continuous fun g : G =>
842 (rightQuotientSectionEmbedding (H := H) τ hτ g).right := by
843 change Continuous (id : G → G)
844 exact continuous_id
845 exact hleft.prodMk hright
847end StandardEmbeddingTopological
849section CocycleFormulas
851variable {A : Type u} {S : Type v} {G : Type w}
852variable [Group A] [Group G] [MulAction G S]
854/-- The left coordinate of an element of a wreath product, viewed as a function of the group
855element on the source. -/
856def wreathLeftCoordinate
857 (ψ : G →* PermutationalWreathProduct A S G) (s : S) : G → A :=
858 fun g => (ψ g).left s
860/-- The cocycle formula for the left coordinates of a homomorphism into a wreath product whose
861right factor is the identity. -/
862theorem wreathLeftCoordinate_mul
863 (ψ : G →* PermutationalWreathProduct A S G)
864 (hψ :
865 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
866 MonoidHom.id G)
867 (s : S) (g₁ g₂ : G) :
868 wreathLeftCoordinate ψ s (g₁ * g₂) =
869 wreathLeftCoordinate ψ s g₁ *
870 wreathLeftCoordinate ψ (g₁⁻¹ • s) g₂ := by
871 have hright : (ψ g₁).right = g₁ := by
872 simpa using congrArg (fun f : G →* G => f g₁) hψ
873 simp only [wreathLeftCoordinate, map_mul, permutationalWreathProduct_mul_left_apply, hright]
875/-- Inversion formula for the left coordinates of a homomorphism into a wreath product whose
876right factor is the identity. -/
877theorem wreathLeftCoordinate_inv
878 (ψ : G →* PermutationalWreathProduct A S G)
879 (hψ :
880 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
881 MonoidHom.id G)
882 (s : S) (g : G) :
883 wreathLeftCoordinate ψ s g⁻¹ =
884 (wreathLeftCoordinate ψ (g • s) g)⁻¹ := by
885 have hright : (ψ g).right = g := by
886 simpa using congrArg (fun f : G →* G => f g) hψ
887 simp only [wreathLeftCoordinate, map_inv, permutationalWreathProduct_inv_left_apply, hright]
889end CocycleFormulas
891section RightQuotientCoordinateRecovery
893variable {A : Type u} {G : Type v}
894variable [Group A] [Group G]
895variable (H : Subgroup G)
897/--
898The coordinate-recovery map for the right-coset standard embedding is compatible with the
899natural multiplication action.
900-/
901instance instMulActionRightCosetCoordinateRecovery :
902 MulAction G (Quotient (QuotientGroup.rightRel H)) :=
903 rightCosetMulAction H
905/-- Basepoint form: if a homomorphism into the wreath product has identity right
906factor and sends the chosen section to elements whose basepoint coordinate is trivial, then the
907basepoint coordinate of the induced subgroup cocycle recovers the original left coordinate. -/
908theorem wreathLeftCoordinate_eq_basepoint_of_rightQuotientSection
909 (τ : Quotient (QuotientGroup.rightRel H) → G)
910 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
911 (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
912 (hψ :
913 (SemidirectProduct.rightHom :
914 PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
915 MonoidHom.id G)
916 (hτpure :
917 ∀ q : Quotient (QuotientGroup.rightRel H),
918 wreathLeftCoordinate ψ
919 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
920 (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
921 wreathLeftCoordinate ψ
922 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
923 (rightQuotientSectionCocycle (H := H) τ hτ g q) =
924 wreathLeftCoordinate ψ q g := by
925 let q' : Quotient (QuotientGroup.rightRel H) := g⁻¹ • q
926 have hτq :
927 (τ q)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) = q := by
928 rw [rightCosetMulAction_inv_mk_smul (H := H) (τ q) 1]
929 simpa using hτ q
930 have hτq' :
931 τ q' • q' = (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
932 calc
933 τ q' • q' = τ q' • (Quotient.mk'' (τ q') : Quotient (QuotientGroup.rightRel H)) := by
934 rw [hτ q']
935 _ = Quotient.mk'' (1 : G) := by
936 rw [rightCosetMulAction_mk_smul (H := H) (τ q') (τ q')]
937 simp only [mul_inv_cancel]
938 have hinv :
939 wreathLeftCoordinate ψ q' (τ q')⁻¹ = 1 := by
940 rw [wreathLeftCoordinate_inv (ψ := ψ) hψ q' (τ q')]
941 simpa [hτq'] using hτpure q'
942 have hq' :
943 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H)) = q' := by
944 calc
945 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H))
946 = (τ q * g)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
947 simp only [mul_inv_rev, rightCosetMulAction_mk_smul, inv_inv, one_mul]
948 _ = g⁻¹ • ((τ q)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))) := by
949 simp only [mul_inv_rev, mul_smul, rightCosetMulAction_mk_smul, inv_inv, one_mul]
950 _ = g⁻¹ • q := by rw [hτq]
951 _ = q' := rfl
952 change
953 wreathLeftCoordinate ψ
954 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
955 ((τ q * g) * (τ q')⁻¹) =
956 wreathLeftCoordinate ψ q g
957 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
958 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
959 (τ q * g) (τ q')⁻¹]
960 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
961 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
962 (τ q) g]
963 simp only [hτpure, hτq, one_mul, mul_inv_rev, rightCosetMulAction_mk_smul, inv_inv, hq', hinv,
964 mul_one, q']
966/-- Basepoint evaluation on the stabilizer subgroup of the trivial right coset, expressed for a
967homomorphism into the wreath product whose right factor is the identity. -/
968def rightQuotientBasepointProjectionHom
969 (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
970 (hψ :
971 (SemidirectProduct.rightHom :
972 PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
973 MonoidHom.id G) :
974 H →* A where
975 toFun h :=
976 wreathLeftCoordinate ψ
977 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) h.1
978 map_one' := by
979 simp only [wreathLeftCoordinate, OneMemClass.coe_one, map_one, SemidirectProduct.one_left,
980 Pi.one_apply]
981 map_mul' a b := by
982 change
983 wreathLeftCoordinate ψ
984 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
985 (a.1 * b.1) =
986 wreathLeftCoordinate ψ
987 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 *
988 wreathLeftCoordinate ψ
989 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) b.1
990 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
991 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 b.1]
992 have ha :
993 a.1⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
994 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
995 rw [rightCosetMulAction_inv_mk_smul (H := H) a.1 1]
996 apply Quotient.sound'
997 rw [QuotientGroup.rightRel_apply]
998 simp only [one_mul, H.inv_mem a.2]
999 simp only [ha]
1001/-- The basepoint projection on `H` evaluates the section cocycle by the corresponding left
1002coordinate, provided the chosen section has trivial basepoint coordinate. -/
1003theorem rightQuotientBasepointProjectionHom_apply_cocycle
1004 (τ : Quotient (QuotientGroup.rightRel H) → G)
1005 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
1006 (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
1007 (hψ :
1008 (SemidirectProduct.rightHom :
1009 PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
1010 MonoidHom.id G)
1011 (hτpure :
1012 ∀ q : Quotient (QuotientGroup.rightRel H),
1013 wreathLeftCoordinate ψ
1014 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
1015 (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
1016 rightQuotientBasepointProjectionHom (H := H) ψ hψ
1017 (rightQuotientSectionCocycle (H := H) τ hτ g q) =
1018 wreathLeftCoordinate ψ q g :=
1019 wreathLeftCoordinate_eq_basepoint_of_rightQuotientSection
1020 (H := H) τ hτ ψ hψ hτpure g q
1022end RightQuotientCoordinateRecovery
1024section StabilizerProjection
1026variable {A : Type u} {S : Type v} {G : Type w}
1027variable [Group A] [Group G] [MulAction G S]
1029/-- Evaluation at a fixed point is a homomorphism on the wreath product over the stabilizer of
1030that point. -/
1031def wreathStabilizerProjection (s : S) :
1032 PermutationalWreathProduct A S (MulAction.stabilizer G s) →* A where
1033 toFun x := x.left s
1034 map_one' := rfl
1035 map_mul' x y := by
1036 have hx : x.right⁻¹ • s = s := by
1037 exact MulAction.mem_stabilizer_iff.mp x.right⁻¹.2
1038 simp only [permutationalWreathProduct_mul_left_apply, hx]
1040/-- The stabilizer projection evaluates the function coordinate at the fixed point. -/
1041@[simp] theorem wreathStabilizerProjection_apply
1042 (s : S) (x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
1043 wreathStabilizerProjection (A := A) (G := G) s x = x.left s :=
1044 rfl
1046/-- The stabilizer projection is natural in the left factor. -/
1047@[simp] theorem wreathStabilizerProjection_mapLeft
1048 {B : Type*} [Group B]
1049 (α : A →* B) (s : S)
1050 (x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
1051 wreathStabilizerProjection (A := B) (G := G) s
1052 (permutationalWreathProductMapLeft
1053 (S := S) (G := MulAction.stabilizer G s) α x) =
1054 α (wreathStabilizerProjection (A := A) (G := G) s x) := by
1055 rfl
1057section RightQuotientBasepoint
1059variable {H : Subgroup G}
1061/-- Basepoint form: on the subgroup `H`, the left coordinate of the standard
1062embedding at the trivial right coset is the given element, provided the section is normalized at
1063the basepoint. -/
1064@[simp 900] theorem rightQuotientSectionEmbedding_left_basepoint_of_mem
1065 (τ : Quotient (QuotientGroup.rightRel H) → G)
1066 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
1067 (hτ1 : τ (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) = 1)
1068 {g : G} (hg : g ∈ H) :
1069 (rightQuotientSectionEmbedding (H := H) τ hτ g).left
1070 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
1071 ⟨g, hg⟩ := by
1072 letI := rightCosetMulAction H
1073 apply Subtype.ext
1074 have hq :
1075 (g⁻¹ •
1076 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))) =
1077 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
1078 rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ 1]
1079 apply Quotient.sound'
1080 rw [QuotientGroup.rightRel_apply]
1081 simpa using hg
1082 simp only [rightQuotientSectionEmbedding, SemidirectProduct.mk_eq_inl_mul_inr, MonoidHom.coe_mk,
1083 OneHom.coe_mk, permutationalWreathProduct_mul_left_apply,
1084 permutationalWreathProduct_inl_left_apply,
1085 rightQuotientSectionCocycle, hτ1, one_mul, hq, inv_one, mul_one, SemidirectProduct.right_inl,
1086 one_smul,
1087 permutationalWreathProduct_inr_left_apply]
1089end RightQuotientBasepoint
1091end StabilizerProjection
1093end ProCGroups.WreathProducts