ProCGroups.WreathProducts
This module formalizes permutational wreath products.
import
- Mathlib.GroupTheory.SemidirectProduct
- ProCGroups.ProC.Subgroups.Products
def rightCosetMulAction (H : Subgroup G) :
MulAction G (Quotient (QuotientGroup.rightRel H)) where
smul g :=
Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
rw [QuotientGroup.rightRel_apply] at hab ⊢
simpa [mul_assoc] using hab
one_smul q := by
refine Quotient.inductionOn' q ?_
intro a
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
mul_smul g h q := by
refine Quotient.inductionOn' q ?_
intro a
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]Right multiplication on right cosets, expressed as the left action \(g\cdot [a]=[a g^{-1}]\).
@[simp 900] theorem rightCosetMulAction_mk_smul
(H : Subgroup G) (g a : G) :
letIThe right-coset action formula sends a coset representative to the expected multiplied representative.
Show proof
rightCosetMulAction H
g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
Quotient.mk'' (a * g⁻¹) :=
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp 900] theorem rightCosetMulAction_inv_mk_smul
(H : Subgroup G) (g a : G) :
letIThe inverse right-coset action formula sends a coset representative to the expected multiplied representative.
Show proof
rightCosetMulAction H
g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
Quotient.mk'' (a * g) := by
rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ a]
simp only [inv_inv]Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem continuous_rightCosetMulAction_inv_smul_of_open
(H : Subgroup G) (hH : IsOpen (H : Set G))
[TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
[DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
(q : Quotient (QuotientGroup.rightRel H)) :
letIFor an open subgroup, the orbit map to the discrete right-coset space is continuous.
Show proof
rightCosetMulAction H
Continuous fun g : G => g⁻¹ • q := by
letI := rightCosetMulAction H
rw [continuous_discrete_rng]
intro q'
classical
let a : G := q.out
let b : G := q'.out
have hpre :
(fun g : G => g⁻¹ • q) ⁻¹' (Set.singleton q') =
(fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) := by
ext g
constructor
· intro hg
have hEq :
(Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H)) =
Quotient.mk'' b := by
calc
(Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H))
= g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
_ = g⁻¹ • q := by rw [Quotient.out_eq' q]
_ = q' := by simpa using hg
_ = Quotient.mk'' b := by simp only [Quotient.out_eq, b]
have hrel : QuotientGroup.rightRel H (a * g) b := Quotient.eq''.mp hEq
simpa [mul_inv_rev, mul_assoc] using (QuotientGroup.rightRel_apply.mp hrel)
· intro hg
have hrel : QuotientGroup.rightRel H (a * g) b := by
rw [QuotientGroup.rightRel_apply]
simpa [mul_inv_rev, mul_assoc] using hg
calc
g⁻¹ • q = g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
rw [Quotient.out_eq' q]
_ = Quotient.mk'' (a * g) := by
rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
_ = Quotient.mk'' b := Quotient.eq''.mpr hrel
_ = q' := Quotient.out_eq' q'
rw [show ((fun g : G => g⁻¹ • q) ⁻¹' ({q'} : Set (Quotient (QuotientGroup.rightRel H)))) =
(fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) by
simpa using hpre]
exact hH.preimage ((continuous_const.mul continuous_inv).mul continuous_const)Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□abbrev PermutationalWreathProduct :=
(S → A) ⋊[(mulAutArrow (G := G) (A := S) (M := A))] GThe permutational wreath product attached to a \(G\)-set \(\Sigma\).
instance instTopologicalSpacePermutationalWreathProduct :
TopologicalSpace (PermutationalWreathProduct A S G) :=
TopologicalSpace.induced
(SemidirectProduct.equivProd :
PermutationalWreathProduct A S G ≃ (S → A) × G)
inferInstanceThe constructed object carries the topological space structure inherited from its construction.
def permutationalWreathProductHomeomorphProd :
PermutationalWreathProduct A S G ≃ₜ (S → A) × G where
toEquiv := SemidirectProduct.equivProd
continuous_toFun := continuous_induced_dom
continuous_invFun := by
rw [continuous_induced_rng]
simpa using (continuous_id : Continuous fun x : (S → A) × G => x)The topology on a permutational wreath product is the one transported from the product of the function factor and the right factor.
@[continuity] theorem continuous_permutationalWreathProduct_equivProd :
Continuous
(SemidirectProduct.equivProd :
PermutationalWreathProduct A S G → (S → A) × G)The product equivalence from the permutational wreath product to the function factor times the acting group is continuous.
Show proof
continuous_induced_domProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[continuity] theorem continuous_permutationalWreathProduct_left :
Continuous (fun x : PermutationalWreathProduct A S G => x.left)The left-coordinate projection of the permutational wreath product is continuous.
Show proof
continuous_fst.comp continuous_permutationalWreathProduct_equivProdProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[continuity] theorem continuous_permutationalWreathProduct_right :
Continuous (fun x : PermutationalWreathProduct A S G => x.right)The right-coordinate projection of the permutational wreath product is continuous.
Show proof
continuous_snd.comp continuous_permutationalWreathProduct_equivProdProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[continuity] theorem continuous_permutationalWreathProduct_left_apply (s : S) :
Continuous (fun x : PermutationalWreathProduct A S G => x.left s)The wreath-product map evaluates componentwise on the base and permutation coordinates.
Show proof
(continuous_apply s).comp continuous_permutationalWreathProduct_leftProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□instance instT2SpacePermutationalWreathProduct [T2Space A] [T2Space G] :
T2Space (PermutationalWreathProduct A S G) :=
(permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm.t2SpaceThe constructed object is Hausdorff, with its \(T_2\) structure inherited from the profinite construction.
instance instCompactSpacePermutationalWreathProduct [CompactSpace A] [CompactSpace G] :
CompactSpace (PermutationalWreathProduct A S G) :=
(permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm.compactSpaceThe constructed object carries the compact space structure inherited from its profinite construction.
instance instTotallyDisconnectedSpacePermutationalWreathProduct
[TotallyDisconnectedSpace A] [TotallyDisconnectedSpace G] :
TotallyDisconnectedSpace (PermutationalWreathProduct A S G) :=
Homeomorph.totallyDisconnectedSpace
((permutationalWreathProductHomeomorphProd (A := A) (S := S) (G := G)).symm)The constructed object carries the totally disconnected space structure inherited from its profinite construction.
def functionPrecomp (g : G) (f : S → A) : S → A :=
fun s => f (g⁻¹ • s)The function coordinate is precomposed by the inverse permutation induced by the \(G\)-action on \(S\).
@[simp] theorem functionPrecomp_apply (g : G) (f : S → A) (s : S) :
functionPrecomp g f s = f (g⁻¹ • s)The composite map is computed pointwise by applying the constituent coordinate formulas in succession.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem mulAutArrow_apply_eq_functionPrecomp (g : G) (f : S → A) :
mulAutArrow (G := G) (A := S) (M := A) g f = functionPrecomp g fThe function coordinate is precomposed by the inverse permutation induced by the \(G\)-action on \(S\).
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem continuous_eval_of_discreteIndex :
Continuous (fun p : (S → A) × S => p.1 p.2)Evaluation is jointly continuous on the product of a function space with a discrete index space.
Show proof
by
rw [continuous_iff_continuousAt]
intro p
have hs :
Prod.snd ⁻¹' ({p.2} : Set S) ∈ nhds p := by
refine IsOpen.mem_nhds ((isOpen_discrete ({p.2} : Set S)).preimage continuous_snd) ?_
simp only [Set.mem_preimage, Set.mem_singleton_iff]
have hEq :
(fun q : (S → A) × S => q.1 q.2) =ᶠ[nhds p] fun q => q.1 p.2 := by
refine Filter.eventuallyEq_iff_exists_mem.mpr ?_
refine ⟨Prod.snd ⁻¹' ({p.2} : Set S), hs, ?_⟩
intro q hq
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hq
simp only [hq]
exact ContinuousAt.congr
(((continuous_apply p.2).comp continuous_fst).continuousAt) hEq.symmProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem continuous_functionPrecomp :
Continuous (fun p : G × (S → A) => functionPrecomp p.1 p.2)The function coordinate is precomposed by the inverse permutation induced by the \(G\)-action on \(S\).
Show proof
by
refine continuous_pi ?_
intro s
simpa [functionPrecomp] using
(continuous_eval_of_discreteIndex (A := A) (S := S)).comp
(continuous_snd.prodMk
(((continuous_inv.comp continuous_fst).smul continuous_const) :
Continuous (fun p : G × (S → A) => p.1⁻¹ • s)))Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp 900] theorem permutationalWreathProduct_mul_left
(x y : PermutationalWreathProduct A S G) :
(x * y).left = x.left * functionPrecomp x.right y.leftThe left coordinate of multiplication in the permutational wreath product is the pointwise product twisted by the right action.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp 900] theorem permutationalWreathProduct_inv_left
(x : PermutationalWreathProduct A S G) :
x⁻¹.left = functionPrecomp x.right⁻¹ x.left⁻¹The left coordinate of the inverse in the permutational wreath product is computed pointwise using the inverse action.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□instance instContinuousMulPermutationalWreathProduct
[ContinuousMul A] [ContinuousMul G] [ContinuousSMul G S] :
ContinuousMul (PermutationalWreathProduct A S G) where
continuous_mul := by
refine continuous_induced_rng.2 ?_
change Continuous
(fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
((p.1 * p.2).left, (p.1 * p.2).right))
have hleft :
Continuous
(fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
p.1.left * functionPrecomp p.1.right p.2.left) :=
(continuous_permutationalWreathProduct_left.comp continuous_fst).mul
(continuous_functionPrecomp.comp
((continuous_permutationalWreathProduct_right.comp continuous_fst).prodMk
(continuous_permutationalWreathProduct_left.comp continuous_snd)))
have hright :
Continuous
(fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
p.1.right * p.2.right) :=
(continuous_permutationalWreathProduct_right.comp continuous_fst).mul
(continuous_permutationalWreathProduct_right.comp continuous_snd)
simpa using hleft.prodMk hrightMultiplication in the permutational wreath product is continuous for the product topology transported from the function and right factors.
instance instContinuousInvPermutationalWreathProduct
[ContinuousInv A] [ContinuousInv G] [ContinuousSMul G S] :
ContinuousInv (PermutationalWreathProduct A S G) where
continuous_inv := by
refine continuous_induced_rng.2 ?_
change Continuous
(fun x : PermutationalWreathProduct A S G => (x⁻¹.left, x⁻¹.right))
have hleft :
Continuous
(fun x : PermutationalWreathProduct A S G =>
functionPrecomp x.right⁻¹ x.left⁻¹) :=
continuous_functionPrecomp.comp
((continuous_permutationalWreathProduct_right.inv).prodMk
(continuous_permutationalWreathProduct_left.inv))
have hright :
Continuous (fun x : PermutationalWreathProduct A S G => x.right⁻¹) :=
continuous_permutationalWreathProduct_right.inv
simpa using hleft.prodMk hrightThe permutational wreath product carries the topological group structure induced by its factors.
instance instIsTopologicalGroupPermutationalWreathProduct
[IsTopologicalGroup A] [IsTopologicalGroup G] [ContinuousSMul G S] :
IsTopologicalGroup (PermutationalWreathProduct A S G) :=
{ }The object is a topological group with the induced group operations and topology.
def permutationalWreathProductInlContinuousHom :
(S → A) →ₜ* PermutationalWreathProduct A S G where
toMonoidHom := SemidirectProduct.inl
continuous_toFun := by
refine continuous_induced_rng.2 ?_
change Continuous
(fun f : S → A =>
((SemidirectProduct.inl f : PermutationalWreathProduct A S G).left,
(SemidirectProduct.inl f : PermutationalWreathProduct A S G).right))
simpa using (continuous_id.prodMk continuous_const)The canonical inclusion of the function factor is continuous.
def permutationalWreathProductInrContinuousHom :
G →ₜ* PermutationalWreathProduct A S G where
toMonoidHom := SemidirectProduct.inr
continuous_toFun := by
refine continuous_induced_rng.2 ?_
change Continuous
(fun g : G =>
((SemidirectProduct.inr g : PermutationalWreathProduct A S G).left,
(SemidirectProduct.inr g : PermutationalWreathProduct A S G).right))
simpa using (continuous_const.prodMk continuous_id)The canonical inclusion of the right factor is continuous.
def permutationalWreathProductRightContinuousHom :
PermutationalWreathProduct A S G →ₜ* G where
toMonoidHom := SemidirectProduct.rightHom
continuous_toFun := continuous_permutationalWreathProduct_rightThe projection to the right factor is a continuous homomorphism.
abbrev permutationalWreathProductRightKernel :
Subgroup (PermutationalWreathProduct A S G) :=
(SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).kerThe kernel of the right projection on a permutational wreath product.
def permutationalWreathProductInlToKernelContinuousHom :
(S → A) →ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G) where
toMonoidHom :=
{ toFun := fun f => ⟨SemidirectProduct.inl f, by simp only [permutationalWreathProductRightKernel, MonoidHom.mem_ker, SemidirectProduct.rightHom_inl]⟩
map_one' := by
apply Subtype.ext
simp only [map_one, OneMemClass.coe_one]
map_mul' := by
intro f g
apply Subtype.ext
simp only [map_mul, MulMemClass.mk_mul_mk]}
continuous_toFun :=
by
exact Continuous.subtype_mk
(permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G)).continuous_toFun
(by
intro f
change (permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G) f).right = 1
rfl)The canonical inclusion of the function factor, with codomain restricted to the kernel of the right projection.
theorem permutationalWreathProductInlToKernel_bijective :
Function.Bijective
((permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G)) :
(S → A) → permutationalWreathProductRightKernel (A := A) (S := S) (G := G))The canonical inclusion of the function part into the kernel of the projection from the permutational wreath product is bijective.
Show proof
by
constructor
· intro f g hfg
funext s
have hs := congrArg
(fun x : permutationalWreathProductRightKernel (A := A) (S := S) (G := G) =>
((x : PermutationalWreathProduct A S G).left s)) hfg
simpa using hs
· intro x
refine ⟨x.1.left, ?_⟩
have hmem :
(SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G)
x.1 = 1 := by
exact x.2
have hright : x.1.right = 1 := by
simpa using hmem
apply Subtype.ext
apply SemidirectProduct.ext
· rfl
· change (SemidirectProduct.inl x.1.left : PermutationalWreathProduct A S G).right =
x.1.right
simp only [SemidirectProduct.right_inl, hright]Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□noncomputable def permutationalWreathProductInlKernelContinuousMulEquiv
[CompactSpace A] [T2Space A]
[CompactSpace G] [T2Space G]
[DiscreteTopology S] :
(S → A) ≃ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G) :=
ContinuousMulEquiv.ofBijectiveCompactToT2
(permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G))
(permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G)).continuous_toFun
(permutationalWreathProductInlToKernel_bijective (A := A) (S := S) (G := G))The kernel of the right projection is topologically isomorphic to the function factor.
theorem isProCGroup_permutationalWreathProduct
(hForm : FiniteGroupClass.Formation C)
(hIso : FiniteGroupClass.IsomClosed C)
(hExt : FiniteGroupClass.ExtensionClosed C)
[Finite S]
[DiscreteTopology S]
(hA : IsProCGroup C A)
(hG : IsProCGroup C G) :
IsProCGroup C (PermutationalWreathProduct A S G)Show proof
by
let hFunc : IsProCGroup C (S → A) :=
IsProCGroup.pi (C := C) (α := S) (β := fun _ : S => A) hForm (fun _ => hA)
letI : CompactSpace A := IsProCGroup.compactSpace hA
letI : T2Space A := IsProCGroup.t2Space hA
letI : TotallyDisconnectedSpace A := IsProCGroup.totallyDisconnectedSpace hA
letI : CompactSpace G := IsProCGroup.compactSpace hG
letI : T2Space G := IsProCGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
have hKernel :
IsProCGroup C (permutationalWreathProductRightKernel (A := A) (S := S) (G := G)) := by
let e :=
permutationalWreathProductInlKernelContinuousMulEquiv (A := A) (S := S) (G := G)
exact IsProCGroup.ofContinuousMulEquiv (C := C) hIso hForm.quotientClosed hFunc e
have hProf :
IsProfiniteGroup (PermutationalWreathProduct A S G) := by
exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
have hQuot :
IsProCGroup C
((PermutationalWreathProduct A S G) ⧸
permutationalWreathProductRightKernel (A := A) (S := S) (G := G)) := by
let α : PermutationalWreathProduct A S G →* G :=
SemidirectProduct.rightHom
have hα : Continuous α := continuous_permutationalWreathProduct_right
have hαbar :
Continuous (QuotientGroup.kerLift α :
(PermutationalWreathProduct A S G) ⧸ α.ker →* G) := by
simpa [QuotientGroup.kerLift, QuotientGroup.lift] using
hα.quotient_lift (fun a b hab => by
simpa [QuotientGroup.con_ker_eq_conKer α, Con.ker_rel] using hab)
let αbar : ((PermutationalWreathProduct A S G) ⧸ α.ker) →ₜ* G :=
{ toMonoidHom := QuotientGroup.kerLift α
continuous_toFun := hαbar }
have hαbar_bij : Function.Bijective αbar := by
constructor
· exact QuotientGroup.kerLift_injective α
· intro g
rcases (SemidirectProduct.rightHom_surjective
(N := (S → A)) (G := G)
(φ := mulAutArrow (G := G) (A := S) (M := A)) g) with ⟨x, rfl⟩
refine ⟨QuotientGroup.mk' α.ker x, ?_⟩
change α x = x.right
rfl
let e : ((PermutationalWreathProduct A S G) ⧸ α.ker) ≃ₜ* G :=
ContinuousMulEquiv.ofBijectiveCompactToT2 αbar αbar.continuous_toFun hαbar_bij
exact IsProCGroup.ofContinuousMulEquiv (C := C) hIso hForm.quotientClosed hG e.symm
exact IsProCGroup.extension (C := C) hIso hForm.quotientClosed hExt hProf
(permutationalWreathProductRightKernel (A := A) (S := S) (G := G))
hKernel hQuotProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem permutationalWreathProduct_mul_left_apply
(x y : PermutationalWreathProduct A S G) (s : S) :
(x * y).left s = x.left s * y.left (x.right⁻¹ • s)Pointwise multiplication formula in the permutational wreath product.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem permutationalWreathProduct_inv_left_apply
(x : PermutationalWreathProduct A S G) (s : S) :
x⁻¹.left s = (x.left (x.right • s))⁻¹Pointwise inversion formula in the permutational wreath product.
Show proof
by
change ((mulAutArrow (G := G) (A := S) (M := A) x.right⁻¹) (x.left⁻¹)) s =
(x.left (x.right • s))⁻¹
change x.left⁻¹ ((x.right⁻¹)⁻¹ • s) = (x.left (x.right • s))⁻¹
simp only [inv_inv, Pi.inv_apply]Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem permutationalWreathProduct_inl_left_apply
(f : S → A) (s : S) :
(SemidirectProduct.inl f : PermutationalWreathProduct A S G).left s = f sThe wreath-product map evaluates componentwise on the base and permutation coordinates.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem permutationalWreathProduct_inr_left_apply
(g : G) (s : S) :
(SemidirectProduct.inr g : PermutationalWreathProduct A S G).left s = 1The wreath-product map evaluates componentwise on the base and permutation coordinates.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem permutationalWreathProduct_rightHom_comp_inr :
(SemidirectProduct.rightHom :
PermutationalWreathProduct A S G →* G).comp SemidirectProduct.inr =
MonoidHom.id GComposing the right projection with the right-factor inclusion of the permutational wreath product is the identity.
Show proof
by
ext g
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□def permutationalWreathProductMapFun (α : A →* B) : (S → A) →* (S → B) where
toFun f := α ∘ f
map_one' := by
funext s
simp only [Function.comp_apply, Pi.one_apply, map_one]
map_mul' f g := by
funext s
simp only [Function.comp_apply, Pi.mul_apply, map_mul]Pointwise application of a group homomorphism to the function factor of a wreath product.
def permutationalWreathProductMapLeft (α : A →* B) :
PermutationalWreathProduct A S G →* PermutationalWreathProduct B S G :=
SemidirectProduct.map (permutationalWreathProductMapFun (S := S) α) (MonoidHom.id G) fun g => by
ext f s
rflFunctoriality of the permutational wreath product in the left factor.
@[simp] theorem permutationalWreathProductMapLeft_left_apply
(α : A →* B) (x : PermutationalWreathProduct A S G) (s : S) :
(permutationalWreathProductMapLeft (S := S) (G := G) α x).left s = α (x.left s)The wreath-product map evaluates componentwise on the base and permutation coordinates.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem permutationalWreathProductMapLeft_right
(α : A →* B) (x : PermutationalWreathProduct A S G) :
(permutationalWreathProductMapLeft (S := S) (G := G) α x).right = x.rightThe right component of the wreath-product or quotient-section map is the expected homomorphism.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□ theorem permutationalWreathProductMapLeft_injective
(α : A →* B) (hα : Function.Injective α) :
Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α)Injectivity of the left-factor map is inherited by the wreath-product map.
Show proof
by
intro x y hxy
ext s
· apply hα
simpa using congrArg (fun z : PermutationalWreathProduct B S G => z.left s) hxy
· simpa using congrArg (fun z : PermutationalWreathProduct B S G => z.right) hxyProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem permutationalWreathProductMapLeft_surjective
(α : A →* B) (hα : Function.Surjective α) :
Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α)Surjectivity of the left-factor map is inherited by the wreath-product map.
Show proof
by
classical
intro x
let f : S → A := fun s => Classical.choose (hα (x.left s))
refine ⟨⟨f, x.right⟩, ?_⟩
ext s
· exact Classical.choose_spec (hα (x.left s))
· rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem injective_of_permutationalWreathProductMapLeft_injective
(α : A →* B) (s : S)
(hα : Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
Function.Injective αIf the wreath-product left-factor map is injective, then the original left-factor map is injective. A chosen point of \(\Sigma\) extracts the selected coordinate.
Show proof
by
intro a b hab
have hEq :
permutationalWreathProductMapLeft (S := S) (G := G) α
(SemidirectProduct.inl (fun _ : S => a) : PermutationalWreathProduct A S G) =
permutationalWreathProductMapLeft (S := S) (G := G) α
(SemidirectProduct.inl (fun _ : S => b) : PermutationalWreathProduct A S G) := by
ext t
· exact hab
· rfl
have hPre := hα hEq
have := congrArg (fun z : PermutationalWreathProduct A S G => z.left s) hPre
simpa using thisProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem surjective_of_permutationalWreathProductMapLeft_surjective
(α : A →* B) (s : S)
(hα : Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
Function.Surjective αIf the wreath-product left-factor map is surjective, then the original left-factor map is surjective. A chosen point of \(\Sigma\) extracts the selected coordinate.
Show proof
by
intro b
obtain ⟨x, hx⟩ :=
hα (SemidirectProduct.inl (fun _ : S => b) : PermutationalWreathProduct B S G)
refine ⟨x.left s, ?_⟩
have := congrArg (fun z : PermutationalWreathProduct B S G => z.left s) hx
simpa using thisProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□def permutationalWreathProductMapLeftContinuous
(α : A →ₜ* B) :
PermutationalWreathProduct A S G →ₜ* PermutationalWreathProduct B S G where
toMonoidHom := permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom
continuous_toFun := by
refine continuous_induced_rng.2 ?_
change Continuous
(fun x : PermutationalWreathProduct A S G =>
((permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left,
(permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right))
have hleft :
Continuous
(fun x : PermutationalWreathProduct A S G =>
(permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left) := by
refine continuous_pi ?_
intro s
simpa using α.continuous_toFun.comp
((continuous_apply s).comp continuous_permutationalWreathProduct_left)
have hright :
Continuous
(fun x : PermutationalWreathProduct A S G =>
(permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right) := by
simpa using continuous_permutationalWreathProduct_right
exact hleft.prodMk hrightFunctoriality of the permutational wreath product in the left factor, upgraded to a continuous homomorphism.
instance instMulActionRightCosetStandardEmbedding :
MulAction G (Quotient (QuotientGroup.rightRel H)) :=
rightCosetMulAction HThe right-coset standard embedding carries the natural multiplication action used in the wreath-product construction.
noncomputable def rightTransversalSection {T : Set G}
(hT : Subgroup.IsComplement (H : Set G) T) :
Quotient (QuotientGroup.rightRel H) → G :=
fun q => (hT.rightQuotientEquiv q : G)The underlying section attached to a right transversal.
@[simp] theorem rightTransversalSection_spec {T : Set G}
(hT : Subgroup.IsComplement (H : Set G) T)
(q : Quotient (QuotientGroup.rightRel H)) :
Quotient.mk'' (rightTransversalSection (H := H) hT q) = qThe chosen right-transversal section represents the prescribed right coset.
Show proof
hT.mk''_rightQuotientEquiv qProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□noncomputable def rightQuotientSectionCocycle
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q)
(g : G) :
Quotient (QuotientGroup.rightRel H) → H := by
letI := rightCosetMulAction H
intro q
refine ⟨τ q * g * (τ (g⁻¹ • q))⁻¹, ?_⟩
have hq :
Quotient.mk'' (τ q * g) = g⁻¹ • q := by
calc
Quotient.mk'' (τ q * g)
= g⁻¹ • (Quotient.mk'' (τ q) : Quotient (QuotientGroup.rightRel H)) := by
symm
rw [rightCosetMulAction_inv_mk_smul (H := H) g (τ q)]
_ = g⁻¹ • q := by rw [hτ q]
have hEq :
(Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H)) =
Quotient.mk'' (τ (g⁻¹ • q)) := by
calc
(Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H))
= g⁻¹ • q := hq
_ = Quotient.mk'' (τ (g⁻¹ • q)) := by symm; exact hτ (g⁻¹ • q)
have hrel : QuotientGroup.rightRel H (τ q * g) (τ (g⁻¹ • q)) := Quotient.exact' hEq
rw [QuotientGroup.rightRel_apply] at hrel
simpa [mul_inv_rev] using H.inv_mem hrelThe cocycle attached to a section of the right quotient by \(H\).
noncomputable def rightQuotientSectionEmbedding
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q) :
G →* PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G where
toFun g := ⟨rightQuotientSectionCocycle (H := H) τ hτ g, g⟩
map_one' := by
apply SemidirectProduct.ext
· funext q
apply Subtype.ext
simp only [rightQuotientSectionCocycle, mul_one, inv_one, one_smul, mul_inv_cancel,
SemidirectProduct.one_left, Pi.one_apply, OneMemClass.coe_one]
· rfl
map_mul' g₁ g₂ := by
apply SemidirectProduct.ext
· funext q
apply Subtype.ext
simp only [rightQuotientSectionCocycle, mul_inv_rev, mul_smul, mul_assoc, SemidirectProduct.mk_eq_inl_mul_inr,
permutationalWreathProduct_mul_left_apply, permutationalWreathProduct_inl_left_apply, SemidirectProduct.right_inl,
inv_one, one_smul, permutationalWreathProduct_inr_left_apply, SemidirectProduct.right_inr, mul_one, one_mul,
MulMemClass.mk_mul_mk, inv_mul_cancel_left]
· rflThe standard wreath-product embedding attached to a section of the right quotient by \(H\).
@[simp] theorem rightQuotientSectionEmbedding_left_apply
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q)
(g : G) (q : Quotient (QuotientGroup.rightRel H)) :
(rightQuotientSectionEmbedding (H := H) τ hτ g).left q =
rightQuotientSectionCocycle (H := H) τ hτ g qPointwise formula for the standard wreath-product embedding attached to a right-quotient section.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem rightQuotientSectionEmbedding_right
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q)
(g : G) :
(rightQuotientSectionEmbedding (H := H) τ hτ g).right = gThe right quotient section embedding lands in the right quotient component.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem rightQuotientSectionEmbedding_rightHom
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q) :
(SemidirectProduct.rightHom :
PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G →* G).comp
(rightQuotientSectionEmbedding (H := H) τ hτ) = MonoidHom.id GThe right component of the wreath-product or quotient-section map is the expected homomorphism.
Show proof
by
ext g
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem rightQuotientSectionEmbedding_injective
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q) :
Function.Injective (rightQuotientSectionEmbedding (H := H) τ hτ)The standard embedding attached to a right-quotient section is injective.
Show proof
by
intro g₁ g₂ hEq
simpa using congrArg
(fun z :
PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G => z.right) hEqProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□instance instMulActionRightCosetStandardEmbeddingTopological :
MulAction G (Quotient (QuotientGroup.rightRel H)) :=
rightCosetMulAction HThe topological right-coset standard embedding carries the natural multiplication action used in the wreath-product construction.
theorem continuous_rightQuotientSectionEmbedding
[TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
[DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
(hH : IsOpen (H : Set G))
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q)
(hτcont : Continuous τ) :
Continuous
(rightQuotientSectionEmbedding (H := H) τ hτ :
G → PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G)The right-quotient section embedding is continuous for the profinite quotient topology.
Show proof
by
refine continuous_induced_rng.2 ?_
change Continuous fun g : G =>
((rightQuotientSectionEmbedding (H := H) τ hτ g).left,
(rightQuotientSectionEmbedding (H := H) τ hτ g).right)
have hleft :
Continuous fun g : G =>
(rightQuotientSectionEmbedding (H := H) τ hτ g).left := by
refine continuous_pi ?_
intro q
refine Continuous.subtype_mk ?_ ?_
have hqcont :
Continuous fun g : G => (g⁻¹ • q : Quotient (QuotientGroup.rightRel H)) :=
continuous_rightCosetMulAction_inv_smul_of_open (G := G) H hH q
have hcont :
Continuous fun g : G => τ q * g * (τ (g⁻¹ • q))⁻¹ := by
exact (continuous_const.mul continuous_id).mul ((hτcont.comp hqcont).inv)
simpa [rightQuotientSectionEmbedding, rightQuotientSectionCocycle, mul_assoc] using hcont
have hright :
Continuous fun g : G =>
(rightQuotientSectionEmbedding (H := H) τ hτ g).right := by
simpa using (continuous_id : Continuous fun g : G => g)
exact hleft.prodMk hrightProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□def wreathLeftCoordinate
(ψ : G →* PermutationalWreathProduct A S G) (s : S) : G → A :=
fun g => (ψ g).left sThe left coordinate of an element of a wreath product is viewed as a function of the group element on the source.
theorem wreathLeftCoordinate_mul
(ψ : G →* PermutationalWreathProduct A S G)
(hψ :
(SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
MonoidHom.id G)
(s : S) (g₁ g₂ : G) :
wreathLeftCoordinate ψ s (g₁ * g₂) =
wreathLeftCoordinate ψ s g₁ *
wreathLeftCoordinate ψ (g₁⁻¹ • s) g₂The cocycle formula for the left coordinates of a homomorphism into a wreath product whose right factor is the identity.
Show proof
by
have hright : (ψ g₁).right = g₁ := by
simpa using congrArg (fun f : G →* G => f g₁) hψ
simp only [wreathLeftCoordinate, map_mul, permutationalWreathProduct_mul_left_apply, hright]Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□theorem wreathLeftCoordinate_inv
(ψ : G →* PermutationalWreathProduct A S G)
(hψ :
(SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
MonoidHom.id G)
(s : S) (g : G) :
wreathLeftCoordinate ψ s g⁻¹ =
(wreathLeftCoordinate ψ (g • s) g)⁻¹Inversion formula for the left coordinates of a homomorphism into a wreath product whose right factor is the identity.
Show proof
by
have hright : (ψ g).right = g := by
simpa using congrArg (fun f : G →* G => f g) hψ
simp only [wreathLeftCoordinate, map_inv, permutationalWreathProduct_inv_left_apply, hright]Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□instance instMulActionRightCosetCoordinateRecovery :
MulAction G (Quotient (QuotientGroup.rightRel H)) :=
rightCosetMulAction HThe coordinate-recovery map for the right-coset standard embedding is compatible with the natural multiplication action.
theorem wreathLeftCoordinate_eq_basepoint_of_rightQuotientSection
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q)
(ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
(hψ :
(SemidirectProduct.rightHom :
PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
MonoidHom.id G)
(hτpure :
∀ q : Quotient (QuotientGroup.rightRel H),
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
(g : G) (q : Quotient (QuotientGroup.rightRel H)) :
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
(rightQuotientSectionCocycle (H := H) τ hτ g q) =
wreathLeftCoordinate ψ q gBasepoint form: if a homomorphism into the wreath product has identity right factor and sends the chosen section to elements whose basepoint coordinate is trivial, then the basepoint coordinate of the induced subgroup cocycle recovers the original left coordinate.
Show proof
by
let q' : Quotient (QuotientGroup.rightRel H) := g⁻¹ • q
have hτq :
(τ q)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) = q := by
rw [rightCosetMulAction_inv_mk_smul (H := H) (τ q) 1]
simpa using hτ q
have hτq' :
τ q' • q' = (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
calc
τ q' • q' = τ q' • (Quotient.mk'' (τ q') : Quotient (QuotientGroup.rightRel H)) := by
rw [hτ q']
_ = Quotient.mk'' (1 : G) := by
rw [rightCosetMulAction_mk_smul (H := H) (τ q') (τ q')]
simp only [mul_inv_cancel]
have hinv :
wreathLeftCoordinate ψ q' (τ q')⁻¹ = 1 := by
rw [wreathLeftCoordinate_inv (ψ := ψ) hψ q' (τ q')]
simpa [hτq'] using hτpure q'
have hq' :
(Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H)) = q' := by
calc
(Quotient.mk'' (τ q * g) : Quotient (QuotientGroup.rightRel H))
= (τ q * g)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
simp only [mul_inv_rev, rightCosetMulAction_mk_smul, inv_inv, one_mul]
_ = g⁻¹ • ((τ q)⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))) := by
simp only [mul_inv_rev, mul_smul, rightCosetMulAction_mk_smul, inv_inv, one_mul]
_ = g⁻¹ • q := by rw [hτq]
_ = q' := rfl
change
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
((τ q * g) * (τ q')⁻¹) =
wreathLeftCoordinate ψ q g
rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
(τ q * g) (τ q')⁻¹]
rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
(τ q) g]
simp only [hτpure, hτq, one_mul, mul_inv_rev, rightCosetMulAction_mk_smul, inv_inv, hq', hinv, mul_one, q']Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□def rightQuotientBasepointProjectionHom
(ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
(hψ :
(SemidirectProduct.rightHom :
PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
MonoidHom.id G) :
H →* A where
toFun h :=
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) h.1
map_one' := by
simp only [wreathLeftCoordinate, OneMemClass.coe_one, map_one, SemidirectProduct.one_left, Pi.one_apply]
map_mul' a b := by
change
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
(a.1 * b.1) =
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 *
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) b.1
rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 b.1]
have ha :
a.1⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
rw [rightCosetMulAction_inv_mk_smul (H := H) a.1 1]
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
simp only [one_mul, H.inv_mem a.2]
simp only [ha]Basepoint evaluation on the stabilizer subgroup of the trivial right coset, expressed for a homomorphism into the wreath product whose right factor is the identity.
theorem rightQuotientBasepointProjectionHom_apply_cocycle
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q)
(ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
(hψ :
(SemidirectProduct.rightHom :
PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
MonoidHom.id G)
(hτpure :
∀ q : Quotient (QuotientGroup.rightRel H),
wreathLeftCoordinate ψ
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
(g : G) (q : Quotient (QuotientGroup.rightRel H)) :
rightQuotientBasepointProjectionHom (H := H) ψ hψ
(rightQuotientSectionCocycle (H := H) τ hτ g q) =
wreathLeftCoordinate ψ q gThe basepoint projection on H evaluates the section cocycle by the corresponding left coordinate, provided the chosen section has trivial basepoint coordinate.
Show proof
wreathLeftCoordinate_eq_basepoint_of_rightQuotientSection
(H := H) τ hτ ψ hψ hτpure g qProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□def wreathStabilizerProjection (s : S) :
PermutationalWreathProduct A S (MulAction.stabilizer G s) →* A where
toFun x := x.left s
map_one' := rfl
map_mul' x y := by
have hx : x.right⁻¹ • s = s := by
exact MulAction.mem_stabilizer_iff.mp x.right⁻¹.2
simp only [permutationalWreathProduct_mul_left_apply, hx]Evaluation at a fixed point is a homomorphism on the wreath product over the stabilizer of that point.
@[simp] theorem wreathStabilizerProjection_apply
(s : S) (x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
wreathStabilizerProjection (A := A) (G := G) s x = x.left sThe stabilizer projection evaluates the wreath-product function coordinate at the chosen fixed point.
Show proof
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp] theorem wreathStabilizerProjection_mapLeft
{B : Type*} [Group B]
(α : A →* B) (s : S)
(x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
wreathStabilizerProjection (A := B) (G := G) s
(permutationalWreathProductMapLeft
(S := S) (G := MulAction.stabilizer G s) α x) =
α (wreathStabilizerProjection (A := A) (G := G) s x)The stabilizer projection is natural in the left factor.
Show proof
by
rflProof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□@[simp 900] theorem rightQuotientSectionEmbedding_left_basepoint_of_mem
(τ : Quotient (QuotientGroup.rightRel H) → G)
(hτ : ∀ q, Quotient.mk'' (τ q) = q)
(hτ1 : τ (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) = 1)
{g : G} (hg : g ∈ H) :
(rightQuotientSectionEmbedding (H := H) τ hτ g).left
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
⟨g, hg⟩Basepoint form: on the subgroup \(H\), the left coordinate of the standard embedding at the trivial right coset is the given element, provided the section is normalized at the basepoint.
Show proof
by
letI := rightCosetMulAction H
apply Subtype.ext
have hq :
(g⁻¹ •
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))) =
(Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ 1]
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
simpa using hg
simp only [rightQuotientSectionEmbedding, SemidirectProduct.mk_eq_inl_mul_inr, MonoidHom.coe_mk,
OneHom.coe_mk, permutationalWreathProduct_mul_left_apply, permutationalWreathProduct_inl_left_apply,
rightQuotientSectionCocycle, hτ1, one_mul, hq, inv_one, mul_one, SemidirectProduct.right_inl, one_smul,
permutationalWreathProduct_inr_left_apply]Proof. Unfold the permutational wreath product as the function factor with the right factor acting by coordinate permutation. Multiplication, inversion, inclusions, projections, and functorial maps are computed on the function coordinate and the right coordinate separately. Continuity and compactness follow from finite products, evaluation maps on a discrete finite index set, and the continuous action; pro-\(C\) membership follows from closure under finite products and extensions.
□