Library Combi.SymGroup.Frobenius_char: Frobenius characteristic

Frobenius / Schur character theory for the symmetric groups.

We develop the theory of Frobenius characteristic associated to a class function of 'SG_n, it is an isometry from class function to symmetric functions, mapping

1%g to 'HH[rowpartn n] (this is Fchar_triv);
1z_l to 'hpl (this is Fchar_ncfuniCT);
induction product to product Fchar_ind_morph;
omega involution to multiplication by the sign character omega_Fchar.

We define the following notions and notations:

Fchar f == the Frobenius characteristic of the class function f. the number of variable is inferred from the context.
Fchar_inv f == the inverse Frobenius characteristic of the homogeneous symmetric polynomial f.
'M[la] == the Young character for 'SG_n associated to the partition la of n. If la = (l1, ..., lk) it is the character induced from the trivial representations of the group 'SG_l1 * ... * SG_lk.
'irrSG[la] == the irreducible character for 'SG_n associated to the partition la of n.

Here is a list of fundamental results:

Fchar_isometry : The Frobenius characteristic is an isometry.
Young_rule : The Young rule for character of 'SG_n.
irrSGP : The 'irrSG[la] | la : 'P_n forms a complete set of irreducible characters for 'SG_n.
Frobenius_char : Frobenius character formula for 'SG_n.
Murnaghan_Nakayama_char : Murnaghan-Nakayama character formula for 'SG_n.
dim_cfReprSG : the dimension of irreducible representation of 'SG_n.
LR_rule_irrSG : Littlewood-Richardson rule for characters of 'SG_n.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import fingroup perm morphism gproduct.
From mathcomp Require Import rat ssralg ssrint ssrnum algC vector archimedean.
From mathcomp Require Import mxrepresentation classfun character.
From mathcomp Require Import mpoly.

Require Import sorted ordtype tools partition antisym sympoly homogsym Cauchy
        Schur_altdef stdtab therule.
Require Import permcomp cycletype towerSn permcent reprSn unitriginv.
Require Import MurnaghanNakayama.

Require ordtype.

Set Implicit Arguments.

Import LeqGeqOrder.
Import GroupScope GRing.Theory Num.Theory.
Open Scope ring_scope.

Reserved Notation "''irrSG[' l ']'"
         (at level 8, l at level 2, format "''irrSG[' l ]").
Reserved Notation "''M[' l ']'"
         (at level 8, l at level 2, format "''M[' l ]").

#[local] Lemma char0_rat : [char rat] =i pred0.
#[local] Lemma char0_algC : [char algC] =i pred0.
#[local] Hint Resolve char0_algC char0_rat : core.

Definition and basic properties

Section NVar.

Variable nvar0 : nat.
#[local] Notation nvar := nvar0.+1.

Section Defs.

Variable n : nat.
#[local] Notation HS := {homsym algC[nvar , n ]}.

Definition Fchar (f : 'CF('SG_n)) : HS :=
  locked (\sum_(la : 'P_n) (f (permCT la) / 'z_la) *: 'hp [la ]).

Definition Fchar_inv (p : HS) : 'CF('SG_n) :=
  locked (\sum_(la : 'P_n) (coord 'hp (enum_rank la) p) *: '1 z_[la ]).

Lemma FcharE (f : 'CF('SG_n)) :
  Fchar f = \sum_(la : 'P_n) (f (permCT la) / 'z_la) *: 'hp [la ].

Lemma Fchar_invE (p : HS) :
  Fchar_inv p = \sum_(la : 'P_n) (coord 'hp (enum_rank la) p) *: '1 z_[la ].

Lemma Fchar_is_linear : linear Fchar.

Lemma Fchar_ncfuniCT (l : 'P_n) : Fchar '1 z_[l ] = 'hp [l ].

Lemma Fchar_inv_is_linear : linear Fchar_inv.

Hypothesis Hn : (n <= nvar)%N.

Lemma FcharK : cancel Fchar Fchar_inv.

Lemma Fchar_invK : cancel Fchar_inv Fchar.

Lemma Fchar_triv : Fchar 1 = 'hh [rowpartn n ].

Lemma Fchar_inv_homsymp (l : 'P_n) : Fchar_inv 'hp [l ] = '1 z_[l ].

Frobenius Characteristic and omega involution

Lemma omega_Fchar_inv (p : HS) :
Fchar_inv (omegahomsym p) = sign_char * (Fchar_inv p).

Lemma omega_Fchar f : omegahomsym (Fchar f) = Fchar (sign_char * f).

Lemma Fchar_sign : Fchar sign_char = 'he [rowpartn n ].

The Frobenius Characteristic is an isometry

Theorem Fchar_isometry f g : '[Fchar f | Fchar g ] = '[f, g].

Theorem Fchar_inv_isometry p q : '[Fchar_inv p, Fchar_inv q] = '[p | q ].

End Defs.

The Frobenius Characteristic is a graded ring morphism

This cannot be written as a SSReflect {morph Fchar : f g / ... >-> ... } because the dependency of Fchar on the degree n. The three Fchar below are actually three different functions.

Note: this can be solved using a dependant record {n; 'CF('S_n)} with a dependent equality but I'm not sure this is really needed.

Theorem Fchar_ind_morph m n (f : 'CF('SG_m)) (g : 'CF('SG_n)) :
Fchar ('Ind['SG_(m + n )] (f \o^ g)) = Fchar f *h Fchar g.

