Permutation wreath products

This file defines the wreath product attached to an arbitrary action of a top group on an index type. The top group acts on the base group by contravariant reindexing, so that

(reindexAut X Q ι q f) i = f (q⁻¹ • i).

Unlike RegularWreathProduct, the action of Q on ι need not be regular.

def Saxl.reindexAut (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] : Q →* MulAut (ι → X)

The action of Q on the base group ι → X by contravariant reindexing.

Equations

• Saxl.reindexAut X Q ι = { toFun := fun (q : Q) => MulEquiv.arrowCongr (MulAction.toPerm q) (MulEquiv.refl X), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Saxl.reindexAut_apply (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] (q : Q) (f : ι → X) (i : ι) : ((reindexAut X Q ι) q) f i = f (q⁻¹ • i)

@[reducible, inline]

abbrev Saxl.PermWreath (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] : Type (max (max u_1 u_3) u_2)

The permutation wreath product X wr_ι Q, with base group ι → X and the specified action of Q on ι.

Equations

• Saxl.PermWreath X Q ι = ((ι → X) ⋊[Saxl.reindexAut X Q ι] Q)

def Saxl.PermWreath.base (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] : (ι → X) →* PermWreath X Q ι

The canonical inclusion of the base group into the permutation wreath product.

Equations

• Saxl.PermWreath.base X Q ι = SemidirectProduct.inl

def Saxl.PermWreath.top (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] : Q →* PermWreath X Q ι

The canonical inclusion of the top group into the permutation wreath product.

Equations

• Saxl.PermWreath.top X Q ι = SemidirectProduct.inr

@[simp]

theorem Saxl.PermWreath.base_left (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] (f : ι → X) : ((base X Q ι) f).left = f

@[simp]

theorem Saxl.PermWreath.base_right (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] (f : ι → X) : ((base X Q ι) f).right = 1

@[simp]

theorem Saxl.PermWreath.top_left (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] (q : Q) : ((top X Q ι) q).left = 1

@[simp]

theorem Saxl.PermWreath.top_right (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] (q : Q) : ((top X Q ι) q).right = q

theorem Saxl.PermWreath.ext (X : Type u_1) (Q : Type u_2) (ι : Type u_3) [Group X] [Group Q] [MulAction Q ι] {g h : PermWreath X Q ι} (hbase : g.left = h.left) (htop : g.right = h.right) : g = h

Extensionality in the base and top coordinates.