Library Combi.MPoly.homogsym: Homogenous Symmetric Polynomials

The Space of Homogeneous Symmetric Polynomials

In this file we study the vector space of homogeneous symmetric polynomials. The main goal is to construct its classical basis and Cauchy's scalar product.

f \is d.-homsym == f is a homogenerous of degree d symmetric polynomial.
f \is [in R[n], d.-homsym] == idem specifying the ring and number of variables.
{homsym R[n, d]} == the space of homogenerous of degree d symmetric polynomials in n variables over R.
p *h q == the product of two homogeneous symmetric polynomial as a homogeneous symmetric polynomials.

The classical bases:

'he[la] == the elementary hom. sym. poly. associated to la
'hh[la] == the complete hom. sym. poly. associated to la
'hp[la] == the power sum hom. sym. poly. associated to la
'hm[la] == the monomial hom. sym. poly. associated to la
'hs[la] == the Schur hom. sym. poly. associated to la
in_homsym d p == if p is a polynomial {mpoly R[n]} which is both symmetric and homogeneous of degree d, return it as a {homsym R[n, d]}. It is canonically linear.
'he == the elementary hom. sym. basis
'hh == the complete hom. sym. basis
'hp == the power sum hom. sym. basis
'hm == the monomial hom. sym. basis
'hs == the Schur hom. sym. basis

The omega involution

omegahomsym f == the image of f under the omega involution.

Changing the base ring and the number of variables:

intpart_of_mon m == if m is the monomial x_1^{i_1}x_2^{i_2}...x_n^{i_n} returns the integer partition n^{i_n}...2^{i_2}1^{i_1}
intpartn_of_mon H == the same as an intpart_of_mon d where H is a proof of mnmwgt m = d
map_homsym mor f == change the base ring of the hom. sym. poly f using the ring morphism mor. This is canonically additive.
cnvarhomsym n f == change the number of variables of the hom. sym. poly f by sending elementary to elementary. This is canonically linear.

The scalar product:

'[ u | v ] == the scalar product of hom. sym. poly., only defined over the field algC.
'[ u | v ] _(n, d) == the scalar product of hom. sym. poly. specifying the number of variable and degree.

The main results are symbm_basis, symbe_basis, symbs_basis, symbh_basis, symbp_basis which asserts that they are all bases (if the characteristic of the base ring is zero for symbp_basis), and the definition of the scalar product.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg matrix vector ssrnum algC archimedean.
From mathcomp Require Import fingroup perm.
From mathcomp Require Import ssrcomplements freeg mpoly.

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

Set Implicit Arguments.

Import GRing.Theory.
Import ssrnum algC GRing.Theory Num.Theory.

#[local] Open Scope nat_scope.
#[local] Open Scope ring_scope.

Reserved Notation "{ 'homsym' T [ n , d ] }"
  (at level 0, T, n, d at level 2, format "{ 'homsym' T [ n , d ] }").
Reserved Notation "'[ p | q ]"
  (at level 2, format "'[hv' ''[' p | '/ ' q ] ']'").
Reserved Notation "'[ p | q ] _( R , n )"
  (at level 2, format "'[hv' ''[' p | '/ ' q ] ']' '_(' R , n )").

Definition ishomogsym1 {n} {R : ringType} (d : nat) :
  qualifier 0 {sympoly R [n ]} := [qualify p | sympol p \is d.-homog].

Module SymPolyHomogKey.
Fact homogsym1_key {n} {R : ringType} d : pred_key (@ishomogsym1 n R d).
Definition homogsym1_keyed {n R} d := KeyedQualifier (@homogsym1_key n R d).
End SymPolyHomogKey.
Canonical SymPolyHomogKey.homogsym1_keyed.

Notation "d .-homsym" := (@ishomogsym1 _ _ d)
  (at level 1, format "d .-homsym") : form_scope.
Notation "[ 'in' R [ n ] , d .-homsym ]" := (@ishomogsym1 n R d)
  (at level 0, R, n at level 2, d at level 0,
     format "[ 'in' R [ n ] , d .-homsym ]") : form_scope.

