Permutation wreath products

Let D be a group and let a group Q act on an index type ι. The associated permutation wreath product is the semidirect product

(ι → D) ⋊ Q,

where Q permutes the coordinates of the base group. This file defines that construction for an arbitrary action, the full wreath product with Q = Equiv.Perm ι, and the wreath product attached to a permutation subgroup Q ≤ Equiv.Perm ι.

The semidirect-product API supplies the inclusions of the base and top groups and the projection to the top group. Two natural actions are defined here. If D acts on Λ, the imprimitive action is on ι × Λ, while the product action is on ι → Λ. These constructions are kept separate; primitivity of the product action requires additional hypotheses and is not asserted here.

Main definitions

• TauCeti.PermutationWreathProduct: the wreath product (X → D) ⋊ Q attached to an arbitrary action of Q on X.
• TauCeti.WreathProduct: the full permutation wreath product (ι → D) ⋊ Equiv.Perm ι.
• TauCeti.PermSubgroupWreathProduct: the wreath product whose top group is a subgroup of Equiv.Perm ι.
• TauCeti.WreathProduct.imprimitiveToPerm: the imprimitive permutation representation on ι × Λ.
• TauCeti.WreathProduct.productToPerm: the product permutation representation on ι → Λ.

Main results

• TauCeti.WreathProduct.mem_of_inl_mulSingle_mem_of_inr_swap_mem: over a finite index type, D ≀ Sym(ι) is generated by the single-coordinate base elements and the transpositions of the top group; TauCeti.WreathProduct.mem_of_inl_mulSingle_swap_mem_of_inr_swap_mem specializes this to the hyperoctahedral group Sym(Bool) ≀ Sym(ι), generated by sign changes of single coordinates and transpositions.
• TauCeti.WreathProduct.mem_range_imprimitiveToPerm_iff: the image of Sym(Λ) ≀ Sym(ι) in Equiv.Perm (ι × Λ) consists of the permutations that permute the fibres {i} × Λ.

The convention agrees with Mathlib.GroupTheory.RegularWreathProduct: an element (a, q) acts on the base by b i ↦ b (q⁻¹ i). In the imprimitive action it sends (i, x) to (q i, a (q i) • x).

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Transactions of the American Mathematical Society 108 (1963), §§2–3.
• J. D. Dixon and B. Mortimer, Permutation Groups, §2.6.

@[reducible, inline]

abbrev TauCeti.PermutationWreathProduct (D : Type u) [Group D] (Q : Type v) [Group Q] (X : Type w) [MulAction Q X] : Type (max (max u w) v)

The permutation wreath product with base group X → D and top group Q, where Q acts on the base through Mathlib's mulAutArrow, sending f to x ↦ f (q⁻¹ • x).

Its multiplication is (f, q) * (g, r) = (fun x ↦ f x * g (q⁻¹ • x), q * r).

Equations

• TauCeti.PermutationWreathProduct D Q X = ((X → D) ⋊[mulAutArrow] Q)

@[simp]

theorem TauCeti.PermutationWreathProduct.mul_left {D : Type u} [Group D] {Q : Type v} [Group Q] {X : Type w} [MulAction Q X] (a b : PermutationWreathProduct D Q X) (x : X) : (a * b).left x = a.left x * b.left (a.right⁻¹ • x)

Multiplication in a permutation wreath product, written in base coordinates.

@[simp]

theorem TauCeti.PermutationWreathProduct.inv_left {D : Type u} [Group D] {Q : Type v} [Group Q] {X : Type w} [MulAction Q X] (a : PermutationWreathProduct D Q X) (x : X) : a⁻¹.left x = (a.left (a.right • x))⁻¹

Inversion in a permutation wreath product, written in base coordinates.

theorem TauCeti.PermutationWreathProduct.card {D : Type u} [Group D] {Q : Type v} [Group Q] {X : Type w} [MulAction Q X] [Finite X] : Nat.card (PermutationWreathProduct D Q X) = Nat.card D ^ Nat.card X * Nat.card Q

The natural cardinality of a permutation wreath product with finite index type.