Combinatorics of characters of the symmetric groups

Young characters and Young Rule

Section Character.

Import LeqGeqOrder.

Variable n : nat.
Hypothesis Hn : (n <= nvar)%N.
#[local] Notation HS := {homsym algC[nvar , n ]}.

Lemma homsymh_character (la : 'P_n) : Fchar_inv 'hh [la ] \is a character.

Lemma homsyme_character (la : 'P_n) : Fchar_inv 'he [la ] \is a character.

End Character.

End NVar.
#[local] Hint Resolve leqSpred : core.

Arguments Fchar nvar0 [n] f.
Arguments Fchar_inv nvar0 [n] p.

Lemma FcharNvar (nvar0 nvar1 n : nat) (f : 'CF('SG_n)) :
  (n <= nvar0.+1)%N || (nvar1 < nvar0.+1)%N ->
  cnvarhomsym nvar1 (Fchar nvar0 f) = (Fchar nvar1 f ).

Section YoungIrrDef.

Variable (n : nat).
Implicit Type (la mu : 'P_n).

Definition YoungSG la : 'CF('SG_n) := Fchar_inv (n.-1) 'hh [la ].
Definition irrSG la : 'CF('SG_n) := Fchar_inv (n.-1) 'hs [la ].

Notation "''M[' l ']'" := (YoungSG l).
Notation "''irrSG[' l ']'" := (irrSG l).

Lemma Fchar_irrSGE nvar0 la : Fchar nvar0 'irrSG [la ] = 'hs [la ].

Lemma Young_char la : 'M [la ] \is a character.

Lemma Young_rule la : 'M [la ] = \sum_(mu : 'P_n) 'K (mu , la ) *: 'irrSG [mu ].

Lemma Young_rule_partdom la :
  'M [la ] =
  'irrSG [la ] + \sum_(mu | (la < mu :> 'PDom_n)%O) 'K (mu , la ) *: 'irrSG [mu ].

Irreducible character

Substracting characters

Lemma rem_irr1 (xi phi : 'CF('SG_n)) :
  xi \in irr 'SG_n -> phi \is a character -> '[phi, xi] != 0 ->
     phi - xi \is a character.

Lemma rem_irr (xi phi : 'CF('SG_n)) :
  xi \in irr 'SG_n -> phi \is a character ->
     phi - '[phi, xi] *: xi \is a character.

Lemma irrSG_orthonormal la mu :
  '['irrSG [la ], 'irrSG [mu ]] = (la == mu)%:R.

Theorem irrSG_irr la : 'irrSG [la ] \in irr 'SG_n.

The 'irrSG[la] forms a complete set of irreducible character

Theorem irrSGP : perm_eq [seq 'irrSG [la ] | la : 'P_n] (irr 'SG_n).

Frobenius character formula for 'SG_n

The value of the irreducible character 'irrSG[la] using scalar product of symmetric function

Theorem Frobenius_char_homsymdot la (sigma : 'S_n) :
  'irrSG [la ] sigma = '[ 'hs [la ] | 'hp [cycle_typeSn sigma ] ] _(n.-1, n ).

Theorem Frobenius_char_coord la (sigma : 'S_n) :
  'irrSG [la ] sigma =
  coord 'hs (enum_rank la) ('hp [cycle_typeSn sigma ] : {homsym algC[n.-1.+1, n ]}).

End YoungIrrDef.
Notation "''M[' l ']'" := (YoungSG l).
Notation "''irrSG[' l ']'" := (irrSG l).

Frobenius character formula for 'SG_n

Theorem Frobenius_char n (la mu : 'P_n) :
'irrSG [la ] (permCT mu ) =
(Vanprod * \prod_(d <- mu) (symp_pol n algC d))@_(mpart la + rho n).

The Murnaghan Nakayama rule for irreducible character 'irrSG[la]

Theorem Murnaghan_Nakayama_char n la (sigma : 'S_n) :
  'irrSG [la ] sigma = (MN_coeff la (cycle_typeSn sigma))%:~R.
Corollary Murnaghan_NakayamaCT n (la mu : 'P_n) :
  'irrSG [la ] (permCT mu ) = (MN_coeff la mu)%:~R.

Corollary irrSG_char_int n (la mu : 'P_n) : 'irrSG [la ] (permCT mu ) \in Num.int.

Example Wikipedia_Murnaghan_Nakayama :
  let p521 := @IntPartN 8 [:: 5; 2; 1]%N is_true_true in
  let p3311 := @IntPartN 8 [:: 3; 3; 1; 1]%N is_true_true in
  'irrSG [p521 ] (permCT p3311 ) = - 2%:~R.

The dimension of the irreducible character 'irrSG[la] is the number of standard tableau of shape la

Theorem dim_irrSG n (la : 'P_n) : 'irrSG [la ] 1%g = #|{: stdtabsh la }|%:R.

Theorem dim_cfReprSG n (la : 'P_n) d (rG : mx_representation algC 'SG_n d) :
cfRepr rG = 'irrSG [la ] -> d = #|{: stdtabsh la }|.

Littlewood-Richardson rule for irreducible characters

Theorem LR_rule_irrSG c d (la : 'P_c) (mu : 'P_d) :
'Ind['SG_(c + d )] ('irrSG[la] \o^ 'irrSG[mu]) =
\sum_(nu : 'P_(c + d ) | included la nu) 'irrSG [nu ] *+ LRyam_coeff la mu nu.