Homogeneous symmetric polynomials

Section DefType.

Variable n : nat.
Variable R : ringType.
Variable d : nat.

Implicit Types p q : {sympoly R [n ]}.

Definition is_homsym p := sympol p \is d.-homog.

Lemma homsymE p : (p \is d .-homsym ) = (is_homsym p ).

Hypothesis Hvar : (d <= n.+1)%N.

Record homogsym : predArgType :=
  HomogSym {homsym :> {sympoly R [n ]}; _ : is_homsym homsym}.

Lemma homsym_inj : injective homsym.

End DefType.

Bind Scope ring_scope with homogsym.
Arguments homogsym n%N R%R.
Arguments homsym_inj n%N R%R d%N.

Notation "{ 'homsym' T [ n , d ] }" := (homogsym n T d).

Section HomogSymLModType.

Variable n : nat.
Variable R : ringType.
Variable d : nat.

#[local] Notation is_homsym := (@is_homsym n R d).

Fact is_homsym_submod_closed : submod_closed is_homsym.

Lemma homsym_is_linear :
  linear (@homsym n R d : {homsym R [n , d ]} -> {sympoly R [n ]}).

Fact homsym_is_dhomog (x : {homsym R [n , d ]}) : sympol x \is d.-homog.
Definition dhomog_of_homogsym (p : {homsym R [n , d ]}) :=
  DHomog (homsym_is_dhomog p).

Fact dhomog_of_sym_is_linear : linear dhomog_of_homogsym.

End HomogSymLModType.

Homogeneous symmetric polynomials as a vector space

Section Vector.

Variable n0 : nat.
#[local] Notation n := (n0.+1).
Variable R : comRingType.

