Library Combi.MPoly.Cauchy: Cauchy formula for symmetric polynomials

Cauchy formula for symmetric polynomials

In this file we fix two non zero natural m and n and consider the two sets of variables X := (x_i)_{i < m} and Y := (y_j)_{j < n}. We also consider the variables z_{i,j} := x_i * y_j.

We encode polynomial in X \cup Y as polynomials in X whose coefficient are polynomials in Y. We denote by mz a monomial in the Z.

monX mz == the monomial in X obtained by setting all the y_i to 1.
monsY mz == the m.-tuple of whose i-th element is the monomial in Y obtained by putting x_i to 1 and all the others to 0.
Ymon ms == given ms : m.-tuple 'X_{1.. n} assemble them to get a monomial in the Z.
polXY m n R == polynomial in m variable whose coefficients are polynomials in n over the commutative ring R. This is canonically a algType over R.
polXY_scale c p == base ring multiplication for elements of polXY m n R
p(X) == the image of p by the canonical inclusion algebra morphism polX -> polXY
p(Y) == the image of p by the canonical inclusion algebra morphism polY -> polXY
p(XY) == the polynomial in polXY from a polynomials in the Z_{i,j}.
Cauchy_kernel d == the Cauchy reproducing kernel in degree d, that is the sum of all monomial in x_i*y_i of degree d which is defined as 'h_d(XY)
co_hp la p == if p is symmetric in X, returns the coefficient of p on 'hp[la]
co_hpXY la mu p == if p is symmetric both in X and Y, returns the coefficient of p on 'hp[la](X) 'hp[mu](Y).

The main result is Theorem homsymdotss which asserts that Schur function are orthonormal for the scalar product.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssrint rat ssralg ssrnum algC matrix vector.
From mathcomp Require Import mpoly.

Require Import tools partition ordtype.
Require Import antisym Schur_mpoly Schur_altdef sympoly homogsym permcent.

Require ordtype.

Set Implicit Arguments.

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

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

Reserved Notation "p '(Y)'" (at level 20, format "p '(Y)'").
Reserved Notation "p '(X)'" (at level 20, format "p '(X)'").
Reserved Notation "p '(XY)'" (at level 20, format "p '(XY)'").

Polynomials in two sets of variables

Section CauchyKernel.

Variables (m0 n0 : nat).
Notation m := m0.+1.
Notation n := n0.+1.
Notation mxvec_index := (@mxvec_index m n).

Let vecmx_index : 'I_(m * n) -> 'I_m * 'I_n :=
  (enum_val \o cast_ord (esym (mxvec_cast m n))).

Lemma vecmx_indexK i : mxvec_index (vecmx_index i ).1 (vecmx_index i ).2 = i.
Lemma mxvec_indexK i j : vecmx_index (mxvec_index i j) = (i , j ).

Section Big.

Variables (R : Type) (idx : R).
Variable op : Monoid.com_law idx.

