Documentation

TauCeti.RingTheory.MvPolynomial.Symmetric.Schur.MurnaghanNakayama

The Murnaghan–Nakayama rule for Schur polynomials #

Multiplying a Schur polynomial by a power sum adds rim hooks: for r > 0,

p_r · s_ν = ∑_μ (-1) ^ ht(μ / ν) · s_μ,

the sum running over the diagrams μ for which μ / ν is a rim hook with r cells, and ht(μ / ν), one less than the number of rows the hook meets, being its height. This is TauCeti.psum_mul_diagramSchurPoly for Young diagrams in the alphabet Fin N, and TauCeti.psum_mul_schurPoly for partitions in an arbitrary finite alphabet. Iterating it from s_∅ = 1 along the parts of a partition ρ expands the power-sum product p_ρ in Schur polynomials; that expansion is the combinatorial half of the Murnaghan–Nakayama rule for the characters of the symmetric groups, whose other half is Frobenius's formula identifying the coefficients with character values.

Main statements #

References #

theorem TauCeti.psum_mul_alternant_betaNumber {R : Type u_1} [CommRing R] {N : ℕ} (ν : YoungDiagram) (hν : ν.colLen 0 ≤ N) {r : ℕ} (hr : 0 < r) :
(MvPolynomial.psum (Fin N) R r * alternant (Fin N) R fun (j : Fin N) => ν.betaNumber N ↑j) = ∑ μ : (ν.card + r).Partition with (diagramOf μ).IsRimHook ν ∧ (diagramOf μ).colLen 0 ≤ N, (-1) ^ (diagramOf μ).rimHookHeight ν * alternant (Fin N) R fun (j : Fin N) => (diagramOf μ).betaNumber N ↑j

The Murnaghan–Nakayama rule for alternants. Let ν be a Young diagram with at most N rows and β its beta-numbers relative to N, so that a_β = s_ν · a_δ. For r > 0, multiplying a_β by the power sum p_r gives the signed sum of the alternants of the beta-numbers of the diagrams μ with at most N rows for which μ / ν is a rim hook with r cells, each weighted by (-1) to the height of its rim hook.

theorem TauCeti.psum_mul_diagramSchurPoly {R : Type u_1} [CommRing R] {N : ℕ} (ν : YoungDiagram) {r : ℕ} (hr : 0 < r) :
MvPolynomial.psum (Fin N) R r * diagramSchurPoly N R ν = ∑ μ : (ν.card + r).Partition with (diagramOf μ).IsRimHook ν, (-1) ^ (diagramOf μ).rimHookHeight ν * diagramSchurPoly N R (diagramOf μ)

The Murnaghan–Nakayama rule for Schur polynomials. For r > 0, multiplying the Schur polynomial of a Young diagram ν in the alphabet Fin N by the power sum p_r gives the signed sum of the Schur polynomials of the diagrams μ for which μ / ν is a rim hook with r cells, each weighted by (-1) to the height of its rim hook: p_r · s_ν = ∑_μ (-1) ^ ht(μ / ν) · s_μ. No bound on the number of rows is needed: the Schur polynomials of the diagrams with more than N rows vanish on both sides.

theorem TauCeti.psum_mul_schurPoly {R : Type u_1} [CommRing R] {σ : Type u_2} [Fintype σ] {n : ℕ} (ν : n.Partition) {r : ℕ} (hr : 0 < r) :
MvPolynomial.psum σ R r * schurPoly σ R ν = ∑ μ : (n + r).Partition with (diagramOf μ).IsRimHook (diagramOf ν), (-1) ^ (diagramOf μ).rimHookHeight (diagramOf ν) * schurPoly σ R μ

The Murnaghan–Nakayama rule for Schur polynomials of partitions. In a finite alphabet σ, for a partition ν of n and r > 0, p_r · s_ν = ∑_μ (-1) ^ ht(μ / ν) · s_μ, the sum running over the partitions μ of n + r whose Young diagram contains that of ν with a rim hook as complement, ht being the height of that rim hook.