Primitivity of the two actions of a wreath product

The permutation wreath product D ≀ Sym(ι) has two natural actions, with opposite behaviour.

The imprimitive action on ι × Λ is never primitive once ι and Λ each have at least two points: every fibre {i} × Λ is a block, and such a fibre is neither a single point nor the whole space. This is the block structure that gives the action its name.

For the product action on ι → Λ, let the group D act faithfully and primitively, but not regularly, on a nontrivial type Λ. When ι is finite, D ≀ Sym(ι) acts primitively on the function space ι → Λ. The nonregularity hypothesis is essential. It provides a nontrivial stabilizer of a base point; primitivity and faithfulness then say that this stabilizer moves every other point. Applied in a single coordinate, such an element turns any nonsingleton block containing a constant function into a block containing a pair that differs in only one coordinate. Primitivity of the D-action then fills that coordinate, symmetry fills every coordinate, and the base group fills the whole function space.

Main results

• TauCeti.WreathProduct.isBlock_fst_preimage_singleton: each fibre {i} × Λ is a block for the imprimitive action.
• TauCeti.WreathProduct.not_isPreprimitive_imprimitive: the imprimitive action of D ≀ Sym(ι) on ι × Λ is not primitive when ι and Λ are nontrivial.
• TauCeti.WreathProduct.isPreprimitive_product: the product action of D ≀ Sym(ι) is primitive when the action of D is faithful, primitive, and nonregular.

References

• J. D. Dixon and B. Mortimer, Permutation Groups, Theorem 2.7A.

The imprimitive action

theorem TauCeti.WreathProduct.isBlock_fst_preimage_singleton {D : Type u} {ι : Type v} {Λ : Type w} [Group D] [MulAction D Λ] (i : ι) : MulAction.IsBlock (WreathProduct D ι) (Prod.fst ⁻¹' {i})

Each fibre {i} × Λ is a block for the imprimitive action of D ≀ Sym(ι) on ι × Λ.

theorem TauCeti.WreathProduct.not_isPreprimitive_imprimitive {D : Type u} {ι : Type v} {Λ : Type w} [Group D] [MulAction D Λ] [Nontrivial ι] [Nontrivial Λ] : ¬MulAction.IsPreprimitive (WreathProduct D ι) (ι × Λ)

The imprimitive action is not primitive. When there are at least two fibres with at least two points each, a fibre {i} × Λ is a block that is neither a subsingleton nor the whole space.

The product action

theorem TauCeti.WreathProduct.isPreprimitive_product {D : Type u} {ι : Type v} {Λ : Type w} [Group D] [MulAction D Λ] [Finite ι] [Nontrivial Λ] [FaithfulSMul D Λ] [MulAction.IsPreprimitive D Λ] (hnotRegular : ¬IsCancelSMul D Λ) : MulAction.IsPreprimitive (WreathProduct D ι) (ι → Λ)

The product action of a full permutation wreath product is primitive when its base action is faithful and primitive but not regular.

Here nonregularity is expressed as failure of IsCancelSMul: for a pretransitive action, IsCancelSMul D Λ says exactly that every point stabilizer is trivial. The hypotheses imply the usual lower bound of three on the size of a finite Λ; stating the theorem this way also covers infinite primitive actions.