The product action of a permutation wreath product

For g = (f, q) the action on ι → Δ is

(g • x) i = f i • x (q⁻¹ • i).

@[instance_reducible]

instance Saxl.permWreathMulAction (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] [MulAction X Δ] : MulAction (PermWreath X Q ι) (ι → Δ)

The product action of an arbitrary permutation wreath product.

Equations

• Saxl.permWreathMulAction X Q ι Δ = { smul := fun (g : Saxl.PermWreath X Q ι) (x : ι → Δ) (i : ι) => g.left i • x (g.right⁻¹ • i), mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance Saxl.permWreathDistribMulAction (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] [AddMonoid Δ] [DistribMulAction X Δ] : DistribMulAction (PermWreath X Q ι) (ι → Δ)

The product action is additive whenever the component action is additive.

Equations

• Saxl.permWreathDistribMulAction X Q ι Δ = { toMulAction := Saxl.permWreathMulAction X Q ι Δ, smul_zero := ⋯, smul_add := ⋯ }

instance Saxl.permWreathSMulCommClass (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] {F : Type u_5} [MulAction X Δ] [SMul F Δ] [SMulCommClass X F Δ] : SMulCommClass (PermWreath X Q ι) F (ι → Δ)

The product action commutes with scalars whenever the component action does.

@[simp]

theorem Saxl.permWreath_smul_apply (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] [MulAction X Δ] (g : PermWreath X Q ι) (x : ι → Δ) (i : ι) : (g • x) i = g.left i • x (g.right⁻¹ • i)

The defining coordinate formula for the product action.

theorem Saxl.one_smul_coord (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] [MulAction X Δ] (x : ι → Δ) (i : ι) : (1 • x) i = x i

Coordinate form of the identity law.

theorem Saxl.mul_smul_coord (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] [MulAction X Δ] (g h : PermWreath X Q ι) (x : ι → Δ) (i : ι) : ((g * h) • x) i = g.left i • h.left (g.right⁻¹ • i) • x (h.right⁻¹ • g.right⁻¹ • i)

Fully expanded coordinate form of the multiplication law.

theorem Saxl.base_smul_coord (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] [MulAction X Δ] (f : ι → X) (x : ι → Δ) (i : ι) : ((PermWreath.base X Q ι) f • x) i = f i • x i

A base-group element acts independently in each coordinate.

theorem Saxl.top_smul_coord (X : Type u_1) (Q : Type u_2) (ι : Type u_3) (Δ : Type u_4) [Group X] [Group Q] [MulAction Q ι] [MulAction X Δ] (q : Q) (x : ι → Δ) (i : ι) : ((PermWreath.top X Q ι) q • x) i = x (q⁻¹ • i)

A top-group element acts by reindexing the coordinates.