Library Combi.MPoly.MurnaghanNakayama: Murnaghan-Nakayama rule

The Murnaghan-Nakayama rule

See the page Murnaghan-Nakayama on Wikipedia for a statement. The fixpoint MN_coeff la mu implement the recursive version, as stated in
Theorem MN_coeff_consE la m0 mu :
  MN_coeff la (m0 :: mu) =
  \sum_(sh : 'P_(sumn mu) | ribbon sh la)
   MN_coeff sh mu * (-1) ^+ (ribbon_height sh la).-1.

and the base case
Lemma MN_coeff0 : MN_coeff [::] [::] = 1.

The Murnaghan-Nakayama rule stated in terms of symmetric polynomials is then
Theorem MN_coeffP d (la : 'P_d) :
'p[la] = \sum_(sh : 'P_d) (MN_coeff sh la)%:~R *: 's[sh] :> {sympoly R[n]}.

There is a second implementation which goes bottom up, adding ribbons instead of removing them. It allows to compute skew Murnaghan-Nakayama coefficients.

We provide the following definitions:

MN_coeff la mu == then Murnaghan-Nakayama coefficients. That is the alternating number of ribbon filling of the shape la with content mu, defined recursively.
MN_coeff_fast la mu == fast version of MN_coeff la mu
MN_coeff_rec la nu mu == The alternating number of ribbon filling of the skew shape la / nu with content mu, defined recursively.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrint perm fingroup tuple vector rat.
From mathcomp Require Import ssrcomplements freeg mpoly monalg.

Require Import sorted tools ordtype permuted partition skewpart.
Require Import antisym Schur_mpoly Schur_altdef sympoly homogsym.

Set Implicit Arguments.

#[local] Open Scope ring_scope.
Import GRing.Theory.

#[local] Reserved Notation "''a_' k"
(at level 8, k at level 2, format "''a_' k").
#[local] Reserved Notation "m # s"
(at level 40, left associativity, format "m # s").

Product of an alternating polynomial and a power sum

Section MultAlternSymp.

Variable n0 : nat.
Variable R : comRingType.

#[local] Notation n := n0.+1.
#[local] Notation rho := (rho n).
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).

Lemma mult_altern_symp_pol p d :
  'a_(mpart p + rho ) * (symp_pol n R d.+1) =
   \sum_(i < n) 'a_(mpart p + rho + U_(i) *+ d.+1).

