Irreducibility of permutation-wreath product actions

Let a group H act linearly on an F-module V, and let a group Q act transitively on a nonempty finite type ι. This file proves that the product action of H wr_ι Q on ι → V is irreducible when the component action is irreducible and nontrivial.

Here nontriviality of the action is recorded by MovesNonzero H V: every nonzero component vector is moved by some element of H. For an irreducible module this follows as soon as the action itself is nontrivial; in particular, it follows from faithfulness and Nontrivial H.

The proof is computation-free. Starting with a nonzero vector in an invariant subspace, subtracting a base-group translate isolates one coordinate. The component irreducibility fills that coordinate, top transitivity transports it to every coordinate, and the finite sum of coordinate vectors fills the whole product module.

def Saxl.MovesNonzero (H : Type u_6) (V : Type u_7) [Zero V] [SMul H V] : Prop

Every nonzero vector is moved by some group element. This is the exact nontriviality condition used by the coordinate-isolation argument.

Equations

• Saxl.MovesNonzero H V = ∀ (v : V), v ≠ 0 → ∃ (h : H), h • v ≠ v

theorem Saxl.movesNonzero_of_irreducible {F : Type u_1} {H : Type u_2} {V : Type u_5} [Field F] [Group H] [AddCommGroup V] [Module F V] [DistribMulAction H V] [SMulCommClass H F V] (hirr : (Representation.ofDistribMulAction F H V).IsIrreducible) (hnontrivial : ∃ (h : H) (v : V), h • v ≠ v) : MovesNonzero H V

For an irreducible module, one moved vector implies that every nonzero vector is moved.

theorem Saxl.movesNonzero_of_irreducible_faithful {F : Type u_1} {H : Type u_2} {V : Type u_5} [Field F] [Group H] [AddCommGroup V] [Module F V] [DistribMulAction H V] [SMulCommClass H F V] [Nontrivial H] [FaithfulSMul H V] (hirr : (Representation.ofDistribMulAction F H V).IsIrreducible) : MovesNonzero H V

A faithful irreducible action of a nontrivial group moves every nonzero vector.

theorem Saxl.PermWreath.movesNonzero {H : Type u_2} {Q : Type u_3} {ι : Type u_4} {V : Type u_5} [Group H] [Group Q] [MulAction Q ι] [AddCommGroup V] [DistribMulAction H V] (hmove : MovesNonzero H V) : MovesNonzero (PermWreath H Q ι) (ι → V)

The coordinate-moving condition passes from a component action to its permutation-wreath product action.

theorem Saxl.PermWreath.isIrreducible_of_movesNonzero {F : Type u_1} {H : Type u_2} {Q : Type u_3} {ι : Type u_4} {V : Type u_5} [Field F] [Group H] [Group Q] [MulAction Q ι] [AddCommGroup V] [Module F V] [DistribMulAction H V] [SMulCommClass H F V] [Finite ι] [Nonempty ι] [Nontrivial V] (hcomponent : (Representation.ofDistribMulAction F H V).IsIrreducible) (hmove : MovesNonzero H V) (htop : MulAction.IsPretransitive Q ι) : (Representation.ofDistribMulAction F (PermWreath H Q ι) (ι → V)).IsIrreducible

A finite transitive permutation wreath product of an irreducible component that moves every nonzero vector is irreducible in its product action.

theorem Saxl.PermWreath.isIrreducible_of_faithful {F : Type u_1} {H : Type u_2} {Q : Type u_3} {ι : Type u_4} {V : Type u_5} [Field F] [Group H] [Group Q] [MulAction Q ι] [AddCommGroup V] [Module F V] [DistribMulAction H V] [SMulCommClass H F V] [Finite ι] [Nonempty ι] [Nontrivial H] [Nontrivial V] [FaithfulSMul H V] (hcomponent : (Representation.ofDistribMulAction F H V).IsIrreducible) (htop : MulAction.IsPretransitive Q ι) : (Representation.ofDistribMulAction F (PermWreath H Q ι) (ι → V)).IsIrreducible

Faithful-action form of isIrreducible_of_movesNonzero.