Polynomial commutant bounds for monomial word actions

Matrix entries of an intertwiner are determined, up to nonzero scalars, by the simultaneous permutation orbits of pairs of words. Such an orbit is determined by its letter-pair counts. Each count lies between zero and the word length, giving the polynomial bound (n + 1) ^ (Fintype.card α ^ 2).

structure RS.MonomialWordAction {α : Type u_1} {n : ℕ} (ρ : Representation ℂ (Equiv.Perm (Fin n)) ((Fin n → α) → ℂ)) : Type u_1

Coordinates of a symmetric-group representation acting on words by permutation of positions and multiplication by nonzero scalars.

• weight : Equiv.Perm (Fin n) → (Fin n → α) → ℂ

  The scalar attached to a permutation and an output word.

• weight_ne_zero (σ : Equiv.Perm (Fin n)) (c : Fin n → α) : self.weight σ c ≠ 0

  Every coordinate scalar is nonzero.

• apply_eq (σ : Equiv.Perm (Fin n)) (v : (Fin n → α) → ℂ) (c : Fin n → α) : (ρ σ) v c = self.weight σ c * v (c ∘ ⇑σ)

  The action reindexes coordinates by the permutation.

theorem RS.finrank_commutant_le_word_counts {α : Type u_1} {n : ℕ} [Fintype α] {ρ : Representation ℂ (Equiv.Perm (Fin n)) ((Fin n → α) → ℂ)} (M : MonomialWordAction ρ) : Module.finrank ℂ (ρ.IntertwiningMap ρ) ≤ (n + 1) ^ Fintype.card α ^ 2

The commutant of a monomial word action has polynomial dimension, with one possible coordinate for each table of letter-pair counts.