Lemma mult_altern_oapp p d :
  is_part p -> size p <= n ->
  'a_(mpart p + rho ) * (symp_pol n R d.+1) =
  \sum_(i < n) oapp (fun ph => (-1) ^+ ph .2.-1 *: 'a_(mpart ph .1 + rho )) 0
   (add_ribbon p d i).

Lemma mult_altern_pmap p d :
  is_part p -> size p <= n ->
  'a_(mpart p + rho ) * (symp_pol n R d.+1) =
  \sum_(psh <- pmap (add_ribbon p d) (iota 0 n))
   (-1) ^+ (psh .2).-1 *: 'a_(mpart psh .1 + rho ).

End MultAlternSymp.

Product of a Schur polynomial and a power sum

Section MultSymsSympIDomain.

Variable n0 : nat.
#[local] Notation n := n0.+1.
#[local] Notation SF := {sympoly int[n ]}.

Lemma syms_sympM_oapp_int d (la : 'P_d) m :
  m != 0%N -> size la <= n ->
  's [la ] * 'p_m =
  \sum_(i < n) oapp (fun ph => (-1) ^+ ph .2.-1 *: 's [ph .1 ]) 0
   (add_ribbon_intpartn la m.-1 i) :> SF.

End MultSymsSympIDomain.

Section MultSymsSymp.

Variable n0 : nat.
Variable R : comRingType.
#[local] Notation n := n0.+1.
#[local] Notation SF := {sympoly R [n ]}.

Lemma syms_sympM_oapp d (la : 'P_d) m :
  m != 0%N ->
  's [la ] * 'p_m =
  \sum_(i < n) oapp (fun ph => (-1) ^+ ph .2.-1 *: 's [ph .1 ]) 0
   (add_ribbon_intpartn la m.-1 i) :> SF.

Lemma syms_sympM_pmap d (la : 'P_d) m :
  m != 0%N ->
  's [la ] * 'p_m =
  \sum_(ph <- pmap (add_ribbon_intpartn la m.-1) (iota 0 n))
   (-1) ^+ ph .2.-1 *: 's [ph .1 ] :> SF.

The following theorem is a step of the Murnaghan-Nakayama rule

Theorem syms_sympM d (la : 'P_d) m :
  m != 0%N ->
  's [la ] * 'p_m =
  \sum_(sh : 'P_(m + d ) | ribbon la sh)
   (-1) ^+ (ribbon_height la sh).-1 *: 's [sh ] :> SF.

End MultSymsSymp.

Murnaghan-Nakayama coefficients

We define those for any sequence of nat, but MN_coeff should only be used when sumn la == sumn mu.

Fixpoint MN_coeff (la mu : seq nat) : int :=
  if mu is m0 :: m then
    foldr (fun sh acc =>
             if ribbon sh la then
               MN_coeff sh m * (-1) ^+ (ribbon_height sh la).-1 + acc
             else acc)
          0 (enum_partn (sumn m))
  else 1.

Base case

Lemma MN_coeff0 : MN_coeff [::] [::] = 1.

Recursive step

Theorem MN_coeff_consE la m0 mu :
  MN_coeff la (m0 :: mu) =
  \sum_(sh : 'P_(sumn mu ) | ribbon sh la)
   MN_coeff sh mu * (-1) ^+ (ribbon_height sh la).-1.

Section Tests.

Tests :

sage: s(p[2,1,1])
-s[1, 1, 1, 1] - s[2, 1, 1] + s[3, 1] + s[4]

Goal ([seq x | x <- [seq (p , MN_coeff p [:: 2; 1; 1]) | p <- enum_partn 4]
               & x .2 != 0%R ] =
      [:: ([:: 4], Posz 1);
      ([:: 3; 1], Posz 1);
      ([:: 2; 1; 1], Negz 0);
      ([:: 1; 1; 1; 1], Negz 0)])%N.

Tests :

sage: s(p[4,2,1,1])
s[1, 1, 1, 1, 1, 1, 1, 1] + s[2, 1, 1, 1, 1, 1, 1] - s[3, 1, 1, 1, 1, 1]
 - 2*s[3, 3, 2] - s[4, 1, 1, 1, 1] + 2*s[4, 2, 1, 1] - s[5, 1, 1, 1]
 - s[6, 1, 1] + s[7, 1] + s[8]

Goal ([seq x | x <- [seq (p , MN_coeff p [:: 4; 2; 1; 1]) | p <- enum_partn 8]
               & x .2 != 0%R ] =
      [:: ([:: 8], Posz 1);
      ([:: 7; 1], Posz 1);
      ([:: 3; 3; 2], Negz 1);
      ([:: 6; 1; 1], Negz 0);
      ([:: 4; 2; 1; 1], Posz 2);
      ([:: 5; 1; 1; 1], Negz 0);
      ([:: 4; 1; 1; 1; 1], Negz 0);
      ([:: 3; 1; 1; 1; 1; 1], Negz 0);
      ([:: 2; 1; 1; 1; 1; 1; 1], Posz 1);
      ([:: 1; 1; 1; 1; 1; 1; 1; 1], Posz 1)])%N.

End Tests.

Murnaghan-Nakayama rule

Section MNRule.

Variable n0 : nat.
#[local] Notation n := n0.+1.

Theorem MN_coeffP_int d (la : 'P_d) :
  'p [la ] = \sum_(sh : 'P_d) MN_coeff sh la *: 's [sh ] :> {sympoly int[n ]}.

Variable R : comRingType.
#[local] Notation SF := {sympoly R [n ]}.
#[local] Notation HSF := {homsym R [n , _]}.

Theorem MN_coeffP d (la : 'P_d) :
  'p [la ] = \sum_(sh : 'P_d) (MN_coeff sh la)%:~R *: 's [sh ] :> SF.

Corollary MN_coeff_homogP d (la : 'P_d) :
  'hp [la ] = \sum_(sh : 'P_d) (MN_coeff sh la)%:~R *: 'hs [sh ] :> HSF.

End MNRule.

MN_coeff_rec should only be used when sumn la == sum nu + sumn mu.

Fixpoint MN_coeff_rec (la nu mu : seq nat) : int :=
  if mu is m0 :: m then
    foldr (fun psh acc =>
             MN_coeff_rec la psh .1 m * (-1) ^+ psh .2.-1 + acc)
          0
          [seq psh | psh <- pmap (add_ribbon nu m0.-1) (iota 0 (size la))
                   & included psh .1 la]
  else (la == nu).
Definition MN_coeff_fast la mu := MN_coeff_rec la [::] mu.

Lemma MN_coeff_rec_szE la nu m0 mu :
  MN_coeff_rec la nu (m0 :: mu) =
  \sum_(psh <- pmap (add_ribbon nu m0.-1) (iota 0 (size la))
       | included psh .1 la)
   MN_coeff_rec la psh .1 mu * (-1) ^+ psh .2.-1.

Lemma MN_coeff_rec_notincl la nu mu :
  0%N \notin mu -> is_part nu -> ~~ included nu la ->
  MN_coeff_rec la nu mu = 0.

Lemma MN_coeff_rec_consE n la nu m0 mu :
  m0 != 0%N -> size la <= n ->
  MN_coeff_rec la nu (m0 :: mu) =
  \sum_(psh <- pmap (add_ribbon nu m0.-1) (iota 0 n) | included psh .1 la)
   MN_coeff_rec la psh .1 mu * (-1) ^+ psh .2.-1.

Section Tests.

Tests :

sage: s(p[3, 3, 1, 1]).coefficient([5, 2, 1])
-2

Goal MN_coeff_fast [:: 5; 2; 1]%N [:: 3; 3; 1; 1]%N = - 2%:R.

Tests :

sage: s(p[5, 2, 1]).coefficient([3, 3, 1, 1])
1

Goal MN_coeff_fast [:: 3; 3; 1; 1]%N [:: 5; 2; 1]%N = 1%:R.

Tests :

sage: s(p[6, 5, 5, 4, 2, 1]).coefficient([12, 5, 2, 2, 1, 1])
4

Goal MN_coeff_fast [:: 12; 5; 2; 2; 1; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = 4%:R.

Tests :

sage: s(p[6, 5, 5, 4, 2, 1]).coefficient([12, 5, 3, 1, 1, 1])
-2

Goal MN_coeff_fast [:: 12; 5; 3; 1; 1; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = - 2%:R.
Goal MN_coeff_fast [:: 12; 5; 3; 2; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = - 3%:R.
Goal MN_coeff_fast [:: 12; 5; 4; 1; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = 2%:R.
Goal MN_coeff_fast [:: 12; 5; 4; 2]%N [:: 6; 5; 5; 4; 2; 1]%N = 4%:R.

End Tests.

Section FastImplem.

Variable n0 : nat.
#[local] Notation n := n0.+1.

Lemma syms_prod_sympM_int dn (nu : 'P_dn) dm (mu : 'P_dm) :
  's [nu ] * 'p [mu ] =
  \sum_(la : 'P_(dn + dm )) MN_coeff_rec la nu mu *: 's [la ] :> {sympoly int[n ]}.

Section ComRing.

Variable R : comRingType.
#[local] Notation SF := {sympoly R [n ]}.
#[local] Notation HSF := {homsym R [n , _]}.

Theorem syms_prod_sympM dn (nu : 'P_dn) dm (mu : 'P_dm) :
  's [nu ] * 'p [mu ] =
  \sum_(la : 'P_(dn + dm )) (MN_coeff_rec la nu mu)%:~R *: 's [la ] :> SF.

Corollary homsyms_homsympM dn (nu : 'P_dn) dm (mu : 'P_dm) :
  'hs [nu ] *h 'hp [mu ] =
  \sum_(la : 'P_(dn + dm )) (MN_coeff_rec la nu mu)%:~R *: 'hs [la ] :> HSF.

Corollary MN_coeff_recP d (la : 'P_d) :
  'p [la ] = \sum_(sh : 'P_d) (MN_coeff_fast sh la)%:~R *: 's [sh ] :> SF.

Corollary MN_coeff_rec_homogP d (la : 'P_d) :
  'hp [la ] = \sum_(sh : 'P_d) (MN_coeff_fast sh la)%:~R *: 'hs [sh ] :> HSF.

End ComRing.

End FastImplem.

The two implementations coincide

Corollary MN_coeffE d (la mu : 'P_d) : MN_coeff_fast la mu = MN_coeff la mu.