Yamaguchi Lean 4 Library
ProCGroups/WreathProducts.lean
ProCGroups/WreathProducts/Source

ProCGroups/WreathProducts.lean

1import Mathlib.GroupTheory.SemidirectProduct
2import ProCGroups.ProC.Subgroups.Products
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/WreathProducts.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Permutational wreath products
15Constructs permutational wreath products with the continuity and action formulas needed for finite quotient and solvable quotient arguments.
16-/
18open scoped Pointwise
20namespace ProCGroups.WreathProducts
22universe u v w
24section RightCosets
26variable {G : Type u} [Group G]
28/-- Right multiplication on right cosets, expressed as a left action by
29`g • [a] = [a * g⁻¹]`. -/
30def rightCosetMulAction (H : Subgroup G) :
31 MulAction G (Quotient (QuotientGroup.rightRel H)) where
32 smul g :=
33 Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
34 rw [QuotientGroup.rightRel_apply] at hab ⊢
35 simpa [mul_assoc] using hab
36 one_smul q := by
37 refine Quotient.inductionOn' q ?_
38 intro a
39 apply Quotient.sound'
40 rw [QuotientGroup.rightRel_apply]
41 simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
42 mul_smul g h q := by
43 refine Quotient.inductionOn' q ?_
44 intro a
45 apply Quotient.sound'
46 rw [QuotientGroup.rightRel_apply]
47 simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]
49@[simp 900] theorem rightCosetMulAction_mk_smul
50 (H : Subgroup G) (g a : G) :
51 letI := rightCosetMulAction H
52 g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
53 Quotient.mk'' (a * g⁻¹) :=
54 rfl
56@[simp 900] theorem rightCosetMulAction_inv_mk_smul
57 (H : Subgroup G) (g a : G) :
58 letI := rightCosetMulAction H
59 g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
60 Quotient.mk'' (a * g) := by
61 rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ a]
62 simp only [inv_inv]
64end RightCosets
66section RightCosetTopology
68variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
70/-- For an open subgroup, the orbit map to the discrete right-coset space is continuous. -/
72 (H : Subgroup G) (hH : IsOpen (H : Set G))
73 [TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
74 [DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
75 (q : Quotient (QuotientGroup.rightRel H)) :
76 letI := rightCosetMulAction H
77 Continuous fun g : G => g⁻¹ • q := by
78 letI := rightCosetMulAction H
79 rw [continuous_discrete_rng]
80 intro q'
81 classical
82 let a : G := q.out
83 let b : G := q'.out
84 have hpre :
85 (fun g : G => g⁻¹ • q) ⁻¹' (Set.singleton q') =
86 (fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) := by
87 ext g
88 constructor
89 · intro hg
90 have hEq :
91 (Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H)) =
92 Quotient.mk'' b := by
93 calc
94 (Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H))
95 = g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
96 rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
97 _ = g⁻¹ • q := by rw [Quotient.out_eq' q]
98 _ = q' := by simpa using hg
99 _ = Quotient.mk'' b := by simp only [Quotient.out_eq, b]
100 have hrel : QuotientGroup.rightRel H (a * g) b := Quotient.eq''.mp hEq
101 simpa [mul_inv_rev, mul_assoc] using (QuotientGroup.rightRel_apply.mp hrel)
102 · intro hg
103 have hrel : QuotientGroup.rightRel H (a * g) b := by
104 rw [QuotientGroup.rightRel_apply]
105 simpa [mul_inv_rev, mul_assoc] using hg
106 calc
107 g⁻¹ • q = g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
108 rw [Quotient.out_eq' q]
109 _ = Quotient.mk'' (a * g) := by
110 rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
111 _ = Quotient.mk'' b := Quotient.eq''.mpr hrel
112 _ = q' := Quotient.out_eq' q'
113 rw [show ((fun g : G => g⁻¹ • q) ⁻¹' ({q'} : Set (Quotient (QuotientGroup.rightRel H)))) =
114 (fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) by
115 simpa using hpre]
116 exact hH.preimage ((continuous_const.mul continuous_inv).mul continuous_const)
118end RightCosetTopology
120section BasicDefinitions
122variable (A : Type u) (S : Type v) (G : Type w)
123variable [Group A] [Group G] [MulAction G S]
125/-- The permutational wreath product attached to a `G`-set `Σ`. -/
127 (S → A) ⋊[(mulAutArrow (G := G) (A := S) (M := A))] G
129end BasicDefinitions
131section Topology
133variable {A : Type u} {S : Type v} {G : Type w}
134variable [Group A] [Group G] [MulAction G S]
135variable [TopologicalSpace A] [TopologicalSpace G]
138 TopologicalSpace (PermutationalWreathProduct A S G) :=
139 TopologicalSpace.induced
140 (SemidirectProduct.equivProd :
141 PermutationalWreathProduct A S G ≃ (S → A) × G)
142 inferInstance
144/-- The topology on a permutational wreath product is the one transported from the product of the
145function factor and the right factor. -/
146@[simps!]
148 PermutationalWreathProduct A S G ≃ₜ (S → A) × G where
149 toEquiv := SemidirectProduct.equivProd
150 continuous_toFun := continuous_induced_dom
151 continuous_invFun := by
152 rw [continuous_induced_rng]
153 simpa using (continuous_id : Continuous fun x : (S → A) × G => x)
156 Continuous
157 (SemidirectProduct.equivProd :
158 PermutationalWreathProduct A S G → (S → A) × G) :=
159 continuous_induced_dom
162 Continuous (fun x : PermutationalWreathProduct A S G => x.left) :=
166 Continuous (fun x : PermutationalWreathProduct A S G => x.right) :=
170 Continuous (fun x : PermutationalWreathProduct A S G => x.left s) :=
173instance instT2SpacePermutationalWreathProduct [T2Space A] [T2Space G] :
174 T2Space (PermutationalWreathProduct A S G) :=
175 (permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm.t2Space
177instance instCompactSpacePermutationalWreathProduct [CompactSpace A] [CompactSpace G] :
178 CompactSpace (PermutationalWreathProduct A S G) :=
179 (permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm.compactSpace
182 [TotallyDisconnectedSpace A] [TotallyDisconnectedSpace G] :
183 TotallyDisconnectedSpace (PermutationalWreathProduct A S G) :=
184 Homeomorph.totallyDisconnectedSpace
185 ((permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm)
187/-- Precomposition by the inverse permutation coming from the `G`-action on `S`. This is the
188action appearing in `mulAutArrow`. -/
189def functionPrecomp (g : G) (f : S → A) : S → A :=
190 fun s => f (g⁻¹ • s)
192omit [Group A] [TopologicalSpace A] [TopologicalSpace G] in
193@[simp] theorem functionPrecomp_apply (g : G) (f : S → A) (s : S) :
194 functionPrecomp g f s = f (g⁻¹ • s) :=
195 rfl
197omit [TopologicalSpace A] [TopologicalSpace G] in
198@[simp] theorem mulAutArrow_apply_eq_functionPrecomp (g : G) (f : S → A) :
199 mulAutArrow (G := G) (A := S) (M := A) g f = functionPrecomp g f :=
200 rfl
202section DiscreteIndex
204variable [TopologicalSpace S] [DiscreteTopology S]
205variable [ContinuousSMul G S] [ContinuousInv G]
207omit [Group A] in
208/-- Evaluation is jointly continuous on the product of a function space with a discrete index
209space. -/
211 Continuous (fun p : (S → A) × S => p.1 p.2) := by
212 rw [continuous_iff_continuousAt]
213 intro p
214 have hs :
215 Prod.snd ⁻¹' ({p.2} : Set S) ∈ nhds p := by
216 refine IsOpen.mem_nhds ((isOpen_discrete ({p.2} : Set S)).preimage continuous_snd) ?_
217 simp only [Set.mem_preimage, Set.mem_singleton_iff]
218 have hEq :
219 (fun q : (S → A) × S => q.1 q.2) =ᶠ[nhds p] fun q => q.1 p.2 := by
220 refine Filter.eventuallyEq_iff_exists_mem.mpr ?_
221 refine ⟨Prod.snd ⁻¹' ({p.2} : Set S), hs, ?_⟩
222 intro q hq
223 simp only [Set.mem_preimage, Set.mem_singleton_iff] at hq
224 simp only [hq]
225 exact ContinuousAt.congr
226 (((continuous_apply p.2).comp continuous_fst).continuousAt) hEq.symm
228omit [Group A] in
229/-- The precomposition action on the function factor is continuous when the index space is
230discrete. -/
232 Continuous (fun p : G × (S → A) => functionPrecomp p.1 p.2) := by
233 refine continuous_pi ?_
234 intro s
235 simpa [functionPrecomp] using
236 (continuous_eval_of_discreteIndex (A := A) (S := S)).comp
237 (continuous_snd.prodMk
238 (((continuous_inv.comp continuous_fst).smul continuous_const) :
239 Continuous (fun p : G × (S → A) => p.1⁻¹ • s)))
241omit [TopologicalSpace A] [TopologicalSpace G] [TopologicalSpace S] [DiscreteTopology S]
242 [ContinuousSMul G S] [ContinuousInv G] in
245 (x * y).left = x.left * functionPrecomp x.right y.left :=
246 rfl
248omit [TopologicalSpace A] [TopologicalSpace G] [TopologicalSpace S] [DiscreteTopology S]
249 [ContinuousSMul G S] [ContinuousInv G] in
252 x⁻¹.left = functionPrecomp x.right⁻¹ x.left⁻¹ :=
253 rfl
256 [ContinuousMul A] [ContinuousMul G] [ContinuousSMul G S] :
257 ContinuousMul (PermutationalWreathProduct A S G) where
258 continuous_mul := by
259 refine continuous_induced_rng.2 ?_
260 change Continuous
262 ((p.1 * p.2).left, (p.1 * p.2).right))
263 have hleft :
264 Continuous
266 p.1.left * functionPrecomp p.1.right p.2.left) :=
267 (continuous_permutationalWreathProduct_left.comp continuous_fst).mul
268 (continuous_functionPrecomp.comp
269 ((continuous_permutationalWreathProduct_right.comp continuous_fst).prodMk
270 (continuous_permutationalWreathProduct_left.comp continuous_snd)))
271 have hright :
272 Continuous
274 p.1.right * p.2.right) :=
275 (continuous_permutationalWreathProduct_right.comp continuous_fst).mul
276 (continuous_permutationalWreathProduct_right.comp continuous_snd)
277 simpa using hleft.prodMk hright
280 [ContinuousInv A] [ContinuousInv G] [ContinuousSMul G S] :
281 ContinuousInv (PermutationalWreathProduct A S G) where
282 continuous_inv := by
283 refine continuous_induced_rng.2 ?_
284 change Continuous
285 (fun x : PermutationalWreathProduct A S G => (x⁻¹.left, x⁻¹.right))
286 have hleft :
287 Continuous
289 functionPrecomp x.right⁻¹ x.left⁻¹) :=
290 continuous_functionPrecomp.comp
291 ((continuous_permutationalWreathProduct_right.inv).prodMk
292 (continuous_permutationalWreathProduct_left.inv))
293 have hright :
294 Continuous (fun x : PermutationalWreathProduct A S G => x.right⁻¹) :=
295 continuous_permutationalWreathProduct_right.inv
296 simpa using hleft.prodMk hright
299 [IsTopologicalGroup A] [IsTopologicalGroup G] [ContinuousSMul G S] :
300 IsTopologicalGroup (PermutationalWreathProduct A S G) :=
301 { }
303end DiscreteIndex
305/-- The canonical inclusion of the function factor is continuous. -/
307 (S → A) →ₜ* PermutationalWreathProduct A S G where
308 toMonoidHom := SemidirectProduct.inl
309 continuous_toFun := by
310 refine continuous_induced_rng.2 ?_
311 change Continuous
312 (fun f : S → A =>
313 ((SemidirectProduct.inl f : PermutationalWreathProduct A S G).left,
314 (SemidirectProduct.inl f : PermutationalWreathProduct A S G).right))
315 simpa using (continuous_id.prodMk continuous_const)
317/-- The canonical inclusion of the right factor is continuous. -/
319 G →ₜ* PermutationalWreathProduct A S G where
320 toMonoidHom := SemidirectProduct.inr
321 continuous_toFun := by
322 refine continuous_induced_rng.2 ?_
323 change Continuous
324 (fun g : G =>
325 ((SemidirectProduct.inr g : PermutationalWreathProduct A S G).left,
326 (SemidirectProduct.inr g : PermutationalWreathProduct A S G).right))
327 simpa using (continuous_const.prodMk continuous_id)
329/-- The projection to the right factor is a continuous homomorphism. -/
331 PermutationalWreathProduct A S G →ₜ* G where
332 toMonoidHom := SemidirectProduct.rightHom
335end Topology
337section ProCStructure
339open ProCGroups.ProC
341variable {C : FiniteGroupClass.{u}}
342variable {A : Type u} {S : Type u} {G : Type u}
343variable [Group A] [Group G] [MulAction G S] [Fintype S]
344variable [TopologicalSpace A] [TopologicalSpace S] [TopologicalSpace G]
345variable [IsTopologicalGroup A] [IsTopologicalGroup G]
346variable [ContinuousSMul G S]
348/-- The kernel of the right projection on a permutational wreath product. -/
350 Subgroup (PermutationalWreathProduct A S G) :=
351 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).ker
353/-- The canonical inclusion of the function factor, with codomain restricted to the kernel of the
354right projection. -/
356 (S → A) →ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G) where
357 toMonoidHom :=
358 { toFun := fun f => ⟨SemidirectProduct.inl f, by simp only [permutationalWreathProductRightKernel, MonoidHom.mem_ker, SemidirectProduct.rightHom_inl]⟩
359 map_one' := by
360 apply Subtype.ext
361 simp only [map_one, OneMemClass.coe_one]
362 map_mul' := by
363 intro f g
364 apply Subtype.ext
365 simp only [map_mul, MulMemClass.mk_mul_mk]}
366 continuous_toFun :=
367 by
368 exact Continuous.subtype_mk
369 (permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G)).continuous_toFun
370 (by
371 intro f
372 change (permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G) f).right = 1
373 rfl)
375omit [Fintype S] [TopologicalSpace S] [IsTopologicalGroup A] [IsTopologicalGroup G]
376 [ContinuousSMul G S] in
378 Function.Bijective
380 (S → A) → permutationalWreathProductRightKernel (A := A) (S := S) (G := G)) := by
381 constructor
382 · intro f g hfg
383 funext s
384 have hs := congrArg
385 (fun x : permutationalWreathProductRightKernel (A := A) (S := S) (G := G) =>
386 ((x : PermutationalWreathProduct A S G).left s)) hfg
387 simpa using hs
388 · intro x
389 refine ⟨x.1.left, ?_⟩
390 have hmem :
391 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G)
392 x.1 = 1 := by
393 exact x.2
394 have hright : x.1.right = 1 := by
395 simpa using hmem
396 apply Subtype.ext
397 apply SemidirectProduct.ext
398 · rfl
399 · change (SemidirectProduct.inl x.1.left : PermutationalWreathProduct A S G).right =
400 x.1.right
401 simp only [SemidirectProduct.right_inl, hright]
403/-- The kernel of the right projection is topologically isomorphic to the function factor. -/
405 [CompactSpace A] [T2Space A]
406 [CompactSpace G] [T2Space G]
407 [DiscreteTopology S] :
408 (S → A) ≃ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G) :=
409 ContinuousMulEquiv.ofBijectiveCompactToT2
411 (permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G)).continuous_toFun
414omit [Fintype S] in
415/-- A permutational wreath product over a finite right factor is pro-`C` whenever both factors are
416pro-`C` and `C` is closed under finite products and extensions. -/
418 (hForm : FiniteGroupClass.Formation C)
419 (hIso : FiniteGroupClass.IsomClosed C)
420 (hExt : FiniteGroupClass.ExtensionClosed C)
421 [Finite S]
422 [DiscreteTopology S]
423 (hA : IsProCGroup C A)
424 (hG : IsProCGroup C G) :
425 IsProCGroup C (PermutationalWreathProduct A S G) := by
426 let hFunc : IsProCGroup C (S → A) :=
427 IsProCGroup.pi (C := C) (α := S) (β := fun _ : S => A) hForm (fun _ => hA)
428 letI : CompactSpace A := IsProCGroup.compactSpace hA
429 letI : T2Space A := IsProCGroup.t2Space hA
430 letI : TotallyDisconnectedSpace A := IsProCGroup.totallyDisconnectedSpace hA
431 letI : CompactSpace G := IsProCGroup.compactSpace hG
432 letI : T2Space G := IsProCGroup.t2Space hG
433 letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
434 have hKernel :
435 IsProCGroup C (permutationalWreathProductRightKernel (A := A) (S := S) (G := G)) := by
436 let e :=
438 exact IsProCGroup.ofContinuousMulEquiv (C := C) hIso hForm.quotientClosed hFunc e
439 have hProf :
441 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
442 have hQuot :
443 IsProCGroup C
445 permutationalWreathProductRightKernel (A := A) (S := S) (G := G)) := by
446 let α : PermutationalWreathProduct A S G →* G :=
447 SemidirectProduct.rightHom
449 have hαbar :
450 Continuous (QuotientGroup.kerLift α :
451 (PermutationalWreathProduct A S G) ⧸ α.ker →* G) := by
452 simpa [QuotientGroup.kerLift, QuotientGroup.lift] using
453 hα.quotient_lift (fun a b hab => by
454 simpa [QuotientGroup.con_ker_eq_conKer α, Con.ker_rel] using hab)
455 let αbar : ((PermutationalWreathProduct A S G) ⧸ α.ker) →ₜ* G :=
456 { toMonoidHom := QuotientGroup.kerLift α
457 continuous_toFun := hαbar }
458 have hαbar_bij : Function.Bijective αbar := by
459 constructor
460 · exact QuotientGroup.kerLift_injective α
461 · intro g
462 rcases (SemidirectProduct.rightHom_surjective
463 (N := (S → A)) (G := G)
464 (φ := mulAutArrow (G := G) (A := S) (M := A)) g) with ⟨x, rfl⟩
465 refine ⟨QuotientGroup.mk' α.ker x, ?_⟩
466 change α x = x.right
467 rfl
468 let e : ((PermutationalWreathProduct A S G) ⧸ α.ker) ≃ₜ* G :=
469 ContinuousMulEquiv.ofBijectiveCompactToT2 αbar αbar.continuous_toFun hαbar_bij
470 exact IsProCGroup.ofContinuousMulEquiv (C := C) hIso hForm.quotientClosed hG e.symm
471 exact IsProCGroup.extension (C := C) hIso hForm.quotientClosed hExt hProf
472 (permutationalWreathProductRightKernel (A := A) (S := S) (G := G))
473 hKernel hQuot
475end ProCStructure
477section BasicLemmas
479variable {A : Type u} {S : Type v} {G : Type w}
480variable [Group A] [Group G] [MulAction G S]
482/-- Pointwise multiplication formula in the permutational wreath product. -/
484 (x y : PermutationalWreathProduct A S G) (s : S) :
485 (x * y).left s = x.left s * y.left (x.right⁻¹ • s) :=
486 rfl
488/-- Pointwise inversion formula in the permutational wreath product. -/
490 (x : PermutationalWreathProduct A S G) (s : S) :
491 x⁻¹.left s = (x.left (x.right • s))⁻¹ := by
492 change ((mulAutArrow (G := G) (A := S) (M := A) x.right⁻¹) (x.left⁻¹)) s =
493 (x.left (x.right • s))⁻¹
494 change x.left⁻¹ ((x.right⁻¹)⁻¹ • s) = (x.left (x.right • s))⁻¹
495 simp only [inv_inv, Pi.inv_apply]
498 (f : S → A) (s : S) :
499 (SemidirectProduct.inl f : PermutationalWreathProduct A S G).left s = f s :=
500 rfl
503 (g : G) (s : S) :
504 (SemidirectProduct.inr g : PermutationalWreathProduct A S G).left s = 1 :=
505 rfl
508 (SemidirectProduct.rightHom :
509 PermutationalWreathProduct A S G →* G).comp SemidirectProduct.inr =
510 MonoidHom.id G := by
511 ext g
512 rfl
514end BasicLemmas
516section LeftFactorFunctoriality
518variable {A : Type u} {B : Type v} {S : Type w} {G : Type*}
519variable [Group A] [Group B] [Group G] [MulAction G S]
521/-- Pointwise application of a group homomorphism to the function factor of a wreath product. -/
522def permutationalWreathProductMapFun (α : A →* B) : (S → A) →* (S → B) where
523 toFun f := α ∘ f
524 map_one' := by
525 funext s
526 simp only [Function.comp_apply, Pi.one_apply, map_one]
527 map_mul' f g := by
528 funext s
529 simp only [Function.comp_apply, Pi.mul_apply, map_mul]
531/-- Functoriality of the permutational wreath product in the left factor. -/
534 SemidirectProduct.map (permutationalWreathProductMapFun (S := S) α) (MonoidHom.id G) fun g => by
535 ext f s
536 rfl
539 (α : A →* B) (x : PermutationalWreathProduct A S G) (s : S) :
540 (permutationalWreathProductMapLeft (S := S) (G := G) α x).left s = α (x.left s) :=
541 rfl
544 (α : A →* B) (x : PermutationalWreathProduct A S G) :
545 (permutationalWreathProductMapLeft (S := S) (G := G) α x).right = x.right :=
546 rfl
548/-- Injectivity of the left-factor map is inherited by the wreath-product map. -/
550 (α : A →* B) (hα : Function.Injective α) :
551 Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α) := by
552 intro x y hxy
553 ext s
554 · apply hα
555 simpa using congrArg (fun z : PermutationalWreathProduct B S G => z.left s) hxy
556 · simpa using congrArg (fun z : PermutationalWreathProduct B S G => z.right) hxy
558/-- Surjectivity of the left-factor map is inherited by the wreath-product map. -/
560 (α : A →* B) (hα : Function.Surjective α) :
561 Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α) := by
562 classical
563 intro x
564 let f : S → A := fun s => Classical.choose (hα (x.left s))
565 refine ⟨⟨f, x.right⟩, ?_⟩
566 ext s
567 · exact Classical.choose_spec (hα (x.left s))
568 · rfl
570/-- If the wreath-product left-factor map is injective, then the original left-factor map is
571injective. A chosen point of `Σ` extracts the relevant coordinate. -/
573 (α : A →* B) (s : S)
574 (hα : Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
575 Function.Injective α := by
576 intro a b hab
577 have hEq :
579 (SemidirectProduct.inl (fun _ : S => a) : PermutationalWreathProduct A S G) =
581 (SemidirectProduct.inl (fun _ : S => b) : PermutationalWreathProduct A S G) := by
582 ext t
583 · exact hab
584 · rfl
585 have hPre := hα hEq
586 have := congrArg (fun z : PermutationalWreathProduct A S G => z.left s) hPre
587 simpa using this
589/-- If the wreath-product left-factor map is surjective, then the original left-factor map is
590surjective. A chosen point of `Σ` extracts the relevant coordinate. -/
592 (α : A →* B) (s : S)
593 (hα : Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
594 Function.Surjective α := by
595 intro b
596 obtain ⟨x, hx⟩ :=
597 hα (SemidirectProduct.inl (fun _ : S => b) : PermutationalWreathProduct B S G)
598 refine ⟨x.left s, ?_⟩
599 have := congrArg (fun z : PermutationalWreathProduct B S G => z.left s) hx
600 simpa using this
602end LeftFactorFunctoriality
604section LeftFactorFunctorialityTopological
606variable {A : Type u} {B : Type v} {S : Type w} {G : Type*}
607variable [Group A] [Group B] [Group G] [MulAction G S]
608variable [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace G]
610/-- Functoriality of the permutational wreath product in the left factor, upgraded to a continuous
611homomorphism. -/
613 (α : A →ₜ* B) :
615 toMonoidHom := permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom
616 continuous_toFun := by
617 refine continuous_induced_rng.2 ?_
618 change Continuous
620 ((permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left,
621 (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right))
622 have hleft :
623 Continuous
625 (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left) := by
626 refine continuous_pi ?_
627 intro s
628 simpa using α.continuous_toFun.comp
630 have hright :
631 Continuous
633 (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right) := by
635 exact hleft.prodMk hright
637end LeftFactorFunctorialityTopological
639section StandardEmbedding
641variable {G : Type u} [Group G]
642variable (H : Subgroup G)
645 MulAction G (Quotient (QuotientGroup.rightRel H)) :=
646 rightCosetMulAction H
648/-- The underlying section attached to a right transversal. -/
649noncomputable def rightTransversalSection {T : Set G}
650 (hT : Subgroup.IsComplement (H : Set G) T) :
651 Quotient (QuotientGroup.rightRel H) → G :=
652 fun q => (hT.rightQuotientEquiv q : G)
654@[simp] theorem rightTransversalSection_spec {T : Set G}
655 (hT : Subgroup.IsComplement (H : Set G) T)
656 (q : Quotient (QuotientGroup.rightRel H)) :
657 Quotient.mk'' (rightTransversalSection (H := H) hT q) = q :=
658 hT.mk''_rightQuotientEquiv q
660/-- The cocycle attached to a section of the right quotient by `H`. -/
662 (τ : Quotient (QuotientGroup.rightRel H) → G)
663 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
664 (g : G) :
665 Quotient (QuotientGroup.rightRel H) → H := by
666 letI := rightCosetMulAction H
667 intro q
668 refine ⟨τ q * g * (τ (g⁻¹ • q))⁻¹, ?_⟩
669 have hq :
670 Quotient.mk'' (τ q * g) = g⁻¹ • q := by
671 calc
672 Quotient.mk'' (τ q * g)
673 = g⁻¹ • (Quotient.mk'' (τ q) : Quotient (QuotientGroup.rightRel H)) := by
674 symm
675 rw [rightCosetMulAction_inv_mk_smul (H := H) g (τ q)]
676 _ = g⁻¹ • q := by rw [hτ q]
677 have hEq :
678 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H)) =
679 Quotient.mk'' (τ (g⁻¹ • q)) := by
680 calc
681 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H))
682 = g⁻¹ • q := hq
683 _ = Quotient.mk'' (τ (g⁻¹ • q)) := by symm; exact hτ (g⁻¹ • q)
684 have hrel : QuotientGroup.rightRel H (τ q * g) (τ (g⁻¹ • q)) := Quotient.exact' hEq
685 rw [QuotientGroup.rightRel_apply] at hrel
686 simpa [mul_inv_rev] using H.inv_mem hrel
688/-- The standard wreath-product embedding attached to a section of the right quotient by `H`. -/
690 (τ : Quotient (QuotientGroup.rightRel H) → G)
691 (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
692 G →* PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G where
693 toFun g := ⟨rightQuotientSectionCocycle (H := H) τ hτ g, g⟩
694 map_one' := by
695 apply SemidirectProduct.ext
696 · funext q
697 apply Subtype.ext
698 simp only [rightQuotientSectionCocycle, mul_one, inv_one, one_smul, mul_inv_cancel,
699 SemidirectProduct.one_left, Pi.one_apply, OneMemClass.coe_one]
700 · rfl
701 map_mul' g₁ g₂ := by
702 apply SemidirectProduct.ext
703 · funext q
704 apply Subtype.ext
705 simp only [rightQuotientSectionCocycle, mul_inv_rev, mul_smul, mul_assoc, SemidirectProduct.mk_eq_inl_mul_inr,
707 inv_one, one_smul, permutationalWreathProduct_inr_left_apply, SemidirectProduct.right_inr, mul_one, one_mul,
708 MulMemClass.mk_mul_mk, inv_mul_cancel_left]
709 · rfl
711/-- Pointwise formula for the standard wreath-product embedding attached to a right-quotient
712section. -/
714 (τ : Quotient (QuotientGroup.rightRel H) → G)
715 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
716 (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
717 (rightQuotientSectionEmbedding (H := H) τ hτ g).left q =
718 rightQuotientSectionCocycle (H := H) τ hτ g q :=
719 rfl
722 (τ : Quotient (QuotientGroup.rightRel H) → G)
723 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
724 (g : G) :
725 (rightQuotientSectionEmbedding (H := H) τ hτ g).right = g :=
726 rfl
729 (τ : Quotient (QuotientGroup.rightRel H) → G)
730 (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
731 (SemidirectProduct.rightHom :
732 PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G →* G).comp
733 (rightQuotientSectionEmbedding (H := H) τ hτ) = MonoidHom.id G := by
734 ext g
735 rfl
737/-- The standard embedding attached to a right-quotient section is injective. -/
739 (τ : Quotient (QuotientGroup.rightRel H) → G)
740 (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
741 Function.Injective (rightQuotientSectionEmbedding (H := H) τ hτ) := by
742 intro g₁ g₂ hEq
743 simpa using congrArg
744 (fun z :
745 PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G => z.right) hEq
747end StandardEmbedding
749section StandardEmbeddingTopological
751variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
752variable (H : Subgroup G)
755 MulAction G (Quotient (QuotientGroup.rightRel H)) :=
756 rightCosetMulAction H
759 [TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
760 [DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
761 (hH : IsOpen (H : Set G))
762 (τ : Quotient (QuotientGroup.rightRel H) → G)
763 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
764 (hτcont : Continuous τ) :
765 Continuous
767 G → PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G) := by
768 refine continuous_induced_rng.2 ?_
769 change Continuous fun g : G =>
770 ((rightQuotientSectionEmbedding (H := H) τ hτ g).left,
771 (rightQuotientSectionEmbedding (H := H) τ hτ g).right)
772 have hleft :
773 Continuous fun g : G =>
774 (rightQuotientSectionEmbedding (H := H) τ hτ g).left := by
775 refine continuous_pi ?_
776 intro q
777 refine Continuous.subtype_mk ?_ ?_
778 have hqcont :
779 Continuous fun g : G => (g⁻¹ • q : Quotient (QuotientGroup.rightRel H)) :=
781 have hcont :
782 Continuous fun g : G => τ q * g * (τ (g⁻¹ • q))⁻¹ := by
783 exact (continuous_const.mul continuous_id).mul ((hτcont.comp hqcont).inv)
785 have hright :
786 Continuous fun g : G =>
787 (rightQuotientSectionEmbedding (H := H) τ hτ g).right := by
788 simpa using (continuous_id : Continuous fun g : G => g)
789 exact hleft.prodMk hright
791end StandardEmbeddingTopological
793section CocycleFormulas
795variable {A : Type u} {S : Type v} {G : Type w}
796variable [Group A] [Group G] [MulAction G S]
798/-- The left coordinate of an element of a wreath product, viewed as a function of the group
799element on the source. -/
801 (ψ : G →* PermutationalWreathProduct A S G) (s : S) : G → A :=
802 fun g => (ψ g).left s
804/-- The cocycle formula for the left coordinates of a homomorphism into a wreath product whose
805right factor is the identity. -/
807 (ψ : G →* PermutationalWreathProduct A S G)
808 (hψ :
809 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
810 MonoidHom.id G)
811 (s : S) (g₁ g₂ : G) :
812 wreathLeftCoordinate ψ s (g₁ * g₂) =
814 wreathLeftCoordinate ψ (g₁⁻¹ • s) g₂ := by
815 have hright : (ψ g₁).right = g₁ := by
816 simpa using congrArg (fun f : G →* G => f g₁) hψ
819/-- Inversion formula for the left coordinates of a homomorphism into a wreath product whose
820right factor is the identity. -/
822 (ψ : G →* PermutationalWreathProduct A S G)
823 (hψ :
824 (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
825 MonoidHom.id G)
826 (s : S) (g : G) :
828 (wreathLeftCoordinate ψ (g • s) g)⁻¹ := by
829 have hright : (ψ g).right = g := by
830 simpa using congrArg (fun f : G →* G => f g) hψ
833end CocycleFormulas
835section RightQuotientCoordinateRecovery
837variable {A : Type u} {G : Type v}
838variable [Group A] [Group G]
839variable (H : Subgroup G)
842 MulAction G (Quotient (QuotientGroup.rightRel H)) :=
843 rightCosetMulAction H
845/-- Basepoint form: if a homomorphism into the wreath product has identity right
846factor and sends the chosen section to elements whose basepoint coordinate is trivial, then the
847basepoint coordinate of the induced subgroup cocycle recovers the original left coordinate. -/
849 (τ : Quotient (QuotientGroup.rightRel H) → G)
850 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
851 (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
852 (hψ :
853 (SemidirectProduct.rightHom :
854 PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
855 MonoidHom.id G)
856 (hτpure :
857 ∀ q : Quotient (QuotientGroup.rightRel H),
859 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
860 (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
862 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
863 (rightQuotientSectionCocycle (H := H) τ hτ g q) =
865 let q' : Quotient (QuotientGroup.rightRel H) := g⁻¹ • q
866 have hτq :
867 (τ q)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) = q := by
868 rw [rightCosetMulAction_inv_mk_smul (H := H) (τ q) 1]
869 simpa using hτ q
870 have hτq' :
871 τ q' • q' = (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
872 calc
873 τ q' • q' = τ q' • (Quotient.mk'' (τ q') : Quotient (QuotientGroup.rightRel H)) := by
874 rw [hτ q']
875 _ = Quotient.mk'' (1 : G) := by
876 rw [rightCosetMulAction_mk_smul (H := H) (τ q') (τ q')]
877 simp only [mul_inv_cancel]
878 have hinv :
879 wreathLeftCoordinate ψ q' (τ q')⁻¹ = 1 := by
880 rw [wreathLeftCoordinate_inv (ψ := ψ) hψ q' (τ q')]
881 simpa [hτq'] using hτpure q'
882 have hq' :
883 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H)) = q' := by
884 calc
885 (Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H))
886 = (τ q * g)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
887 simp only [mul_inv_rev, rightCosetMulAction_mk_smul, inv_inv, one_mul]
888 _ = g⁻¹ • ((τ q)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))) := by
889 simp only [mul_inv_rev, mul_smul, rightCosetMulAction_mk_smul, inv_inv, one_mul]
890 _ = g⁻¹ • q := by rw [hτq]
891 _ = q' := rfl
892 change
894 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
895 ((τ q * g) * (τ q')⁻¹) =
897 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
898 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
899 (τ q * g) (τ q')⁻¹]
900 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
901 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
902 (τ q) g]
903 simp only [hτpure, hτq, one_mul, mul_inv_rev, rightCosetMulAction_mk_smul, inv_inv, hq', hinv, mul_one, q']
905/-- Basepoint evaluation on the stabilizer subgroup of the trivial right coset, expressed for a
906homomorphism into the wreath product whose right factor is the identity. -/
908 (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
909 (hψ :
910 (SemidirectProduct.rightHom :
911 PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
912 MonoidHom.id G) :
913 H →* A where
914 toFun h :=
916 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) h.1
917 map_one' := by
918 simp only [wreathLeftCoordinate, OneMemClass.coe_one, map_one, SemidirectProduct.one_left, Pi.one_apply]
919 map_mul' a b := by
920 change
922 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
923 (a.1 * b.1) =
925 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 *
927 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) b.1
928 rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
929 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 b.1]
930 have ha :
931 a.1⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
932 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
933 rw [rightCosetMulAction_inv_mk_smul (H := H) a.1 1]
934 apply Quotient.sound'
935 rw [QuotientGroup.rightRel_apply]
936 simp only [one_mul, H.inv_mem a.2]
937 simp only [ha]
939/-- The basepoint projection on `H` evaluates the section cocycle by the corresponding left
940coordinate, provided the chosen section has trivial basepoint coordinate. -/
942 (τ : Quotient (QuotientGroup.rightRel H) → G)
943 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
944 (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
945 (hψ :
946 (SemidirectProduct.rightHom :
947 PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
948 MonoidHom.id G)
949 (hτpure :
950 ∀ q : Quotient (QuotientGroup.rightRel H),
952 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
953 (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
955 (rightQuotientSectionCocycle (H := H) τ hτ g q) =
958 (H := H) τ hτ ψ hψ hτpure g q
960end RightQuotientCoordinateRecovery
962section StabilizerProjection
964variable {A : Type u} {S : Type v} {G : Type w}
965variable [Group A] [Group G] [MulAction G S]
967/-- Evaluation at a fixed point is a homomorphism on the wreath product over the stabilizer of
968that point. -/
970 PermutationalWreathProduct A S (MulAction.stabilizer G s) →* A where
971 toFun x := x.left s
972 map_one' := rfl
973 map_mul' x y := by
974 have hx : x.right⁻¹ • s = s := by
975 exact MulAction.mem_stabilizer_iff.mp x.right⁻¹.2
979 (s : S) (x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
980 wreathStabilizerProjection (A := A) (G := G) s x = x.left s :=
981 rfl
983/-- The stabilizer projection is natural in the left factor. -/
985 {B : Type*} [Group B]
986 (α : A →* B) (s : S)
987 (x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
988 wreathStabilizerProjection (A := B) (G := G) s
990 (S := S) (G := MulAction.stabilizer G s) α x) =
991 α (wreathStabilizerProjection (A := A) (G := G) s x) := by
992 rfl
994section RightQuotientBasepoint
996variable {H : Subgroup G}
998/-- Basepoint form: on the subgroup `H`, the left coordinate of the standard
999embedding at the trivial right coset is the given element, provided the section is normalized at
1000the basepoint. -/
1002 (τ : Quotient (QuotientGroup.rightRel H) → G)
1003 (hτ : ∀ q, Quotient.mk'' (τ q) = q)
1004 (hτ1 : τ (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) = 1)
1005 {g : G} (hg : g ∈ H) :
1006 (rightQuotientSectionEmbedding (H := H) τ hτ g).left
1007 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
1008 ⟨g, hg⟩ := by
1009 letI := rightCosetMulAction H
1010 apply Subtype.ext
1011 have hq :
1012 (g⁻¹ •
1013 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))) =
1014 (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
1015 rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ 1]
1016 apply Quotient.sound'
1017 rw [QuotientGroup.rightRel_apply]
1018 simpa using hg
1019 simp only [rightQuotientSectionEmbedding, SemidirectProduct.mk_eq_inl_mul_inr, MonoidHom.coe_mk,
1021 rightQuotientSectionCocycle, hτ1, one_mul, hq, inv_one, mul_one, SemidirectProduct.right_inl, one_smul,
1024end RightQuotientBasepoint
1026end StabilizerProjection
1028end ProCGroups.WreathProducts