@[reducible, inline]

abbrev TauCeti.WreathProduct (D : Type u) (ι : Type v) [Group D] : Type (max (max u v) v)

The full permutation wreath product of D by the symmetric group on ι. Its base group is ι → D, and its top group is Equiv.Perm ι.

Equations

• TauCeti.WreathProduct D ι = TauCeti.PermutationWreathProduct D (Equiv.Perm ι) ι

@[reducible, inline]

abbrev TauCeti.PermSubgroupWreathProduct (D : Type u) (ι : Type v) [Group D] (Q : Subgroup (Equiv.Perm ι)) : Type (max (max u v) v)

The permutation wreath product with top group restricted to Q ≤ Equiv.Perm ι.

Equations

• TauCeti.PermSubgroupWreathProduct D ι Q = TauCeti.PermutationWreathProduct D (↥Q) ι

theorem TauCeti.WreathProduct.card {D : Type u} {ι : Type v} [Group D] [Finite ι] : Nat.card (WreathProduct D ι) = Nat.card D ^ Nat.card ι * (Nat.card ι).factorial

The natural cardinality of a full permutation wreath product with finite index type.

theorem TauCeti.PermSubgroupWreathProduct.card {D : Type u} {ι : Type v} [Group D] (Q : Subgroup (Equiv.Perm ι)) [Finite ι] : Nat.card (PermSubgroupWreathProduct D ι Q) = Nat.card D ^ Nat.card ι * Nat.card ↥Q

The natural cardinality of a permutation-subgroup wreath product with finite index type.

def TauCeti.WreathProduct.emptyEquiv {D : Type u} [Group D] : WreathProduct D Empty ≃* PUnit.{u_1 + 1}

A wreath product over the empty index type is the trivial group.

Equations