Lemma big_mxvec_index P F :
  \big[op/idx]_(i : 'I_(m * n) | P i) F i =
   \big[op/idx]_(i < m)
    \big[op/idx]_(j < n | P (mxvec_index i j)) F (mxvec_index i j).

End Big.

Definition monX (mon : 'X_{1.. m*n}) : 'X_{1.. m} :=
  [multinom (\sum_(j < n) mon (mxvec_index i j))%N | i < m].

Lemma mdeg_monX mon : mdeg (monX mon) = mdeg mon.

Definition monsY (mz : 'X_{1.. m*n}) :=
  [tuple [multinom mz (mxvec_index i j) | j < n] | i < m].

Definition Ymon (ms : m.-tuple 'X_{1.. n}) :=
  [multinom (tnth ms (vecmx_index i ).1) (vecmx_index i ).2 | i < m*n].

Lemma monsYK : cancel monsY Ymon.
Lemma YmonK : cancel Ymon monsY.
Lemma monsY_bij : bijective monsY.
Lemma Ymon_bij : bijective Ymon.

Lemma mdeg_tnth_monsY mz i :
  mdeg (tnth (monsY mz) i) = tnth (monX mz) i.

Variable (R : comRingType).

#[local] Notation polZ := {mpoly R[m * n]}.
#[local] Notation polX := {mpoly R[m]}.
#[local] Notation polY := {mpoly R[n]}.
Definition polXY := {mpoly polY[m]}.
Definition polXY_scale (c : R) (p : polXY) : polXY := c%:MP *: p.
#[local] Notation "c *:M p" := (polXY_scale c p)
  (at level 40, left associativity).

Fact scale_polXYA a b p : a *:M (b *:M p ) = (a * b ) *:M p.
Fact scale_polXY1m p : 1 *:M p = p.
Fact scale_polXYDr c p1 p2 :
  c *:M (p1 + p2 ) = c *:M p1 + c *:M p2.
Fact scale_polXYDl p c1 c2 :
  (c1 + c2 ) *:M p = c1 *:M p + c2 *:M p.

Lemma scale_polXYE (c : R) (p : polXY) : c *: p = c *:M p.

Fact polXY_scaleAl (c : R) (p q : polXY) : c *: (p * q : polXY) = (c *: p) * q.

Fact polXY_scaleAr (c : R) (p q : polXY) : c *: (p * q : polXY) = p * (c *: q).

Definition polX_XY : polX -> polXY := map_mpoly (mpolyC n (R := R)).

Fact polX_XY_is_additive : additive polX_XY.

Fact polX_XY_is_multiplicative : multiplicative polX_XY.

Fact polX_XY_is_linear : linear polX_XY.

Definition polY_XY : polY -> polXY := mpolyC m (R := {mpoly R[n]}).

Fact polY_XY_is_additive : additive polY_XY.

Fact polY_XY_is_multiplicative : multiplicative polY_XY.

Fact polY_XY_is_linear : linear polY_XY.

Notation "p '(Y)'" := (polY_XY p).
Notation "p '(X)'" := (polX_XY p).

Lemma polyXY_scale p q : p (X ) * q (Y ) = q *: p (X ).

Lemma symmX d (la : 'P_d) : 'hm [la ](X ) = 'hm [la ].

Definition evalXY : polZ -> polXY :=
  mmap ((@mpolyC m _) \o (@mpolyC n R ))
       (fun i => 'X_((vecmx_index i ).1) (X ) * 'X_((vecmx_index i ).2) (Y )).
Notation "p '(XY)'" := (evalXY p).

Fact evalXY_is_additive : additive evalXY.

Fact evalXY_is_multiplicative : multiplicative evalXY.

Fact evalXY_is_linear : linear evalXY.

Lemma evalXY_XE mz :
  'X_[mz](XY ) = 'X_[monX mz](X ) * \prod_(i < m) 'X_[tnth (monsY mz) i](Y ).

Lemma evalXY_homog d p : p \is d.-homog -> p (XY ) \is d.-homog.

Lemma sympXY k : 'p_k (XY ) = 'p_k (X ) * 'p_k (Y ).

Lemma prod_sympXY d (la : 'P_d) : 'hp [la ](XY ) = 'hp [la ](X ) * 'hp [la ](Y ).

The Cauchy reproducing kernel

Definition Cauchy_kernel d := 'h_d (XY ).

Lemma Cauchy_kernel_dhomog d : Cauchy_kernel d \is d.-homog.

Section BijectionFam.

Variable d : nat.

Fact famY_subproof (mz : 'X_{1.. (m * n) < d.+1}) i :
    (mdeg (tnth (monsY (val mz)) i) < d.+1)%N.
Definition famY mz : {ffun 'I_m -> 'X_{1.. n < d.+1}} :=
  [ffun i : 'I_m => BMultinom (famY_subproof mz i)].

Let famYinv_fun (ff : {ffun 'I_m -> 'X_{1.. n < d.+1}}) :=
  let mz := [multinom (ff (vecmx_index i ).1 (vecmx_index i ).2) | i < m * n]
  in if (mdeg mz < d.+1)%N then mz else 0%MM.
Fact famYinv_subproof ff : (mdeg (famYinv_fun ff) < d.+1)%N.
Definition famYinv ff := BMultinom (famYinv_subproof ff).

Lemma famY_bij (mon : 'X_{1.. m}) :
  mdeg mon = d ->
  {on [pred i in
       family (fun i0 (j : 'X_{1.. n < d.+1}) => mdeg j == tnth mon i0)],
    bijective famY }.

End BijectionFam.

Variable d : nat.

Cauchy formula for complete and monomial symmetric polynomials

Lemma Cauchy_symm_symh :
Cauchy_kernel d = \sum_(la : 'P_d) ('h [la ] : polY) *: ('m [la ] : polXY).

Lemma Cauchy_homsymm_homsymh :
Cauchy_kernel d = \sum_(la : 'P_d) 'hm [la ](X ) * 'hh [la ](Y ).

Cauchy formula for Schur symmetric polynomials

Lemma Cauchy_homsyms_homsyms :
Cauchy_kernel d = \sum_(la : 'P_d) 'hs [la ](X ) * 'hs [la ](Y ).

Unused lemma

Lemma Cauchy_kernel_symmetric : Cauchy_kernel d \is symmetric.

Unused lemma

Lemma Cauchy_kernel_coeff_symmetric mon :
(Cauchy_kernel d)@_mon \is symmetric.

Unused lemma

Lemma Cauchy_kernel_coeff_homog mon :
(Cauchy_kernel d)@_mon \is d.-homog.

End CauchyKernel.

Notation "p '(Y)'" := (@polY_XY _ _ _ p).
Notation "p '(X)'" := (@polX_XY _ _ _ p).
Notation "p '(XY)'" := (@evalXY _ _ _ p).

Section CauchyKernelField.
Variable R : fieldType.

Cauchy formula for power sum symmetric polynomials

Lemma Cauchy_homsymp_zhomsymp m n d :
  [char R] =i pred0 ->
  Cauchy_kernel m n R d =
  \sum_(la : 'P_d) 'hp [la ](X ) * ((zcard la)%:R^-1 *: 'hp [la ](Y )).

End CauchyKernelField.

Cauchy kernel and scalar product of symmetric functions

Section Scalar.

Variable n0 d : nat.
#[local] Notation n := n0.+1.
Hypothesis Hd : (d <= n)%N.

#[local] Notation HSC := {homsym algC[n , d ]}.
#[local] Notation HSQ := {homsym rat[n , d ]}.
#[local] Notation polXY := (polXY n0 n0 algC).
#[local] Notation pol := {mpoly algC[n]}.
#[local] Notation "p '(Y)'" := (@polY_XY n0 n0 _ p)
                             (at level 20, format "p '(Y)'").
#[local] Notation "p '(X)'" := (@polX_XY n0 n0 _ p)
                             (at level 20, format "p '(X)'").

#[local] Notation "''hsC[' la ]" := ('hs [la] : HSC).
#[local] Notation "''hsQ[' la ]" := ('hs [la] : HSQ).
#[local] Notation "''hpC[' la ]" := ('hp [la] : HSC).
#[local] Notation "''hpQ[' la ]" := ('hp [la] : HSQ).

Definition co_hp (la : 'P_d) : pol -> algC :=
  homsymdotr 'hp [la ] \o in_homsym d (R := algC).
Definition co_hpXY (la mu : 'P_d) : polXY -> algC :=
  locked (co_hp la \o map_mpoly (co_hp mu)).

Fact co_hp_is_additive la : additive (co_hp la).

Fact co_hp_is_scalar la : scalar (co_hp la).

Lemma co_hp_hp la mu : co_hp la 'hp [mu ] = (zcard mu)%:R * (mu == la)%:R.

Fact co_hpXY_is_additive la mu : additive (co_hpXY la mu).

Lemma co_hpYE la (p q : pol) :
  map_mpoly (co_hp la) (p (X ) * q (Y )) = (co_hp la q) *: p.

Lemma co_hprXYE la mu (p q : pol) :
  co_hpXY la mu (p (X ) * q (Y )) = (co_hp la p) * (co_hp mu q).

Lemma coord_zsympsps (la mu : 'P_d) :
  (\sum_nu
    (coord 'hp (enum_rank la) 'hsC [nu ]) *
    ((zcard mu)%:R * coord 'hp (enum_rank mu) 'hsC [nu ]))
  = (la == mu)%:R.

Lemma coord_zsymspsp (la mu : 'P_d) :
  (\sum_nu
    (coord 'hp (enum_rank nu) 'hsC [la ]) *
    ((zcard nu)%:R * coord 'hp (enum_rank nu) 'hsC [mu ]))
  = (la == mu)%:R.

Schur function are orthonormal

Theorem homsymdotss la mu : '[ 'hsC [la ] | 'hsC [mu ] ] = (la == mu)%:R.

End Scalar.