Variable d : nat.
#[local] Notation SF := {sympoly R [n ]}.
Implicit Type (la : 'P_d).

Definition homsymm la : {homsym R [n , d ]} := HomogSym (symm_homog n R la).
Definition homsyme la : {homsym R [n , d ]} := HomogSym (prod_syme_homog n R la).
Definition homsymh la : {homsym R [n , d ]} := HomogSym (prod_symh_homog n R la).
Definition homsymp la : {homsym R [n , d ]} := HomogSym (prod_symp_homog n R la).
Definition homsyms la : {homsym R [n , d ]} := HomogSym (syms_homog n0 R la).

Lemma homsymmE (f : {homsym R [n , d ]}) :
  f = \sum_(l : 'P_d) f@_(mpart l) *: homsymm l.

Fact homogsym_vecaxiom :
  vector_axiom #|[set p : 'P_d | (size p <= n)%N]| {homsym R [n , d ]}.

End Vector.

Notation "''he[' k ]" := (homsyme _ _ k)
                              (at level 8, k at level 2, format "''he[' k ]").
Notation "''hh[' k ]" := (homsymh _ _ k)
                              (at level 8, k at level 2, format "''hh[' k ]").
Notation "''hp[' k ]" := (homsymp _ _ k)
                              (at level 8, k at level 2, format "''hp[' k ]").
Notation "''hm[' k ]" := (homsymm _ _ k)
                              (at level 8, k at level 2, format "''hm[' k ]").
Notation "''hs[' k ]" := (homsyms _ _ k)
                              (at level 8, k at level 2, format "''hs[' k ]").

Products of homogeneous symmetric polynomials

Section HomogSymProd.

Variable n : nat.
Variable R : comRingType.
Variable c d : nat.

Fact homsymprod_subproof (p : {homsym R [n , c ]}) (q : {homsym R [n , d ]}) :
  homsym p * homsym q \is (c + d ).-homsym.
Canonical homsymprod p q : {homsym R [n , c + d ]} :=
  HomogSym (homsymprod_subproof p q).
Definition homsymprodr_head k p q := let: tt := k in homsymprod q p.

Notation homsymprodr := (homsymprodr_head tt).
#[local] Notation "p *h q" := (homsymprod p q)
                             (at level 20, format "p *h q").

Fact homsymprod_is_linear p : linear (homsymprod p).

Lemma homsymprodrE p q : homsymprodr p q = q *h p.
Fact homsymprodr_is_linear p : linear (homsymprodr p).

Lemma homsymprod0r p : p *h 0 = 0.
Lemma homsymprodBr p q1 q2 : p *h (q1 - q2 ) = p *h q1 - p *h q2.
Lemma homsymprodNr p q : p *h (- q ) = - p *h q.
Lemma homsymprodDr p q1 q2 : p *h (q1 + q2 ) = p *h q1 + p *h q2.
Lemma homsymprodMnr p q m : p *h (q *+ m ) = (p *h q) *+ m.
Lemma homsymprod_sumr p I r (P : pred I) (q : I -> {homsym R [n , d ]}) :
  p *h (\sum_(i <- r | P i) q i ) = \sum_(i <- r | P i) p *h q i.
Lemma homsymprodZr a p q : p *h (a *: q ) = a *: (p *h q).

Lemma homsymprod0l p : 0 *h p = 0.
Lemma homsymprodNl p q : (- q ) *h p = - q *h p.
Lemma homsymprodDl p q1 q2 : (q1 + q2 ) *h p = q1 *h p + q2 *h p.
Lemma homsymprodBl p q1 q2 : (q1 - q2 ) *h p = q1 *h p - q2 *h p.
Lemma homsymprodMnl p q m : (q *+ m ) *h p = q *h p *+ m.
Lemma homsymprod_suml p I r (P : pred I) (q : I -> {homsym R [n , c ]}) :
  (\sum_(i <- r | P i) q i ) *h p = \sum_(i <- r | P i) q i *h p.
Lemma homsymprodZl p a q : (a *: q ) *h p = a *: q *h p.

End HomogSymProd.

Notation homsymprodr := (homsymprodr_head tt).
Notation "p *h q" := (homsymprod p q)
                       (at level 20, format "p *h q").

Section HomSymProdGen.

Variable n0 : nat.
#[local] Notation n := (n0.+1).
Variable R : comRingType.
#[local] Notation HSF := {homsym R [n , _]}.

Import LeqGeqOrder.

Variables (d l0 : nat) (la : seq nat).
Hypotheses (Hla : is_part_of_n d la)
           (Hlla : is_part_of_n (l0 + d)%N (l0 :: la)).
Notation Plla := (IntPartN Hlla).
Notation Pla := (IntPartN Hla).

Lemma homsymprod_hh : 'hh [Plla ] = 'hh [rowpartn l0 ] *h 'hh [Pla ] :> HSF.
Lemma homsymprod_he : 'he [Plla ] = 'he [rowpartn l0 ] *h 'he [Pla ] :> HSF.
Lemma homsymprod_hp : 'hp [Plla ] = 'hp [rowpartn l0 ] *h 'hp [Pla ] :> HSF.

End HomSymProdGen.

Section InHomSym.

Variable n0 d : nat.
#[local] Notation n := (n0.+1).
Variable R : comRingType.
#[local] Notation Pol := {mpoly R[n]}.
#[local] Notation HSF := {homsym R [n , d ]}.

#[local] Notation "''pi_' d" :=
  (pihomog [measure of mdeg] d) (at level 5, format "''pi_' d").

TODO: Contribute to Pierre-Yves's multinomials

Lemma msym_pihomog nv s (p : {mpoly R[nv]}) :
  msym s ('pi_d p) = 'pi_d (msym s p ).

Lemma pihomog_sym nv (p : {mpoly R[nv]}) :
  p \is symmetric -> 'pi_d p \is symmetric.

Definition in_homsym (p : Pol) : HSF :=
  \sum_(la : 'P_d) p@_(mpart la) *: 'hm [la ].

Fact in_homsym_is_linear : linear in_homsym.

Lemma in_homsymE (p : HSF) : in_homsym p = p.

End InHomSym.

The omega involution

Section OmegaHomSym.

Variable n0 d : nat.
#[local] Notation n := (n0.+1).
Variable R : comRingType.
#[local] Notation HSF := {homsym R [n , d ]}.
Implicit Types (p q : HSF) (la : intpartn d).

Fact omegahomsym_subproof p : is_homsym d (omegasf p).
Definition omegahomsym p : HSF := HomogSym (omegahomsym_subproof p).
Fact omegahomsym_is_linear : linear omegahomsym.

Lemma omega_homsymh la :
  (head 0%N la <= n)%N -> omegahomsym 'hh [la ] = 'he [la ].
Lemma omega_homsyme la :
  (head 0%N la <= n)%N -> omegahomsym 'he [la ] = 'hh [la ].
Lemma omega_homsyms la :
  (d <= n)%N -> omegahomsym 'hs [la ] = 'hs [conj_intpartn la ].
Lemma omega_homsymp la :
  (head 0%N la <= n)%N -> omegahomsym 'hp [la ] = (-1) ^+ (d - size la) *: 'hp [la ].

End OmegaHomSym.

Section OmegaProd.

Variable n0 : nat.
#[local] Notation n := (n0.+1).
Variable R : comRingType.

Lemma omegahomsym_rmorph c d (p : {homsym R [n , c ]}) (q : {homsym R [n , d ]}) :
  omegahomsym (p *h q) = (omegahomsym p ) *h (omegahomsym q ).

End OmegaProd.

The classical bases of homogeneous symmetric polynomials

Section HomSymField.

Variable n0 d : nat.
#[local] Notation n := (n0.+1).
Variable R : fieldType.
#[local] Notation HSF := {homsym R [n , d ]}.

#[local] Notation Basis := (#|{:'P_d }|.-tuple HSF).
Definition symbe : Basis := [tuple of [seq 'he [la ] | la : 'P_d]].
Definition symbh : Basis := [tuple of [seq 'hh [la ] | la : 'P_d]].
Definition symbm : Basis := [tuple of [seq 'hm [la ] | la : 'P_d]].
Definition symbs : Basis := [tuple of [seq 'hs [la ] | la : 'P_d]].
Definition symbp : Basis := [tuple of [seq 'hp [la ] | la : 'P_d]].

Hypothesis Hd : (d <= n)%N.

Lemma basis_homsym : [set p : 'P_d | (size p <= n)%N] =i {:'P_d }.

Lemma dim_homsym :
  \dim (fullv (vT := HSF)) = #|{:'P_d }|.

Lemma symbm_free : free symbm.

Lemma symbm_basis : basis_of fullv symbm.

Lemma symbs_basis : basis_of fullv symbs.
Lemma symbs_free : free symbs.

Theorem mcoeff_symbs (la : 'P_d) f :
  coord symbs (enum_rank la) f =
  (alternpol 'X_[rho n] * sympol (homsym f))@_(mpart la + rho n).

#[local] Notation E := [tuple mesym n R i.+1 | i < n].

Definition intpart_of_mon m : seq nat :=
  rev (flatten [tuple nseq (m i) i.+1 | i < n]).

Lemma intpart_of_monP m : mnmwgt m = d -> is_part_of_n d (intpart_of_mon m).
Canonical intpartn_of_mon m (H : mnmwgt m = d) := IntPartN (intpart_of_monP H).

#[local] Lemma Esym : (forall i : 'I_n, E`_i \is symmetric).

Lemma comp_symbe m (H : mnmwgt m = d) :
  'X_[m] \mPo E = 'he [intpartn_of_mon H ].

Lemma in_homsym_comp_symbe m (H : mnmwgt m = d) :
  in_homsym d ('X_[m] \mPo E) = 'he [intpartn_of_mon H ].

Lemma symbe_basis : basis_of fullv symbe.
Lemma symbe_free : free symbe.

Lemma symbh_basis : basis_of fullv symbh.
Lemma symbh_free : free symbh.

Lemma symbp_basis : [char R] =i pred0 -> basis_of fullv symbp.
Lemma symbp_free : [char R] =i pred0 -> free symbp.

End HomSymField.

Notation "''he'" := (symbe _ _ _) (at level 8, format "''he'").
Notation "''hh'" := (symbh _ _ _) (at level 8, format "''hh'").
Notation "''hp'" := (symbp _ _ _) (at level 8, format "''hp'").
Notation "''hm'" := (symbm _ _ _) (at level 8, format "''hm'").
Notation "''hs'" := (symbs _ _ _) (at level 8, format "''hs'").

Changing the base field

Section ChangeField.

Variable R S : fieldType.
Variable mor : {rmorphism R -> S}.

Variable n0 d : nat.
#[local] Notation n := (n0.+1).
#[local] Notation HSFR := {homsym R [n , d ]}.
#[local] Notation HSFS := {homsym S [n , d ]}.

Fact map_sympoly_d_homog (p : HSFR) : map_sympoly mor p \is d .-homsym.
Definition map_homsym (p : HSFR) : HSFS := HomogSym (map_sympoly_d_homog p).

Fact map_homsym_is_additive : additive map_homsym.

Lemma map_homsym_is_scalable : scalable_for (mor \; *:%R) map_homsym.

Lemma coord_map_homsym (b : #|{:'P_d }|.-tuple HSFR) j (f : HSFR) :
  basis_of fullv b ->
  basis_of fullv (map_tuple map_homsym b) ->
  coord (map_tuple map_homsym b) j (map_homsym f) = mor (coord b j f).

Lemma map_homsymm la : map_homsym 'hm [la ] = 'hm [la ].
Lemma map_homsyme la : map_homsym 'he [la ] = 'he [la ].
Lemma map_homsymh la : map_homsym 'hh [la ] = 'hh [la ].
Lemma map_homsymp la : map_homsym 'hp [la ] = 'hp [la ].
Lemma map_homsyms la : map_homsym 'hs [la ] = 'hs [la ].

Lemma map_homsymbm : map_tuple map_homsym 'hm = 'hm.
Lemma map_homsymbe : map_tuple map_homsym 'he = 'he.
Lemma map_homsymbh : map_tuple map_homsym 'hh = 'hh.
Lemma map_homsymbp : map_tuple map_homsym 'hp = 'hp.
Lemma map_homsymbs : map_tuple map_homsym 'hs = 'hs.

End ChangeField.

Extracting coords

Section Coord.

Variable n0 d : nat.
#[local] Notation n := (n0.+1).
Variable R : fieldType.
#[local] Notation HSF := {homsym R [n , d ]}.
Implicit Type (la : 'P_d).

Lemma symbmE la : ('hm)`_(enum_rank la) = 'hm [la ] :> HSF.
Lemma symbeE la : ('he)`_(enum_rank la) = 'he [la ] :> HSF.
Lemma symbhE la : ('hh)`_(enum_rank la) = 'hh [la ] :> HSF.
Lemma symbpE la : ('hp)`_(enum_rank la) = 'hp [la ] :> HSF.
Lemma symbsE la : ('hs)`_(enum_rank la) = 'hs [la ] :> HSF.

#[local] Lemma er_eqE (la mu : 'P_d) :
(enum_rank la == enum_rank mu ) = (la == mu ).

#[local] Notation coord := (coord (vT := HSF)).

Hypothesis (Hd : (d <= n)%N).
Lemma coord_symbm la mu : coord 'hm (enum_rank mu) 'hm [la ] = (la == mu)%:R.
Lemma coord_symbe la mu : coord 'he (enum_rank mu) 'he [la ] = (la == mu)%:R.
Lemma coord_symbh la mu : coord 'hh (enum_rank mu) 'hh [la ] = (la == mu)%:R.
Lemma coord_symbs la mu : coord 'hs (enum_rank mu) 'hs [la ] = (la == mu)%:R.

Lemma coord_symbp (char0 : [char R] =i pred0) la mu :
coord 'hp (enum_rank mu) 'hp [la ] = (la == mu)%:R.

End Coord.

Changing the number of variables

Section ChangeNVar.

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

Fact cnvarhomsym_subproof (p : {homsym R [m , d ]}) :
(cnvarsym n0 p ) \is d .-homsym.
Definition cnvarhomsym (p : {homsym R [m , d ]}) : {homsym R [n , d ]} :=
HomogSym (cnvarhomsym_subproof p).
Fact cnvarhomsym_is_linear : linear cnvarhomsym.

Lemma cnvarhomsyme la : cnvarhomsym 'he [la ] = 'he [la ].
Lemma cnvarhomsymh la : cnvarhomsym 'hh [la ] = 'hh [la ].
Lemma cnvarhomsymp la : cnvarhomsym 'hp [la ] = 'hp [la ].
Lemma cnvarhomsymm la : cnvarhomsym 'hm [la ] = 'hm [la ].
Lemma cnvarhomsyms la : cnvarhomsym 'hs [la ] = 'hs [la ].

End ChangeNVar.

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

The scalar product

Section ScalarProduct.

Variable n0 d : nat.
#[local] Notation n := (n0.+1).
#[local] Notation HSF := {homsym algC[n , d ]}.

Definition homsymdot (p q : HSF) : algC :=
  \sum_(i < #|{:'P_d }|)
    (zcard (enum_val i))%:R * (coord 'hp i p) * (coord 'hp i q)^*.
Definition homsymdotr_head k p q := let: tt := k in homsymdot q p.

Notation homsymdotr := (homsymdotr_head tt).
Notation "''[' u | v ]" := (homsymdot u v) : ring_scope.

Lemma homsymdotE p q :
  '[ p | q ] =
  \sum_(la : 'P_d) (zcard la)%:R *
    (coord 'hp (enum_rank la) p) * (coord 'hp (enum_rank la) q)^*.
Lemma homsymdotrE p q : homsymdotr p q = '[q | p ].

Fact homsymdotr_is_scalar p : scalar (homsymdotr p).

Lemma homsymdot0l p : '[0 | p ] = 0.
Lemma homsymdotNl p q : '[- q | p ] = - '[q | p ].
Lemma homsymdotDl p q1 q2 : '[q1 + q2 | p ] = '[q1 | p ] + '[q2 | p ].
Lemma homsymdotBl p q1 q2 : '[q1 - q2 | p ] = '[q1 | p ] - '[q2 | p ].
Lemma homsymdotMnl p q n : '[q *+ n | p ] = '[q | p ] *+ n.
Lemma homsymdot_suml p I r (P : pred I) (q : I -> HSF) :
  '[\sum_(i <- r | P i) q i | p ] = \sum_(i <- r | P i) '[q i | p ].
Lemma homsymdotZl p a q : '[a *: q | p ] = a * '[q | p ].

Lemma homsymdotC p q : '[p | q ] = ('[q | p ])^*.

Lemma homsymdotBr p q1 q2 : '[p | q1 - q2 ] = '[p | q1 ] - '[p | q2 ].

Lemma homsymdot0r p : '[p | 0] = 0.
Lemma homsymdotNr p q : '[p | - q ] = - '[p | q ].
Lemma homsymdotDr p q1 q2 : '[p | q1 + q2 ] = '[p | q1 ] + '[p | q2 ].
Lemma homsymdotMnr p q n : '[p | q *+ n ] = '[p | q ] *+ n.
Lemma homsymdot_sumr p I r (P : pred I) (q : I -> HSF) :
  '[p | \sum_(i <- r | P i) q i ] = \sum_(i <- r | P i) '[p | q i ].
Lemma homsymdotZr a p q : '[p | a *: q ] = a^* * '[p | q ].

Lemma homsymdotpp (Hd : (d <= n)%N) la mu :
  '[ 'hp [la ] | 'hp [mu ] ] = (zcard la)%:R * (la == mu)%:R.

Lemma homsymdot_omegasf f g :
  (d <= n)%N -> '[ omegahomsym f | omegahomsym g ] = '[ f | g ].

End ScalarProduct.

Notation homsymdotr := (homsymdotr_head tt).
Notation "''[' u | v ]" := (homsymdot u v) : ring_scope.
Notation "''[' u | v ] _( n , d )" :=
  (@homsymdot n d u v) (only parsing) : ring_scope.