• TauCeti.WreathProduct.emptyEquiv = { toFun := fun (x : TauCeti.WreathProduct D Empty) => PUnit.unit, invFun := fun (x : PUnit.{?u.1 + 1}) => 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.WreathProduct.emptyEquiv_apply {D : Type u} [Group D] (w : WreathProduct D Empty) : emptyEquiv w = PUnit.unit

@[simp]

theorem TauCeti.WreathProduct.emptyEquiv_symm_left {D : Type u} [Group D] (x : PUnit.{u_1 + 1}) : (emptyEquiv.symm x).left = 1

The inverse empty-index equivalence has trivial base component.

@[simp]

theorem TauCeti.WreathProduct.emptyEquiv_symm_right {D : Type u} [Group D] (x : PUnit.{u_1 + 1}) : (emptyEquiv.symm x).right = 1

The inverse empty-index equivalence has trivial top permutation.

def TauCeti.WreathProduct.finOneEquiv {D : Type u} [Group D] : WreathProduct D (Fin 1) ≃* D

A wreath product over a singleton index type is canonically isomorphic to its base group.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.WreathProduct.finOneEquiv_apply {D : Type u} [Group D] (w : WreathProduct D (Fin 1)) : finOneEquiv w = w.left 0

@[simp]

theorem TauCeti.WreathProduct.finOneEquiv_symm_left {D : Type u} [Group D] (d : D) : (finOneEquiv.symm d).left = fun (x : Fin 1) => d

@[simp]

theorem TauCeti.WreathProduct.finOneEquiv_symm_right {D : Type u} [Group D] (d : D) : (finOneEquiv.symm d).right = 1

The inverse singleton-index equivalence has trivial top permutation.

def TauCeti.WreathProduct.subsingletonBaseEquiv {D : Type u} {ι : Type v} [Group D] [Subsingleton D] : WreathProduct D ι ≃* Equiv.Perm ι

A wreath product with a trivial base group is canonically isomorphic to its top symmetric group.

Equations

• TauCeti.WreathProduct.subsingletonBaseEquiv = SemidirectProduct.rightHom.toMulEquiv SemidirectProduct.inr ⋯ ⋯

@[simp]

theorem TauCeti.WreathProduct.subsingletonBaseEquiv_apply {D : Type u} {ι : Type v} [Group D] [Subsingleton D] (w : WreathProduct D ι) : subsingletonBaseEquiv w = w.right

@[simp]

theorem TauCeti.WreathProduct.subsingletonBaseEquiv_symm_left {D : Type u} {ι : Type v} [Group D] [Subsingleton D] (σ : Equiv.Perm ι) : (subsingletonBaseEquiv.symm σ).left = 1

The inverse trivial-base equivalence has trivial base component.

@[simp]

theorem TauCeti.WreathProduct.subsingletonBaseEquiv_symm_right {D : Type u} {ι : Type v} [Group D] [Subsingleton D] (σ : Equiv.Perm ι) : (subsingletonBaseEquiv.symm σ).right = σ

The inverse trivial-base equivalence preserves the top permutation.

def TauCeti.WreathProduct.map {D : Type u} {ι : Type v} [Group D] {D' : Type u_1} [Group D'] (f : D →* D') : WreathProduct D ι →* WreathProduct D' ι

A group homomorphism of base groups induces a homomorphism of full permutation wreath products, acting pointwise on the base and identically on the top group.

Equations

• TauCeti.WreathProduct.map f = SemidirectProduct.map (MonoidHom.piMap fun (x : ι) => f) (MonoidHom.id (Equiv.Perm ι)) ⋯

@[simp]

theorem TauCeti.WreathProduct.map_left {D : Type u} {ι : Type v} [Group D] {D' : Type u_1} [Group D'] (f : D →* D') (w : WreathProduct D ι) (i : ι) : ((map f) w).left i = f (w.left i)

Mapping the base group acts pointwise on the base coordinates.

@[simp]

theorem TauCeti.WreathProduct.map_right {D : Type u} {ι : Type v} [Group D] {D' : Type u_1} [Group D'] (f : D →* D') (w : WreathProduct D ι) : ((map f) w).right = w.right

Mapping the base group leaves the top permutation unchanged.

@[simp]

theorem TauCeti.WreathProduct.map_id {D : Type u} {ι : Type v} [Group D] : map (MonoidHom.id D) = MonoidHom.id (WreathProduct D ι)

Mapping by the identity homomorphism is the identity on the wreath product.

@[simp]

theorem TauCeti.WreathProduct.map_comp {D : Type u} {ι : Type v} [Group D] {D' : Type u_1} [Group D'] {D'' : Type u_2} [Group D''] (g : D' →* D'') (f : D →* D') : map (g.comp f) = (map g).comp (map f)

Mapping the base group along a composite homomorphism is the composite of the induced wreath product homomorphisms.

def TauCeti.WreathProduct.congr {D : Type u} {ι : Type v} [Group D] {κ : Type w} (e : ι ≃ κ) : WreathProduct D ι ≃* WreathProduct D κ

Relabeling the index type induces an isomorphism of full permutation wreath products.

Equations

• TauCeti.WreathProduct.congr e = SemidirectProduct.congr (MulEquiv.arrowCongr e (MulEquiv.refl D)) e.permCongrHom ⋯

@[simp]

theorem TauCeti.WreathProduct.congr_left {D : Type u} {ι : Type v} [Group D] {κ : Type w} (e : ι ≃ κ) (w : WreathProduct D ι) (i : κ) : ((congr e) w).left i = w.left (e.symm i)

The base coordinates of a relabeled wreath-product element are relabeled by e.

@[simp]

theorem TauCeti.WreathProduct.congr_right {D : Type u} {ι : Type v} [Group D] {κ : Type w} (e : ι ≃ κ) (w : WreathProduct D ι) : ((congr e) w).right = e.permCongr w.right

The top permutation of a relabeled wreath-product element is conjugated by e.

@[simp]

theorem TauCeti.WreathProduct.congr_refl {D : Type u} {ι : Type v} [Group D] : congr (Equiv.refl ι) = MulEquiv.refl (WreathProduct D ι)

Relabeling by the identity equivalence is the identity isomorphism.

@[simp]

theorem TauCeti.WreathProduct.congr_trans {D : Type u} {ι : Type v} [Group D] {κ : Type w} {μ : Type u_1} (e : ι ≃ κ) (e' : κ ≃ μ) : (congr e).trans (congr e') = congr (e.trans e')

Successive relabelings compose to the relabeling by the composite equivalence.

theorem TauCeti.WreathProduct.mem_of_inl_mulSingle_mem_of_inr_swap_mem {D : Type u} {ι : Type v} [Group D] [Finite ι] [DecidableEq ι] {H : Subgroup (WreathProduct D ι)} (hbase : ∀ (i : ι) (d : D), SemidirectProduct.inl (Pi.mulSingle i d) ∈ H) (hswap : ∀ (i j : ι), i ≠ j → SemidirectProduct.inr (Equiv.swap i j) ∈ H) (w : WreathProduct D ι) : w ∈ H

Over a finite index type, D ≀ Sym(ι) is generated by the base elements supported on a single coordinate and the transpositions of the top group: a subgroup containing all of them is everything.

theorem TauCeti.WreathProduct.mem_of_inl_mulSingle_swap_mem_of_inr_swap_mem {ι : Type v} [Finite ι] [DecidableEq ι] {H : Subgroup (WreathProduct (Equiv.Perm Bool) ι)} (hsign : ∀ (i : ι), SemidirectProduct.inl (Pi.mulSingle i (Equiv.swap false true)) ∈ H) (hswap : ∀ (i j : ι), i ≠ j → SemidirectProduct.inr (Equiv.swap i j) ∈ H) (w : WreathProduct (Equiv.Perm Bool) ι) : w ∈ H

Generators of the hyperoctahedral group. Sym(Bool) ≀ Sym(ι) is generated by the sign changes of single coordinates and the transpositions of coordinates: a subgroup containing all of them is everything.

@[instance_reducible]

instance TauCeti.WreathProduct.instSMulProd (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] : SMul (WreathProduct D ι) (ι × Λ)

The scalar action underlying the imprimitive action of D ≀ Sym(ι) on ι × Λ.

Equations

• TauCeti.WreathProduct.instSMulProd D ι Λ = { smul := fun (w : TauCeti.WreathProduct D ι) (x : ι × Λ) => (w.right x.1, w.left (w.right x.1) • x.2) }

@[instance_reducible]

instance TauCeti.WreathProduct.instMulActionProd (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] : MulAction (WreathProduct D ι) (ι × Λ)

The imprimitive action of D ≀ Sym(ι) on ι × Λ. The base group acts independently inside each fibre {i} × Λ, and the top group permutes those fibres.

Equations

• TauCeti.WreathProduct.instMulActionProd D ι Λ = { toSMul := TauCeti.WreathProduct.instSMulProd D ι Λ, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem TauCeti.WreathProduct.imprimitive_smul (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] (w : WreathProduct D ι) (x : ι × Λ) : w • x = (w.right x.1, w.left (w.right x.1) • x.2)

Evaluation formula for the imprimitive wreath-product action on ι × Λ.

def TauCeti.WreathProduct.imprimitiveToPerm (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] : WreathProduct D ι →* Equiv.Perm (ι × Λ)

The permutation representation of the imprimitive wreath-product action on ι × Λ.

Equations

• TauCeti.WreathProduct.imprimitiveToPerm D ι Λ = MulAction.toPermHom (TauCeti.WreathProduct D ι) (ι × Λ)

@[simp]

theorem TauCeti.WreathProduct.imprimitiveToPerm_apply (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] (w : WreathProduct D ι) (x : ι × Λ) : ((imprimitiveToPerm D ι Λ) w) x = (w.right x.1, w.left (w.right x.1) • x.2)

The imprimitive permutation representation evaluates via the imprimitive action.

instance TauCeti.WreathProduct.instFaithfulSMulProdOfNonempty (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] [Nonempty Λ] [FaithfulSMul D Λ] : FaithfulSMul (WreathProduct D ι) (ι × Λ)

If the action of D on a nonempty Λ is faithful, then the imprimitive wreath-product action is faithful.

theorem TauCeti.WreathProduct.imprimitiveToPerm_injective (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] [Nonempty Λ] [FaithfulSMul D Λ] : Function.Injective ⇑(imprimitiveToPerm D ι Λ)

The imprimitive permutation representation is injective when the action on each nonempty fibre is faithful.

theorem TauCeti.WreathProduct.mem_range_imprimitiveToPerm_iff {ι : Type v} {Λ : Type w} {σ : Equiv.Perm (ι × Λ)} : σ ∈ (imprimitiveToPerm (Equiv.Perm Λ) ι Λ).range ↔ ∃ (τ : Equiv.Perm ι), ∀ (x : ι × Λ), (σ x).1 = τ x.1

A permutation of ι × Λ comes from the imprimitive action of Sym(Λ) ≀ Sym(ι) exactly when it permutes the fibres {i} × Λ, that is, when its first coordinate is a permutation of the first coordinate of its argument.

theorem TauCeti.WreathProduct.mem_range_imprimitiveToPerm_bool_iff {ι : Type v} {σ : Equiv.Perm (ι × Bool)} : σ ∈ (imprimitiveToPerm (Equiv.Perm Bool) ι Bool).range ↔ ∀ (x : ι × Bool), σ (x.1, !x.2) = ((σ x).1, !(σ x).2)

Signed permutations. A permutation of ι × Bool comes from the imprimitive action of the hyperoctahedral group Sym(Bool) ≀ Sym(ι) exactly when it commutes with flipping the Bool coordinate.

@[instance_reducible]

instance TauCeti.WreathProduct.instSMulForall (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] : SMul (WreathProduct D ι) (ι → Λ)

The scalar action underlying the product action of D ≀ Sym(ι) on ι → Λ.

Equations

• TauCeti.WreathProduct.instSMulForall D ι Λ = { smul := fun (w : TauCeti.WreathProduct D ι) (x : ι → Λ) (i : ι) => w.left i • x (w.right⁻¹ i) }

@[instance_reducible]

instance TauCeti.WreathProduct.instMulActionForall (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] : MulAction (WreathProduct D ι) (ι → Λ)

The product action of D ≀ Sym(ι) on ι → Λ. The top permutation rearranges the arguments, and the base group acts pointwise on the resulting values.

Equations

• TauCeti.WreathProduct.instMulActionForall D ι Λ = { toSMul := TauCeti.WreathProduct.instSMulForall D ι Λ, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem TauCeti.WreathProduct.product_smul (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] (w : WreathProduct D ι) (x : ι → Λ) (i : ι) : (w • x) i = w.left i • x (w.right⁻¹ i)

Evaluation formula for the product wreath-product action on ι → Λ.

def TauCeti.WreathProduct.productToPerm (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] : WreathProduct D ι →* Equiv.Perm (ι → Λ)

The permutation representation of the product wreath-product action on ι → Λ.

Equations

• TauCeti.WreathProduct.productToPerm D ι Λ = MulAction.toPermHom (TauCeti.WreathProduct D ι) (ι → Λ)

@[simp]

theorem TauCeti.WreathProduct.productToPerm_apply (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] (w : WreathProduct D ι) (x : ι → Λ) (i : ι) : ((productToPerm D ι Λ) w) x i = w.left i • x (w.right⁻¹ i)

The product permutation representation evaluates via the product action.

instance TauCeti.WreathProduct.instFaithfulSMulForallOfNontrivial (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] [Nontrivial Λ] [FaithfulSMul D Λ] : FaithfulSMul (WreathProduct D ι) (ι → Λ)

If D acts faithfully on a type with at least two elements, then the product wreath-product action is faithful.

theorem TauCeti.WreathProduct.productToPerm_injective (D : Type u) (ι : Type v) [Group D] (Λ : Type w) [MulAction D Λ] [Nontrivial Λ] [FaithfulSMul D Λ] : Function.Injective ⇑(productToPerm D ι Λ)

The product permutation representation is injective when the base action is faithful, the acted-on type has at least two elements.