The tensor-space permutation representation and its character

The symmetric group Equiv.Perm (Fin n) acts on the full function space Fin n → Fin m by precomposition with the inverse. This is the tensor space (ℂ^m)^{⊗n} in its basis-indexed form. The character of the induced representation equals the completed cycle-type product at the constant sequence fun _ => (m : ℂ).

The permutation action on the full function space

@[instance_reducible]

instance RS.tensorAction (n m : ℕ) : MulAction (Equiv.Perm (Fin n)) (Fin n → Fin m)

The symmetric group acts on Fin n → Fin m by precomposition with the inverse permutation.

Equations

• RS.tensorAction n m = { smul := fun (π : Equiv.Perm (Fin n)) (g : Fin n → Fin m) => g ∘ ⇑π⁻¹, mul_smul := ⋯, one_smul := ⋯ }

cycleProd at the constant sequence