Nonvanishing of idempotent images from Schur values

Generic functional evaluations of charIdempotent: any linear functional whose values on permutations are the (plain or signed) constant cycle products evaluates the idempotent to a multiple of the Schur value at the (plain or negated) constant sequence. Consequently a linear map out of the group algebra admitting such a functional cannot kill the idempotent when the Schur value is nonzero — the even and odd sectors of the dimension-bound dichotomy.

theorem RS.functional_charIdempotent (μ : YoungDiagram) (d : ℕ) (L : SymGroupAlgebra μ.card →ₗ[ℂ] ℂ) (φ : Equiv.Perm (Fin μ.card) → ℂ) (hL : ∀ (π : Equiv.Perm (Fin μ.card)), L ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin μ.card))) π) = φ π) : L (charIdempotent d (jtChar μ)) = ↑d / ↑μ.card.factorial * ∑ π : Equiv.Perm (Fin μ.card), jtChar μ π * φ π

Evaluating a linear functional on charIdempotent through its values on permutations.

theorem RS.functional_charIdempotent_frobenius (m : ℕ) (μ : YoungDiagram) (d : ℕ) (L : SymGroupAlgebra μ.card →ₗ[ℂ] ℂ) (hL : ∀ (π : Equiv.Perm (Fin μ.card)), L ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin μ.card))) π) = cycleProd (fun (x : ℕ) => ↑m) π) : L (charIdempotent d (jtChar μ)) = ↑d * diagramSchur μ fun (x : ℕ) => ↑m

The even evaluation: a functional whose permutation values are the constant cycle products evaluates the idempotent to d · s_μ(m, m, …).

theorem RS.functional_charIdempotent_signed (m : ℕ) (μ : YoungDiagram) (d : ℕ) (L : SymGroupAlgebra μ.card →ₗ[ℂ] ℂ) (hL : ∀ (π : Equiv.Perm (Fin μ.card)), L ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin μ.card))) π) = ↑↑(Equiv.Perm.sign π) * cycleProd (fun (x : ℕ) => ↑m) π) : L (charIdempotent d (jtChar μ)) = (-1) ^ μ.card * (↑d * diagramSchur μ fun (x : ℕ) => -↑m)

The odd evaluation: a functional whose permutation values are the sign-twisted constant cycle products evaluates the idempotent to (−1)^n · d · s_μ(−m, −m, …).

theorem RS.charIdempotent_image_ne_zero {M : Type u_1} [AddCommGroup M] [Module ℂ M] (m : ℕ) (μ : YoungDiagram) (d : ℕ) (hd : 0 < d) (ρ : SymGroupAlgebra μ.card →ₗ[ℂ] M) (tr : M →ₗ[ℂ] ℂ) (htr : ∀ (π : Equiv.Perm (Fin μ.card)), tr (ρ ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin μ.card))) π)) = cycleProd (fun (x : ℕ) => ↑m) π) (hSchur : (diagramSchur μ fun (x : ℕ) => ↑m) ≠ 0) : ρ (charIdempotent d (jtChar μ)) ≠ 0

Even nonvanishing: a linear map out of the group algebra admitting a trace functional with constant-cycle-product character cannot kill charIdempotent when the Schur value at the constant sequence is nonzero.

theorem RS.charIdempotent_image_ne_zero_signed {M : Type u_1} [AddCommGroup M] [Module ℂ M] (m : ℕ) (μ : YoungDiagram) (d : ℕ) (hd : 0 < d) (ρ : SymGroupAlgebra μ.card →ₗ[ℂ] M) (tr : M →ₗ[ℂ] ℂ) (htr : ∀ (π : Equiv.Perm (Fin μ.card)), tr (ρ ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin μ.card))) π)) = ↑↑(Equiv.Perm.sign π) * cycleProd (fun (x : ℕ) => ↑m) π) (hSchur : (diagramSchur μ fun (x : ℕ) => -↑m) ≠ 0) : ρ (charIdempotent d (jtChar μ)) ≠ 0

Odd nonvanishing: a linear map admitting a trace functional with sign-twisted constant-cycle-product character cannot kill charIdempotent when the Schur value at the negated constant sequence is nonzero.