Library Combi.MPoly.sympoly: Symmetric Polynomials
The Ring of Symmetric Polynomials
- {sympoly R[n]} == the ring of symmetric polynomial in n variable over R.
- sympol f == the coercion from {sympoly R[n]} to {mpoly R[n]}
- 'e_k == the k-th elementary symmetric polynomial
- 'h_k == the k-th complete homogeneous symmetric polynomial
- 'p_k == the k-th power sum symmetric polynomial
- prod_gen G la == given a familly of generators G : nat -> {sympoly R[n]}
the product \prod_(i <- la) G i.
- 'e[mu] == the product of elementary symmetric polynomial
- 'h[mu] == the product of complete homogeneous symmetric polynomial
- 'p[mu] == the product of power sum symmetric polynomial
- 'm[mu] == the monomial symmetric polynomial
- 's[mu] == the Schur symmetric polynomial
- coeff_prodgen Co la mu == the coefficient of the product 'g[la] on 'g_[mu] assuming that co : forall d : nat, 'P_d -> R gives the coefficients of 'f_i on 'g_[mu]
- map_sympoly M == the ring morphism {sympoly R[n]} -> {sympoly S[n]} obtained by the change of scalar M : {rmorphism R -> S}
- perm_partn la == the number of composition which are permuted of la
- prod_partsum la == the product of the sum of all the prefix of la
- e and h : syme_to_symh symh_to_syme
- s and m : syms_symm symm_syms
- s and h : syms_symh symh_syms
- h and p : symh_to_symp and Newton's formulas Newton_symh Newton_symh1
- e and p : Newton's formulas Newton_syme1
- h and m : symh_to_symm
- p and m : symp_to_symm
- omegasf == the omega involution, that is the unique ring morphism exchanging 'e_k and 'h_k wheneven k is smaller than the number of variables.
- sympolyf R m == the algebra morphism expanding any symetric polynomial (in {sympoly R[m]}) as a polynomial in the 'e_i (in {mpoly R[m]}) by the fundamental theorem of symmetric polynomials.
- cnvarsym R m n == the canonical algebra morphism {sympoly R[m.+1]} -> {sympoly R[n.+1]} sending 'e_i to 'e_i computed thanks to the fundamental theorem.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrint fingroup perm.
From mathcomp Require Import ssrcomplements freeg mpoly.
Require Import sorted tools ordtype permuted partition skewpart composition.
Require Import Yamanouchi std tableau stdtab skewtab permcent.
Require Import antisym Schur_mpoly therule Schur_altdef unitriginv.
Set Implicit Arguments.
#[local] Open Scope ring_scope.
Import GRing.Theory.
Lemma boolRP (R : ringType) (b : bool) : reflect (b%:R = 0 :> R) (~~b).
Section MultinomCompl.
Variables (n : nat) (R : comRingType).
Lemma mnm_n0E : @all_equal_to 'X_{1..0} 0%MM.
Lemma eq_mnm1 (i j : 'I_n) : (U_(i)%MM == U_(j)%MM) = (i == j).
Lemma mcoeffXU (i j : 'I_n) : ('X_i @_U_(j) : R) = (i == j)%:R.
End MultinomCompl.
Reserved Notation "{ 'sympoly' T [ n ] }"
(at level 0, T, n at level 2, format "{ 'sympoly' T [ n ] }").
Reserved Notation "''e_' k" (at level 8, k at level 2, format "''e_' k").
Reserved Notation "''h_' k" (at level 8, k at level 2, format "''h_' k").
Reserved Notation "''p_' k" (at level 8, k at level 2, format "''p_' k").
Reserved Notation "''e[' k ]" (at level 8, format "''e[' k ]").
Reserved Notation "''h[' k ]" (at level 8, format "''h[' k ]").
Reserved Notation "''p[' k ]" (at level 8, format "''p[' k ]").
Reserved Notation "''m[' k ]" (at level 8, format "''m[' k ]").
Reserved Notation "''s[' k ]" (at level 8, format "''s[' k ]").
Section DefType.
Variable n : nat.
Variable R : ringType.
Record sympoly : predArgType :=
SymPoly {sympol :> {mpoly R[n]}; _ : sympol \is symmetric}.
Lemma sympol_inj : injective sympol.
End DefType.
Bind Scope ring_scope with sympoly.
Arguments sympol n%N R%R.
Notation "{ 'sympoly' T [ n ] }" := (sympoly n T).
Section SymPolyRingType.
Variable n : nat.
Variable R : ringType.
Fact sympol_is_linear : linear (@sympol n R).
Fact sympol_is_multiplicative : multiplicative (@sympol n R).
Lemma sympolP (x : {sympoly R[n]}) : sympol x \is symmetric.
End SymPolyRingType.
#[export] Hint Resolve sympolP : core.
Section SymPolyComRingType.
Variable n : nat.
Variable R : comRingType.
End SymPolyComRingType.
Section SymPolyIdomainType.
Variable n : nat.
Variable R : idomainType.
End SymPolyIdomainType.
Section Bases.
Variable n : nat.
Variable R : comRingType.
Implicit Type m : 'X_{1.. n}.
#[local] Notation "m # s" := [multinom m (s i) | i < n]
(at level 40, left associativity, format "m # s").
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrint fingroup perm.
From mathcomp Require Import ssrcomplements freeg mpoly.
Require Import sorted tools ordtype permuted partition skewpart composition.
Require Import Yamanouchi std tableau stdtab skewtab permcent.
Require Import antisym Schur_mpoly therule Schur_altdef unitriginv.
Set Implicit Arguments.
#[local] Open Scope ring_scope.
Import GRing.Theory.
Lemma boolRP (R : ringType) (b : bool) : reflect (b%:R = 0 :> R) (~~b).
Section MultinomCompl.
Variables (n : nat) (R : comRingType).
Lemma mnm_n0E : @all_equal_to 'X_{1..0} 0%MM.
Lemma eq_mnm1 (i j : 'I_n) : (U_(i)%MM == U_(j)%MM) = (i == j).
Lemma mcoeffXU (i j : 'I_n) : ('X_i @_U_(j) : R) = (i == j)%:R.
End MultinomCompl.
Reserved Notation "{ 'sympoly' T [ n ] }"
(at level 0, T, n at level 2, format "{ 'sympoly' T [ n ] }").
Reserved Notation "''e_' k" (at level 8, k at level 2, format "''e_' k").
Reserved Notation "''h_' k" (at level 8, k at level 2, format "''h_' k").
Reserved Notation "''p_' k" (at level 8, k at level 2, format "''p_' k").
Reserved Notation "''e[' k ]" (at level 8, format "''e[' k ]").
Reserved Notation "''h[' k ]" (at level 8, format "''h[' k ]").
Reserved Notation "''p[' k ]" (at level 8, format "''p[' k ]").
Reserved Notation "''m[' k ]" (at level 8, format "''m[' k ]").
Reserved Notation "''s[' k ]" (at level 8, format "''s[' k ]").
Section DefType.
Variable n : nat.
Variable R : ringType.
Record sympoly : predArgType :=
SymPoly {sympol :> {mpoly R[n]}; _ : sympol \is symmetric}.
Lemma sympol_inj : injective sympol.
End DefType.
Bind Scope ring_scope with sympoly.
Arguments sympol n%N R%R.
Notation "{ 'sympoly' T [ n ] }" := (sympoly n T).
Section SymPolyRingType.
Variable n : nat.
Variable R : ringType.
Fact sympol_is_linear : linear (@sympol n R).
Fact sympol_is_multiplicative : multiplicative (@sympol n R).
Lemma sympolP (x : {sympoly R[n]}) : sympol x \is symmetric.
End SymPolyRingType.
#[export] Hint Resolve sympolP : core.
Section SymPolyComRingType.
Variable n : nat.
Variable R : comRingType.
End SymPolyComRingType.
Section SymPolyIdomainType.
Variable n : nat.
Variable R : idomainType.
End SymPolyIdomainType.
Section Bases.
Variable n : nat.
Variable R : comRingType.
Implicit Type m : 'X_{1.. n}.
#[local] Notation "m # s" := [multinom m (s i) | i < n]
(at level 40, left associativity, format "m # s").
Fact syme_sym d : mesym n R d \is symmetric.
Canonical syme d : {sympoly R[n]} := SymPoly (syme_sym d).
#[local] Notation "''e_' k" := (syme k).
Lemma syme_geqnE d : d > n -> 'e_d = 0.
Lemma syme_homog d : sympol 'e_d \is d.-homog.
Canonical syme d : {sympoly R[n]} := SymPoly (syme_sym d).
#[local] Notation "''e_' k" := (syme k).
Lemma syme_geqnE d : d > n -> 'e_d = 0.
Lemma syme_homog d : sympol 'e_d \is d.-homog.
Definition symh_pol_bound b d : {mpoly R[n]} :=
\sum_(m : 'X_{1..n < b} | mdeg m == d) 'X_[m].
Definition symh_pol d : {mpoly R[n]} := symh_pol_bound d.+1 d.
Lemma mcoeff_symh_pol_bound b d m :
b > d -> (symh_pol_bound b d)@_m = (mdeg m == d)%:R.
Lemma mcoeff_symh_pol d m : (symh_pol d)@_m = (mdeg m == d)%:R.
Lemma symh_pol_any b d : d < b -> symh_pol d = symh_pol_bound b d.
Fact symh_sym d : symh_pol d \is symmetric.
Canonical symh d : {sympoly R[n]} := SymPoly (symh_sym d).
#[local] Notation "''h_' k" := (symh k).
Lemma mcoeff_symh d m : 'h_d@_m = (mdeg m == d)%:R.
Lemma symh_homog d : sympol 'h_d \is d.-homog.
\sum_(m : 'X_{1..n < b} | mdeg m == d) 'X_[m].
Definition symh_pol d : {mpoly R[n]} := symh_pol_bound d.+1 d.
Lemma mcoeff_symh_pol_bound b d m :
b > d -> (symh_pol_bound b d)@_m = (mdeg m == d)%:R.
Lemma mcoeff_symh_pol d m : (symh_pol d)@_m = (mdeg m == d)%:R.
Lemma symh_pol_any b d : d < b -> symh_pol d = symh_pol_bound b d.
Fact symh_sym d : symh_pol d \is symmetric.
Canonical symh d : {sympoly R[n]} := SymPoly (symh_sym d).
#[local] Notation "''h_' k" := (symh k).
Lemma mcoeff_symh d m : 'h_d@_m = (mdeg m == d)%:R.
Lemma symh_homog d : sympol 'h_d \is d.-homog.
Definition symp_pol d : {mpoly R[n]} := \sum_(i < n) 'X_i ^+ d.
Fact symp_sym d : symp_pol d \is symmetric.
Canonical symp d : {sympoly R[n]} := SymPoly (symp_sym d).
#[local] Notation "''p_' k" := (symp k).
Lemma symp_homog d : sympol 'p_d \is d.-homog.
Fact symp_sym d : symp_pol d \is symmetric.
Canonical symp d : {sympoly R[n]} := SymPoly (symp_sym d).
#[local] Notation "''p_' k" := (symp k).
Lemma symp_homog d : sympol 'p_d \is d.-homog.
Definition symm_pol (sh : n.-tuple nat) : {mpoly R[n]} :=
\sum_(p : permuted sh) 'X_[Multinom p].
Lemma mcoeff_symm_pol sh m : (symm_pol sh)@_m = (perm_eq sh m)%:R.
Fact symm_sym sh : symm_pol sh \is symmetric.
Definition symm sh : {sympoly R[n]} :=
if size sh <= n then SymPoly (symm_sym (mpart sh)) else 0 : {sympoly R[n]}.
Notation "''m[' k ]" := (symm k).
Lemma symm_oversize sh : n < size sh -> 'm[sh] = 0.
Lemma mcoeff_symm sh m :
size sh <= n -> 'm[sh]@_m = (perm_eq (mpart (n := n) sh) m)%:R.
Lemma symm_homog d (sh : 'P_d) : sympol 'm[sh] \is d.-homog.
Lemma symE (p q : {sympoly R[n]}) :
reflect (forall m, m \is dominant -> p@_m = q@_m) (p == q).
\sum_(p : permuted sh) 'X_[Multinom p].
Lemma mcoeff_symm_pol sh m : (symm_pol sh)@_m = (perm_eq sh m)%:R.
Fact symm_sym sh : symm_pol sh \is symmetric.
Definition symm sh : {sympoly R[n]} :=
if size sh <= n then SymPoly (symm_sym (mpart sh)) else 0 : {sympoly R[n]}.
Notation "''m[' k ]" := (symm k).
Lemma symm_oversize sh : n < size sh -> 'm[sh] = 0.
Lemma mcoeff_symm sh m :
size sh <= n -> 'm[sh]@_m = (perm_eq (mpart (n := n) sh) m)%:R.
Lemma symm_homog d (sh : 'P_d) : sympol 'm[sh] \is d.-homog.
Lemma symE (p q : {sympoly R[n]}) :
reflect (forall m, m \is dominant -> p@_m = q@_m) (p == q).
Lemma sym_symmE (p : {sympoly R[n]}) :
p = \sum_(m <- msupp p | m \is dominant) p@_m *: 'm[partm m].
Lemma size_mpart_in_supp (f : {mpoly R[n]}) d (p : 'P_d) :
f \is d.-homog -> mpart p \in msupp f -> size p <= n.
Lemma dominant_mpart d m :
m \is dominant -> mdeg m = d -> { p : 'P_d | m = mpart p }.
Lemma homog_symmE d (f : {sympoly R[n]}) :
sympol f \is d.-homog -> f = \sum_(l : 'P_d) f@_(mpart l) *: 'm[l].
Lemma symm_unique d (f : {sympoly R[n]}) c :
f = \sum_(l : 'P_d) (c l) *: 'm[l] ->
forall l : 'P_d, size l <= n -> c l = f@_(mpart l).
Lemma symm_unique0 d c :
\sum_(l : 'P_d) (c l) *: 'm[l] = 0 ->
forall l : 'P_d, size l <= n -> c l = 0.
Lemma sum_symmE d (f : {sympoly R[n]}) :
\sum_(l : 'P_d) f@_(mpart l) *: 'm[l] =
\sum_(l <- [seq val p | p <- enum {: 'P_d}]) f@_(mpart l) *: 'm[l].
p = \sum_(m <- msupp p | m \is dominant) p@_m *: 'm[partm m].
Lemma size_mpart_in_supp (f : {mpoly R[n]}) d (p : 'P_d) :
f \is d.-homog -> mpart p \in msupp f -> size p <= n.
Lemma dominant_mpart d m :
m \is dominant -> mdeg m = d -> { p : 'P_d | m = mpart p }.
Lemma homog_symmE d (f : {sympoly R[n]}) :
sympol f \is d.-homog -> f = \sum_(l : 'P_d) f@_(mpart l) *: 'm[l].
Lemma symm_unique d (f : {sympoly R[n]}) c :
f = \sum_(l : 'P_d) (c l) *: 'm[l] ->
forall l : 'P_d, size l <= n -> c l = f@_(mpart l).
Lemma symm_unique0 d c :
\sum_(l : 'P_d) (c l) *: 'm[l] = 0 ->
forall l : 'P_d, size l <= n -> c l = 0.
Lemma sum_symmE d (f : {sympoly R[n]}) :
\sum_(l : 'P_d) f@_(mpart l) *: 'm[l] =
\sum_(l <- [seq val p | p <- enum {: 'P_d}]) f@_(mpart l) *: 'm[l].
Lemma syme0 : 'e_0 = 1.
Lemma symp0 : 'p_0 = n%:R.
Lemma symh0 : 'h_0 = 1.
Lemma symm0 : 'm[[::]] = 1.
Lemma symp0 : 'p_0 = n%:R.
Lemma symh0 : 'h_0 = 1.
Lemma symm0 : 'm[[::]] = 1.
Lemma syme1 : val ('e_1) = \sum_(i < n) 'X_i.
Lemma sympe1E : 'p_1 = 'e_1.
Lemma symhe1E : 'h_1 = 'e_1.
End Bases.
Notation "''e_' k" := (syme _ _ k).
Notation "''h_' k" := (symh _ _ k).
Notation "''p_' k" := (symp _ _ k).
Notation "''m[' k ]" := (symm _ _ k).
Section ChangeBaseMonomial.
Variables (n : nat) (R : comRingType).
#[local] Notation SP := {sympoly R[n]}.
Lemma expUmpartE nv k :
(U_(ord0) *+ k)%MM = mpart (rowpartn k) :> 'X_{1..nv.+1}.
Lemma expUmpartNE nv k i (P : intpartn k.+1) :
((U_(i) *+ k.+1)%MM == mpart P :> 'X_{1..nv.+1})
= (i == ord0) && (P == rowpartn k.+1).
Lemma symp_to_symm k : 'p_k.+1 = 'm[rowpartn k.+1] :> SP.
Lemma symh_to_symm k : 'h_k = \sum_(l : 'P_k) 'm[l] :> SP.
Lemma syme_to_symm k : 'e_k = 'm[colpartn k] :> SP.
End ChangeBaseMonomial.
Lemma sympe1E : 'p_1 = 'e_1.
Lemma symhe1E : 'h_1 = 'e_1.
End Bases.
Notation "''e_' k" := (syme _ _ k).
Notation "''h_' k" := (symh _ _ k).
Notation "''p_' k" := (symp _ _ k).
Notation "''m[' k ]" := (symm _ _ k).
Section ChangeBaseMonomial.
Variables (n : nat) (R : comRingType).
#[local] Notation SP := {sympoly R[n]}.
Lemma expUmpartE nv k :
(U_(ord0) *+ k)%MM = mpart (rowpartn k) :> 'X_{1..nv.+1}.
Lemma expUmpartNE nv k i (P : intpartn k.+1) :
((U_(i) *+ k.+1)%MM == mpart P :> 'X_{1..nv.+1})
= (i == ord0) && (P == rowpartn k.+1).
Lemma symp_to_symm k : 'p_k.+1 = 'm[rowpartn k.+1] :> SP.
Lemma symh_to_symm k : 'h_k = \sum_(l : 'P_k) 'm[l] :> SP.
Lemma syme_to_symm k : 'e_k = 'm[colpartn k] :> SP.
End ChangeBaseMonomial.
Section Schur.
Variable n0 : nat.
Variable R : comRingType.
#[local] Notation n := n0.+1.
Definition syms d (la : 'P_d) : {sympoly R[n]} :=
SymPoly (Schur_sym n0 R la).
#[local] Notation "''s[' k ]" := (syms k).
Lemma syms_homog d (la : 'P_d) : sympol 's[la] \is d.-homog.
Lemma syms0 (la : 'P_0) : 's[la] = 1.
Lemma syms1 (la : 'P_1) : 's[la] = \sum_(i < n) 'X_i :> {mpoly R[n]}.
Lemma syms_rowpartn d : 's[rowpartn d] = 'h_d.
Lemma syms_colpartn d : 's[colpartn d] = 'e_d.
Lemma syms_oversize d (la : 'P_d) : n < size la -> 's[la] = 0.
End Schur.
Notation "''s[' k ]" := (syms _ _ k).
Variable n0 : nat.
Variable R : comRingType.
#[local] Notation n := n0.+1.
Definition syms d (la : 'P_d) : {sympoly R[n]} :=
SymPoly (Schur_sym n0 R la).
#[local] Notation "''s[' k ]" := (syms k).
Lemma syms_homog d (la : 'P_d) : sympol 's[la] \is d.-homog.
Lemma syms0 (la : 'P_0) : 's[la] = 1.
Lemma syms1 (la : 'P_1) : 's[la] = \sum_(i < n) 'X_i :> {mpoly R[n]}.
Lemma syms_rowpartn d : 's[rowpartn d] = 'h_d.
Lemma syms_colpartn d : 's[colpartn d] = 'e_d.
Lemma syms_oversize d (la : 'P_d) : n < size la -> 's[la] = 0.
End Schur.
Notation "''s[' k ]" := (syms _ _ k).
Multiplicative bases.
Section ProdGen.
Variable n : nat.
Variable R : comRingType.
#[local] Notation SF := {sympoly R[n]}.
Section Defs.
Variable gen : nat -> SF.
Hypothesis gen_homog : forall d, sympol (gen d) \is d.-homog.
Definition prod_gen d (sh : 'P_d) := \prod_(i <- sh) gen i.
#[local] Notation "''g_' k" := (gen k) (at level 8, format "''g_' k").
#[local] Notation "''g[' k ]" := (prod_gen k) (at level 8, format "''g[' k ]").
Lemma prod_gen_homog d (sh : 'P_d) : sympol 'g[sh] \is d.-homog.
Lemma prod_gen0 (l : 'P_0) : 'g[l] = 1.
Lemma prod_genM c d (l : 'P_c) (k : 'P_d) : 'g[l] * 'g[k] = 'g[l +|+ k].
Lemma prod_gen_colpartn d : 'g[colpartn d] = 'g_1 ^+ d.
Lemma prod_gen_cast d1 d2 (eq_d : d1 = d2) (la : 'P_d1) :
'g[cast_intpartn eq_d la] = 'g[la].
End Defs.
Variable gA gB : nat -> SF.
Variable co : forall (d : nat), 'P_d -> R.
#[local] Notation "''gA_' k" := (gA k) (at level 8, format "''gA_' k").
#[local] Notation "''gA[' k ]" :=
(prod_gen gA k) (at level 8, format "''gA[' k ]").
#[local] Notation "''gB_' k" := (gB k) (at level 8, format "''gB_' k").
#[local] Notation "''gB[' k ]" :=
(prod_gen gB k) (at level 8, format "''gB[' k ]").
Fixpoint coeff_prodgen_seq l : 'P_(sumn l) -> R :=
if l is l0 :: l' then
fun la : 'P_(sumn (l0 :: l')) =>
\sum_(p | la == p.1 +|+ p.2) co p.1 * coeff_prodgen_seq p.2
else fun _ => 1.
#[local] Notation "''co[' k ]" := (coeff_prodgen_seq k)
(at level 8, format "''co[' k ]").
#[local] Notation "''co[' k ]_ l" := (coeff_prodgen_seq (l := l) k)
(at level 8, only parsing).
Definition coeff_prodgen d (la mu : 'P_d) : R :=
'co[cast_intpartn (esym (sumn_intpartn la)) mu].
Lemma coeff_prodgen_cast l k nu (eqlamu : l = k) (eqsum : sumn l = sumn k) :
'co[cast_intpartn eqsum nu] = 'co[nu].
Lemma prod_prodgen :
(forall d, 'gA_d = \sum_(la : 'P_d) co la *: 'gB[la] :> SF) ->
forall d (la : 'P_d),
'gA[la] = \sum_(mu : 'P_d)
coeff_prodgen la mu *: 'gB[mu] :> SF.
Definition prod_syme := prod_gen (@syme n R).
Definition prod_syme_homog := prod_gen_homog (@syme_homog n R).
Definition prod_symh := prod_gen (@symh n R).
Definition prod_symh_homog := prod_gen_homog (@symh_homog n R).
Definition prod_symp := prod_gen (@symp n R).
Definition prod_symp_homog := prod_gen_homog (@symp_homog n R).
End ProdGen.
Notation "''e[' k ]" := (prod_syme _ _ k).
Notation "''h[' k ]" := (prod_symh _ _ k).
Notation "''p[' k ]" := (prod_symp _ _ k).
Variable n : nat.
Variable R : comRingType.
#[local] Notation SF := {sympoly R[n]}.
Section Defs.
Variable gen : nat -> SF.
Hypothesis gen_homog : forall d, sympol (gen d) \is d.-homog.
Definition prod_gen d (sh : 'P_d) := \prod_(i <- sh) gen i.
#[local] Notation "''g_' k" := (gen k) (at level 8, format "''g_' k").
#[local] Notation "''g[' k ]" := (prod_gen k) (at level 8, format "''g[' k ]").
Lemma prod_gen_homog d (sh : 'P_d) : sympol 'g[sh] \is d.-homog.
Lemma prod_gen0 (l : 'P_0) : 'g[l] = 1.
Lemma prod_genM c d (l : 'P_c) (k : 'P_d) : 'g[l] * 'g[k] = 'g[l +|+ k].
Lemma prod_gen_colpartn d : 'g[colpartn d] = 'g_1 ^+ d.
Lemma prod_gen_cast d1 d2 (eq_d : d1 = d2) (la : 'P_d1) :
'g[cast_intpartn eq_d la] = 'g[la].
End Defs.
Variable gA gB : nat -> SF.
Variable co : forall (d : nat), 'P_d -> R.
#[local] Notation "''gA_' k" := (gA k) (at level 8, format "''gA_' k").
#[local] Notation "''gA[' k ]" :=
(prod_gen gA k) (at level 8, format "''gA[' k ]").
#[local] Notation "''gB_' k" := (gB k) (at level 8, format "''gB_' k").
#[local] Notation "''gB[' k ]" :=
(prod_gen gB k) (at level 8, format "''gB[' k ]").
Fixpoint coeff_prodgen_seq l : 'P_(sumn l) -> R :=
if l is l0 :: l' then
fun la : 'P_(sumn (l0 :: l')) =>
\sum_(p | la == p.1 +|+ p.2) co p.1 * coeff_prodgen_seq p.2
else fun _ => 1.
#[local] Notation "''co[' k ]" := (coeff_prodgen_seq k)
(at level 8, format "''co[' k ]").
#[local] Notation "''co[' k ]_ l" := (coeff_prodgen_seq (l := l) k)
(at level 8, only parsing).
Definition coeff_prodgen d (la mu : 'P_d) : R :=
'co[cast_intpartn (esym (sumn_intpartn la)) mu].
Lemma coeff_prodgen_cast l k nu (eqlamu : l = k) (eqsum : sumn l = sumn k) :
'co[cast_intpartn eqsum nu] = 'co[nu].
Lemma prod_prodgen :
(forall d, 'gA_d = \sum_(la : 'P_d) co la *: 'gB[la] :> SF) ->
forall d (la : 'P_d),
'gA[la] = \sum_(mu : 'P_d)
coeff_prodgen la mu *: 'gB[mu] :> SF.
Definition prod_syme := prod_gen (@syme n R).
Definition prod_syme_homog := prod_gen_homog (@syme_homog n R).
Definition prod_symh := prod_gen (@symh n R).
Definition prod_symh_homog := prod_gen_homog (@symh_homog n R).
Definition prod_symp := prod_gen (@symp n R).
Definition prod_symp_homog := prod_gen_homog (@symp_homog n R).
End ProdGen.
Notation "''e[' k ]" := (prod_syme _ _ k).
Notation "''h[' k ]" := (prod_symh _ _ k).
Notation "''p[' k ]" := (prod_symp _ _ k).
Casting the index
Section Cast.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variables R : comRingType.
#[local] Notation SF := {sympoly R[n]}.
Variables (d1 d2 : nat) (eq_d : d1 = d2) (la : 'P_d1).
Lemma syms_cast : 's[cast_intpartn eq_d la] = 's[la] :> SF.
Lemma syme_cast : 'e[cast_intpartn eq_d la] = 'e[la] :> SF.
Lemma symh_cast : 'h[cast_intpartn eq_d la] = 'h[la] :> SF.
Lemma symp_cast : 'p[cast_intpartn eq_d la] = 'p[la] :> SF.
Lemma symm_cast : 'm[cast_intpartn eq_d la] = 'm[la] :> SF.
End Cast.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variables R : comRingType.
#[local] Notation SF := {sympoly R[n]}.
Variables (d1 d2 : nat) (eq_d : d1 = d2) (la : 'P_d1).
Lemma syms_cast : 's[cast_intpartn eq_d la] = 's[la] :> SF.
Lemma syme_cast : 'e[cast_intpartn eq_d la] = 'e[la] :> SF.
Lemma symh_cast : 'h[cast_intpartn eq_d la] = 'h[la] :> SF.
Lemma symp_cast : 'p[cast_intpartn eq_d la] = 'p[la] :> SF.
Lemma symm_cast : 'm[cast_intpartn eq_d la] = 'm[la] :> SF.
End Cast.
Section LRrule_Pieri.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variables R : comRingType.
#[local] Notation SF := {sympoly R[n]}.
Lemma syms_symsM d1 (la : 'P_d1) d2 (mu : 'P_d2) :
's[la] * 's[mu] =
\sum_(nu : 'P_(d1 + d2) | included la nu)
's[nu] *+ LRyam_coeff la mu nu :> SF.
Lemma syms_symhM d1 (la : 'P_d1) d2 :
's[la] * 'h_d2 = \sum_(nu : 'P_(d1 + d2) | hb_strip la nu) 's[nu] :> SF.
Lemma syms_symeM d1 (la : 'P_d1) d2 :
's[la] * 'e_d2 = \sum_(nu : 'P_(d1 + d2) | vb_strip la nu) 's[nu] :> SF.
End LRrule_Pieri.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variables R : comRingType.
#[local] Notation SF := {sympoly R[n]}.
Lemma syms_symsM d1 (la : 'P_d1) d2 (mu : 'P_d2) :
's[la] * 's[mu] =
\sum_(nu : 'P_(d1 + d2) | included la nu)
's[nu] *+ LRyam_coeff la mu nu :> SF.
Lemma syms_symhM d1 (la : 'P_d1) d2 :
's[la] * 'h_d2 = \sum_(nu : 'P_(d1 + d2) | hb_strip la nu) 's[nu] :> SF.
Lemma syms_symeM d1 (la : 'P_d1) d2 :
's[la] * 'e_d2 = \sum_(nu : 'P_(d1 + d2) | vb_strip la nu) 's[nu] :> SF.
End LRrule_Pieri.
Section ScalarChange.
Variables R S : comRingType.
Variable mor : {rmorphism R -> S}.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Lemma map_mpoly_issym (f : {sympoly R[n]}) : map_mpoly mor f \is symmetric.
Definition map_sympoly (f : {sympoly R[n]}) : {sympoly S[n]} :=
SymPoly (map_mpoly_issym f).
Fact map_sympoly_is_additive : additive map_sympoly.
Fact map_sympoly_is_multiplicative : multiplicative map_sympoly.
Lemma map_sympoly_is_scalable : scalable_for (mor \; *:%R) map_sympoly.
Lemma map_symm d : map_sympoly 'm[d] = 'm[d].
Lemma map_syme d : map_sympoly 'e_d = 'e_d.
Lemma map_syme_prod d (l : 'P_d) : map_sympoly 'e[l] = 'e[l].
Lemma map_symh d : map_sympoly 'h_d = 'h_d.
Lemma map_symh_prod d (l : 'P_d) : map_sympoly 'h[l] = 'h[l].
Lemma map_symp d : map_sympoly 'p_d = 'p_d.
Lemma map_symp_prod d (l : 'P_d) : map_sympoly 'p[l] = 'p[l].
Lemma map_syms d (la : 'P_d) :
map_sympoly 's[la] = 's[la].
End ScalarChange.
Variables R S : comRingType.
Variable mor : {rmorphism R -> S}.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Lemma map_mpoly_issym (f : {sympoly R[n]}) : map_mpoly mor f \is symmetric.
Definition map_sympoly (f : {sympoly R[n]}) : {sympoly S[n]} :=
SymPoly (map_mpoly_issym f).
Fact map_sympoly_is_additive : additive map_sympoly.
Fact map_sympoly_is_multiplicative : multiplicative map_sympoly.
Lemma map_sympoly_is_scalable : scalable_for (mor \; *:%R) map_sympoly.
Lemma map_symm d : map_sympoly 'm[d] = 'm[d].
Lemma map_syme d : map_sympoly 'e_d = 'e_d.
Lemma map_syme_prod d (l : 'P_d) : map_sympoly 'e[l] = 'e[l].
Lemma map_symh d : map_sympoly 'h_d = 'h_d.
Lemma map_symh_prod d (l : 'P_d) : map_sympoly 'h[l] = 'h[l].
Lemma map_symp d : map_sympoly 'p_d = 'p_d.
Lemma map_symp_prod d (l : 'P_d) : map_sympoly 'p[l] = 'p[l].
Lemma map_syms d (la : 'P_d) :
map_sympoly 's[la] = 's[la].
End ScalarChange.
Section ChangeBasis.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variable R : comRingType.
#[local] Notation "''Xn'" := 'X_{1.. n}.
#[local] Notation "''Xn_' m" := 'X_{1.. n < (mdeg m).+1}
(at level 10, m at next level, format "''Xn_' m").
#[local] Notation "''XXn_' m" := 'X_{1.. n < (mdeg m).+1, (mdeg m).+1}
(at level 10, m at next level, format "''XXn_' m").
Implicit Type m : 'Xn.
#[local] Notation SF := {sympoly R[n]}.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variable R : comRingType.
#[local] Notation "''Xn'" := 'X_{1.. n}.
#[local] Notation "''Xn_' m" := 'X_{1.. n < (mdeg m).+1}
(at level 10, m at next level, format "''Xn_' m").
#[local] Notation "''XXn_' m" := 'X_{1.. n < (mdeg m).+1, (mdeg m).+1}
(at level 10, m at next level, format "''XXn_' m").
Implicit Type m : 'Xn.
#[local] Notation SF := {sympoly R[n]}.
Lemma sum_symh_syme (d : nat) :
d != 0%N ->
\sum_(0 <= i < d.+1) (-1) ^+ i *: ('h_i * 'e_(d - i)) = 0 :> SF.
Lemma sum_syme_symh (d : nat) :
d != 0%N ->
\sum_(0 <= i < d.+1) (-1) ^+ i *: ('e_i * 'h_(d - i)) = 0 :> SF.
Section HandE.
Variable E H : nat -> {sympoly R[n]}.
Hypothesis E0 : E 0 = 1.
Hypothesis H0 : H 0 = 1.
Hypothesis Hanti : forall d : nat,
d != 0%N ->
\sum_(0 <= i < d.+1) (-1) ^+ i *: (H i * E (d - i)) = 0.
Lemma symHE_rec (d : nat) :
d != 0%N ->
E d = \sum_(1 <= i < d.+1) H i * ((-1) ^+ i.-1 *: E (d - i)).
Lemma symHE_prod_intcomp d :
E d = \sum_(c : intcompn d) (-1) ^+ (d - size c) *: (\prod_(i <- c) H i).
Lemma symHE_intcompn d :
E d = \sum_(c : intcompn d)
(-1)^+(d - size c) *: prod_gen H (partn_of_compn c).
Definition perm_partn d (la : 'P_d) :=
#|[set c : intcompn d | sort geq c == la]|.
Lemma symHE_intpartn d :
E d = \sum_(la : 'P_d)
(-1)^+(d - size la) * (perm_partn la)%:R *: prod_gen H la.
End HandE.
Lemma syme_symhE (d : nat) :
d != 0%N ->
'e_d = \sum_(1 <= i < d.+1) 'h_i * ((-1) ^+ i.-1 *: 'e_(d - i)) :> SF.
Lemma symh_symeE (d : nat) :
d != 0%N ->
'h_d = \sum_(1 <= i < d.+1) 'e_i * ((-1) ^+ i.-1 *: 'h_(d - i)) :> SF.
Lemma syme_to_symh d :
'e_d = \sum_(la : 'P_d)
(-1) ^+ (d - size la) * (perm_partn la)%:R *: 'h[la] :> SF.
Lemma symh_to_syme d :
'h_d = \sum_(la : 'P_d)
(-1) ^+ (d - size la) * (perm_partn la)%:R *: 'e[la] :> SF.
d != 0%N ->
\sum_(0 <= i < d.+1) (-1) ^+ i *: ('h_i * 'e_(d - i)) = 0 :> SF.
Lemma sum_syme_symh (d : nat) :
d != 0%N ->
\sum_(0 <= i < d.+1) (-1) ^+ i *: ('e_i * 'h_(d - i)) = 0 :> SF.
Section HandE.
Variable E H : nat -> {sympoly R[n]}.
Hypothesis E0 : E 0 = 1.
Hypothesis H0 : H 0 = 1.
Hypothesis Hanti : forall d : nat,
d != 0%N ->
\sum_(0 <= i < d.+1) (-1) ^+ i *: (H i * E (d - i)) = 0.
Lemma symHE_rec (d : nat) :
d != 0%N ->
E d = \sum_(1 <= i < d.+1) H i * ((-1) ^+ i.-1 *: E (d - i)).
Lemma symHE_prod_intcomp d :
E d = \sum_(c : intcompn d) (-1) ^+ (d - size c) *: (\prod_(i <- c) H i).
Lemma symHE_intcompn d :
E d = \sum_(c : intcompn d)
(-1)^+(d - size c) *: prod_gen H (partn_of_compn c).
Definition perm_partn d (la : 'P_d) :=
#|[set c : intcompn d | sort geq c == la]|.
Lemma symHE_intpartn d :
E d = \sum_(la : 'P_d)
(-1)^+(d - size la) * (perm_partn la)%:R *: prod_gen H la.
End HandE.
Lemma syme_symhE (d : nat) :
d != 0%N ->
'e_d = \sum_(1 <= i < d.+1) 'h_i * ((-1) ^+ i.-1 *: 'e_(d - i)) :> SF.
Lemma symh_symeE (d : nat) :
d != 0%N ->
'h_d = \sum_(1 <= i < d.+1) 'e_i * ((-1) ^+ i.-1 *: 'h_(d - i)) :> SF.
Lemma syme_to_symh d :
'e_d = \sum_(la : 'P_d)
(-1) ^+ (d - size la) * (perm_partn la)%:R *: 'h[la] :> SF.
Lemma symh_to_syme d :
'h_d = \sum_(la : 'P_d)
(-1) ^+ (d - size la) * (perm_partn la)%:R *: 'e[la] :> SF.
Lemma mult_symh_U k d i m :
(('h_k : {mpoly R[n]}) * 'X_i ^+ d)@_m =
((mdeg m == (k + d)%N) && (m i >= d))%:R.
Lemma mult_symh_powersum k d m :
('h_k * 'p_d : SF)@_m =
(mdeg m == (k + d)%N)%:R * \sum_(i < n) (m i >= d)%:R.
Lemma Newton_symh (k : nat) :
k%:R *: 'h_k = \sum_(0 <= i < k) 'h_i * 'p_(k - i) :> SF.
Lemma Newton_symh1 (k : nat) :
k%:R *: 'h_k = \sum_(1 <= i < k.+1) 'p_i * 'h_(k - i) :> SF.
Lemma mult_syme_U k d i m :
(('e_k : {mpoly R[n]}) * 'X_i ^+ d)@_m =
[&& mdeg m == (k + d)%N, (d <= m i <= d.+1) &
[forall j : 'I_n, (j != i) ==> (m j <= 1%N)]]%:R.
Lemma mul_ek_p1 (k : nat) :
'e_k.+1 * 'p_1 = k.+2%:R *: 'e_k.+2 + 'm[hookpartn k.+2 1] :> SF.
Lemma mul_ek_pk (k l : nat) :
'e_k.+1 * 'p_l.+2 =
'm[hookpartn (k + l).+3 l.+1] + 'm[hookpartn (k + l).+3 l.+2] :> SF.
Lemma expri2 i : (-1) ^+ i.+2 = (-1) ^+ i :> R.
Lemma Newton_syme1 (k : nat) :
k%:R *: 'e_k =
\sum_(1 <= i < k.+1) (-1) ^+ i.+1 *: 'p_i * 'e_(k - i) :> SF.
Lemma Newton_syme (k : nat) :
k%:R *: 'e_k =
\sum_(0 <= i < k) (-1) ^+ (k - i).+1 *: 'e_i * 'p_(k - i) :> SF.
End ChangeBasis.
(('h_k : {mpoly R[n]}) * 'X_i ^+ d)@_m =
((mdeg m == (k + d)%N) && (m i >= d))%:R.
Lemma mult_symh_powersum k d m :
('h_k * 'p_d : SF)@_m =
(mdeg m == (k + d)%N)%:R * \sum_(i < n) (m i >= d)%:R.
Lemma Newton_symh (k : nat) :
k%:R *: 'h_k = \sum_(0 <= i < k) 'h_i * 'p_(k - i) :> SF.
Lemma Newton_symh1 (k : nat) :
k%:R *: 'h_k = \sum_(1 <= i < k.+1) 'p_i * 'h_(k - i) :> SF.
Lemma mult_syme_U k d i m :
(('e_k : {mpoly R[n]}) * 'X_i ^+ d)@_m =
[&& mdeg m == (k + d)%N, (d <= m i <= d.+1) &
[forall j : 'I_n, (j != i) ==> (m j <= 1%N)]]%:R.
Lemma mul_ek_p1 (k : nat) :
'e_k.+1 * 'p_1 = k.+2%:R *: 'e_k.+2 + 'm[hookpartn k.+2 1] :> SF.
Lemma mul_ek_pk (k l : nat) :
'e_k.+1 * 'p_l.+2 =
'm[hookpartn (k + l).+3 l.+1] + 'm[hookpartn (k + l).+3 l.+2] :> SF.
Lemma expri2 i : (-1) ^+ i.+2 = (-1) ^+ i :> R.
Lemma Newton_syme1 (k : nat) :
k%:R *: 'e_k =
\sum_(1 <= i < k.+1) (-1) ^+ i.+1 *: 'p_i * 'e_(k - i) :> SF.
Lemma Newton_syme (k : nat) :
k%:R *: 'e_k =
\sum_(0 <= i < k) (-1) ^+ (k - i).+1 *: 'e_i * 'p_(k - i) :> SF.
End ChangeBasis.
Basis change from Schur to monomial
Section SymsSymmInt.
Variable (n : nat) (d : nat).
#[local] Notation SF := {sympoly int[n.+1]}.
Implicit Type (la mu : 'P_d).
Lemma syms_symm_int la :
's[la] = \sum_(mu : 'P_d) 'K(la, mu)%:R *: 'm[mu] :> SF.
Lemma syms_symm_partdom_int la :
's[la] =
'm[la] + \sum_(mu : 'PDom_d | (mu < la)%O) 'K(la, mu) *: 'm[mu] :> SF.
Lemma symm_syms_int la :
'm[la] = \sum_(mu : 'P_d) KostkaInv la mu *: 's[mu] :> SF.
Lemma symm_syms_partdom_int la :
'm[la] =
's[la] + \sum_(mu : 'PDom_d | (mu < la)%O) KostkaInv la mu *:'s[mu] :> SF.
End SymsSymmInt.
Section SymsSymm.
Variable (n : nat) (R : comRingType) (d : nat).
#[local] Notation SF := {sympoly R[n.+1]}.
Implicit Type (la mu : 'P_d).
Lemma syms_symm la :
's[la] = \sum_(mu : 'P_d) 'K(la, mu)%:R *: 'm[mu] :> SF.
Lemma syms_symm_partdom la :
's[la] =
'm[la] + \sum_(mu | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 'm[mu] :> SF.
Lemma symm_syms la :
'm[la] = \sum_(mu : 'P_d) 'K^-1(la, mu) *: 's[mu] :> SF.
Lemma symm_syms_partdom la :
'm[la] =
's[la] + \sum_(mu | (mu < la :> 'PDom_d)%O) 'K^-1(la, mu) *: 's[mu] :> SF.
End SymsSymm.
Variable (n : nat) (d : nat).
#[local] Notation SF := {sympoly int[n.+1]}.
Implicit Type (la mu : 'P_d).
Lemma syms_symm_int la :
's[la] = \sum_(mu : 'P_d) 'K(la, mu)%:R *: 'm[mu] :> SF.
Lemma syms_symm_partdom_int la :
's[la] =
'm[la] + \sum_(mu : 'PDom_d | (mu < la)%O) 'K(la, mu) *: 'm[mu] :> SF.
Lemma symm_syms_int la :
'm[la] = \sum_(mu : 'P_d) KostkaInv la mu *: 's[mu] :> SF.
Lemma symm_syms_partdom_int la :
'm[la] =
's[la] + \sum_(mu : 'PDom_d | (mu < la)%O) KostkaInv la mu *:'s[mu] :> SF.
End SymsSymmInt.
Section SymsSymm.
Variable (n : nat) (R : comRingType) (d : nat).
#[local] Notation SF := {sympoly R[n.+1]}.
Implicit Type (la mu : 'P_d).
Lemma syms_symm la :
's[la] = \sum_(mu : 'P_d) 'K(la, mu)%:R *: 'm[mu] :> SF.
Lemma syms_symm_partdom la :
's[la] =
'm[la] + \sum_(mu | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 'm[mu] :> SF.
Lemma symm_syms la :
'm[la] = \sum_(mu : 'P_d) 'K^-1(la, mu) *: 's[mu] :> SF.
Lemma symm_syms_partdom la :
'm[la] =
's[la] + \sum_(mu | (mu < la :> 'PDom_d)%O) 'K^-1(la, mu) *: 's[mu] :> SF.
End SymsSymm.
Basis change from complete and elementary to Schur
Section SymheSymsInt.
Variables (n : nat) (d : nat).
#[local] Notation SF := {sympoly int[n.+1]}.
Implicit Type la mu : 'P_d.
Lemma symh_syms_int mu :
'h[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la] :> SF.
Lemma symh_syms_partdom_int mu :
'h[mu] =
's[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la] :> SF.
Lemma syms_symh_int mu :
's[mu] = \sum_(la : 'P_d) KostkaInv la mu *: 'h[la] :> SF.
Lemma syms_symh_partdom_int mu :
's[mu] =
'h[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) KostkaInv la mu *: 'h[la] :> SF.
#[local] Notation "la '^~'" := (conj_intpartn la) (at level 10).
Lemma syme_syms_int mu :
'e[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la^~] :> SF.
Lemma syme_syms_partdom_int mu :
'e[mu] =
's[mu^~] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la^~] :> SF.
Lemma syms_syme_int mu :
's[mu^~] = \sum_(la : 'P_d) KostkaInv la mu *: 'e[la] :> SF.
Lemma syms_syme_partdom_int mu :
's[mu^~] =
'e[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) KostkaInv la mu *: 'e[la] :> SF.
End SymheSymsInt.
Section SymheSyms.
Variables (R : comRingType) (n : nat) (d : nat).
#[local] Notation SF := {sympoly R[n.+1]}.
Implicit Type la mu : 'P_d.
Lemma symh_syms mu : 'h[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la] :> SF.
Lemma symh_syms_partdom mu :
'h[mu] =
's[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la] :> SF.
Lemma syms_symh mu : 's[mu] = \sum_(la : 'P_d) 'K^-1(la, mu) *: 'h[la] :> SF.
Lemma syms_symh_partdom mu :
's[mu] =
'h[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K^-1(la, mu) *: 'h[la] :> SF.
#[local] Notation "la '^~'" := (conj_intpartn la) (at level 10).
Lemma syme_syms mu : 'e[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la ^~] :> SF.
Lemma syme_syms_partdom mu :
'e[mu] =
's[mu^~] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la^~] :> SF.
Lemma syms_syme mu : 's[mu^~] = \sum_(la : 'P_d) 'K^-1(la, mu) *: 'e[la] :> SF.
Lemma syms_syme_partdom mu :
's[mu^~] =
'e[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K^-1(la, mu) *: 'e[la] :> SF.
End SymheSyms.
Variables (n : nat) (d : nat).
#[local] Notation SF := {sympoly int[n.+1]}.
Implicit Type la mu : 'P_d.
Lemma symh_syms_int mu :
'h[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la] :> SF.
Lemma symh_syms_partdom_int mu :
'h[mu] =
's[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la] :> SF.
Lemma syms_symh_int mu :
's[mu] = \sum_(la : 'P_d) KostkaInv la mu *: 'h[la] :> SF.
Lemma syms_symh_partdom_int mu :
's[mu] =
'h[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) KostkaInv la mu *: 'h[la] :> SF.
#[local] Notation "la '^~'" := (conj_intpartn la) (at level 10).
Lemma syme_syms_int mu :
'e[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la^~] :> SF.
Lemma syme_syms_partdom_int mu :
'e[mu] =
's[mu^~] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la^~] :> SF.
Lemma syms_syme_int mu :
's[mu^~] = \sum_(la : 'P_d) KostkaInv la mu *: 'e[la] :> SF.
Lemma syms_syme_partdom_int mu :
's[mu^~] =
'e[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) KostkaInv la mu *: 'e[la] :> SF.
End SymheSymsInt.
Section SymheSyms.
Variables (R : comRingType) (n : nat) (d : nat).
#[local] Notation SF := {sympoly R[n.+1]}.
Implicit Type la mu : 'P_d.
Lemma symh_syms mu : 'h[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la] :> SF.
Lemma symh_syms_partdom mu :
'h[mu] =
's[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la] :> SF.
Lemma syms_symh mu : 's[mu] = \sum_(la : 'P_d) 'K^-1(la, mu) *: 'h[la] :> SF.
Lemma syms_symh_partdom mu :
's[mu] =
'h[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K^-1(la, mu) *: 'h[la] :> SF.
#[local] Notation "la '^~'" := (conj_intpartn la) (at level 10).
Lemma syme_syms mu : 'e[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la ^~] :> SF.
Lemma syme_syms_partdom mu :
'e[mu] =
's[mu^~] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K(la, mu) *: 's[la^~] :> SF.
Lemma syms_syme mu : 's[mu^~] = \sum_(la : 'P_d) 'K^-1(la, mu) *: 'e[la] :> SF.
Lemma syms_syme_partdom mu :
's[mu^~] =
'e[mu] + \sum_(la | (mu < la :> 'PDom_d)%O) 'K^-1(la, mu) *: 'e[la] :> SF.
End SymheSyms.
Section ChangeBasisSymhPowerSum.
Variable nvar0 : nat.
Variable R : fieldType.
#[local] Notation nvar := nvar0.+1.
#[local] Notation SF := {sympoly R[nvar]}.
Fixpoint prod_partsum (s : seq nat) :=
if s is _ :: s' then (sumn s * prod_partsum s')%N else 1%N.
#[local] Notation "\Pi s" := (prod_partsum s)%:R^-1 (at level 0, s at level 2).
Lemma symh_to_symp_prod_partsum n :
[char R] =i pred0 ->
'h_n = \sum_(c : intcompn n) \Pi c *: \prod_(i <- c) 'p_i :> SF.
Import LeqGeqOrder.
Lemma symh_to_symp_intpartn n :
[char R] =i pred0 ->
'h_n = \sum_(l : 'P_n)
(\sum_(c : intcompn n | perm_eq l c) \Pi c) *: 'p[l] :> SF.
Lemma intcompn_cons_sub_proof i n (c : intcompn (n - i)) :
i != 0%N -> i <= n -> is_comp_of_n n (i :: c).
#[local] Definition intcompn_cons i (Hi : i != 0%N) n (Hin : i <= n) c :=
IntCompN (intcompn_cons_sub_proof c Hi Hin).
Lemma intcompn_behead_sub_proof i n (c : intcompn n) :
i != 0%N -> i <= n ->
is_comp_of_n (n - i)%N (if head 0%N c == i then behead c else rowcompn (n-i)).
#[local] Definition intcompn_behead i (Hi : i != 0%N) n (Hin : i <= n) c :=
IntCompN (intcompn_behead_sub_proof c Hi Hin).
Lemma part_sumn_count l :
is_part l ->
(\sum_(i < (sumn l).+1 | val i \in l) i * (count_mem (val i) l))%N
= sumn l.
Lemma coeff_symh_to_symp n (l : 'P_n) :
[char R] =i pred0 ->
\sum_(c : intcompn n | perm_eq l c) \Pi c = (zcard l)%:R^-1 :> R.
Theorem symh_to_symp n :
[char R] =i pred0 -> 'h_n = \sum_(l : 'P_n) (zcard l)%:R^-1 *: 'p[l] :> SF.
End ChangeBasisSymhPowerSum.
Section Generators.
Variables (n : nat) (R : comRingType).
Lemma prod_homog nv l (df : 'I_l -> nat) (mf : 'I_l -> {mpoly R[nv]}) :
(forall i : 'I_l, mf i \is (df i).-homog) ->
\prod_(i < l) mf i \is (\sum_(i < l) df i).-homog.
Variable gen : forall nv : nat, nat -> {mpoly R[nv]}.
Hypothesis gen_homog : forall nv i : nat, gen nv i \is i.-homog.
#[local] Notation G nv := [tuple gen nv i.+1 | i < n].
Lemma homog_X_mPo_gen nv m : 'X_[m] \mPo G nv \is (mnmwgt m).-homog.
Lemma pihomog_mPo nv p d :
pihomog mdeg d (p \mPo G nv) = (pihomog mnmwgt d p) \mPo G nv.
End Generators.
Variable nvar0 : nat.
Variable R : fieldType.
#[local] Notation nvar := nvar0.+1.
#[local] Notation SF := {sympoly R[nvar]}.
Fixpoint prod_partsum (s : seq nat) :=
if s is _ :: s' then (sumn s * prod_partsum s')%N else 1%N.
#[local] Notation "\Pi s" := (prod_partsum s)%:R^-1 (at level 0, s at level 2).
Lemma symh_to_symp_prod_partsum n :
[char R] =i pred0 ->
'h_n = \sum_(c : intcompn n) \Pi c *: \prod_(i <- c) 'p_i :> SF.
Import LeqGeqOrder.
Lemma symh_to_symp_intpartn n :
[char R] =i pred0 ->
'h_n = \sum_(l : 'P_n)
(\sum_(c : intcompn n | perm_eq l c) \Pi c) *: 'p[l] :> SF.
Lemma intcompn_cons_sub_proof i n (c : intcompn (n - i)) :
i != 0%N -> i <= n -> is_comp_of_n n (i :: c).
#[local] Definition intcompn_cons i (Hi : i != 0%N) n (Hin : i <= n) c :=
IntCompN (intcompn_cons_sub_proof c Hi Hin).
Lemma intcompn_behead_sub_proof i n (c : intcompn n) :
i != 0%N -> i <= n ->
is_comp_of_n (n - i)%N (if head 0%N c == i then behead c else rowcompn (n-i)).
#[local] Definition intcompn_behead i (Hi : i != 0%N) n (Hin : i <= n) c :=
IntCompN (intcompn_behead_sub_proof c Hi Hin).
Lemma part_sumn_count l :
is_part l ->
(\sum_(i < (sumn l).+1 | val i \in l) i * (count_mem (val i) l))%N
= sumn l.
Lemma coeff_symh_to_symp n (l : 'P_n) :
[char R] =i pred0 ->
\sum_(c : intcompn n | perm_eq l c) \Pi c = (zcard l)%:R^-1 :> R.
Theorem symh_to_symp n :
[char R] =i pred0 -> 'h_n = \sum_(l : 'P_n) (zcard l)%:R^-1 *: 'p[l] :> SF.
End ChangeBasisSymhPowerSum.
Section Generators.
Variables (n : nat) (R : comRingType).
Lemma prod_homog nv l (df : 'I_l -> nat) (mf : 'I_l -> {mpoly R[nv]}) :
(forall i : 'I_l, mf i \is (df i).-homog) ->
\prod_(i < l) mf i \is (\sum_(i < l) df i).-homog.
Variable gen : forall nv : nat, nat -> {mpoly R[nv]}.
Hypothesis gen_homog : forall nv i : nat, gen nv i \is i.-homog.
#[local] Notation G nv := [tuple gen nv i.+1 | i < n].
Lemma homog_X_mPo_gen nv m : 'X_[m] \mPo G nv \is (mnmwgt m).-homog.
Lemma pihomog_mPo nv p d :
pihomog mdeg d (p \mPo G nv) = (pihomog mnmwgt d p) \mPo G nv.
End Generators.
Section MPoESymHomog.
Variables (n : nat) (R : comRingType).
#[local] Notation E nv := [tuple mesym nv R i.+1 | i < n].
Lemma mwmwgt_homogP (p : {mpoly R[n]}) d :
reflect
(forall nv, p \mPo E nv \is d.-homog)
(p \is d.-homog for mnmwgt).
Lemma sym_fundamental_homog (p : {mpoly R[n]}) (d : nat) :
p \is symmetric -> p \is d.-homog ->
{ t | t \mPo (E n) = p /\ t \is d.-homog for mnmwgt }.
End MPoESymHomog.
Section SymPolF.
Variable R : comRingType.
Variable m : nat.
Implicit Type p : {sympoly R[m]}.
#[local] Notation SF p := (sym_fundamental (sympolP p)).
Definition sympolyf p := let: exist t _ := SF p in t.
Fact sympolyf_is_linear : linear sympolyf.
Fact sympolyf_is_multiplicative : multiplicative sympolyf.
Variables (n : nat) (R : comRingType).
#[local] Notation E nv := [tuple mesym nv R i.+1 | i < n].
Lemma mwmwgt_homogP (p : {mpoly R[n]}) d :
reflect
(forall nv, p \mPo E nv \is d.-homog)
(p \is d.-homog for mnmwgt).
Lemma sym_fundamental_homog (p : {mpoly R[n]}) (d : nat) :
p \is symmetric -> p \is d.-homog ->
{ t | t \mPo (E n) = p /\ t \is d.-homog for mnmwgt }.
End MPoESymHomog.
Section SymPolF.
Variable R : comRingType.
Variable m : nat.
Implicit Type p : {sympoly R[m]}.
#[local] Notation SF p := (sym_fundamental (sympolP p)).
Definition sympolyf p := let: exist t _ := SF p in t.
Fact sympolyf_is_linear : linear sympolyf.
Fact sympolyf_is_multiplicative : multiplicative sympolyf.
Lemma sympolyfP p : (sympolyf p) \mPo [tuple sympol 'e_i.+1 | i < m] = p.
Definition sympolyf_eval : {mpoly R[m]} -> {sympoly R[m]} :=
mmap (GRing.in_alg {sympoly R[m]}) (fun i : 'I_m => 'e_i.+1).
Lemma sympolyf_evalE (q : {mpoly R[m]}) :
q \mPo [tuple sympol 'e_i.+1 | i < m] = sympolyf_eval q.
Lemma sympolyfK p : sympolyf_eval (sympolyf p) = p.
Lemma sympolyf_evalK q : sympolyf (sympolyf_eval q) = q.
Fact esympolyf_eval_is_linear : linear sympolyf_eval.
Fact esympolyf_eval_is_multiplicative : multiplicative sympolyf_eval.
Lemma sympolyf_evalX (i : 'I_m) : sympolyf_eval 'X_i = 'e_i.+1.
End SymPolF.
Section Omega.
Variable R : comRingType.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Implicit Type p : {sympoly R[n]}.
#[local] Notation SF p := (sym_fundamental (sympolP p)).
Fact omegasf_is_symmetric p :
(sympolyf p) \mPo [tuple sympol 'h_i.+1 | i < n] \is @symmetric n R.
Definition omegasf p : {sympoly R[n]} := SymPoly (omegasf_is_symmetric p).
Lemma val_omegasf p :
sympol (omegasf p) = (sympolyf p) \mPo [tuple sympol 'h_i.+1 | i < n].
Fact omegasf_is_linear : linear omegasf.
Fact omegasf_is_multiplicative : multiplicative omegasf.
Lemma omegasf_syme i : i <= n -> omegasf 'e_i = 'h_i.
Lemma omegasf_symh i : i <= n -> omegasf 'h_i = 'e_i.
Lemma omegasfK : involutive omegasf.
Lemma omegasf_symp i : 0 < i <= n -> omegasf 'p_i = (-1) ^+ i.+1 *: 'p_i.
Lemma omegasf_homog d :
{homo omegasf: p / sympol p \in [in R[n], d.-homog]}.
Lemma omegasf_homogE d :
{mono omegasf: p / sympol p \in [in R[n], d.-homog]}.
Notation S := ([tuple sympol 'h_i.+1 | i < n] : n.-tuple {mpoly R[n]}).
Notation E := ([tuple sympol 'e_i.+1 | i < n] : n.-tuple {mpoly R[n]}).
Lemma msym_fundamental_symh_un (t1 t2 : {mpoly R[n]}) :
t1 \mPo S = t2 \mPo S -> t1 = t2.
Lemma omegasf_sympolyf_eval q :
sympol (omegasf (sympolyf_eval q)) = q \mPo [tuple sympol 'h_i.+1 | i < n].
Lemma omegasf_compsymh p q :
(sympol p == q \mPo [tuple sympol 'h_i.+1 | i < n]) =
(sympol (omegasf p) == q \mPo [tuple sympol 'e_i.+1 | i < n]).
Lemma sym_fundamental_symh_homog (p : {mpoly R[n]}) (d : nat) :
p \is symmetric -> p \is d.-homog ->
{ t | t \mPo S = p /\ t \is d.-homog for mnmwgt }.
Lemma sym_fundamental_symh (p : {mpoly R[n]}) :
p \is symmetric -> { t | t \mPo S = p }.
Variable (d : nat).
Implicit Type (la : 'P_d).
Lemma omegasf_prodsyme la : head 0%N la <= n -> omegasf 'e[la] = 'h[la].
Lemma omegasf_prodsymh la : head 0%N la <= n -> omegasf 'h[la] = 'e[la].
Lemma exp1sumnDsize la :
(-1) ^+ (d - size la) = \prod_(i <- la) (-1) ^+ i.+1 :> R.
Lemma omegasf_prodsymp la :
head 0%N la <= n -> omegasf 'p[la] = (-1) ^+ (d - size la) *: 'p[la].
Lemma omegasf_syms la : d <= n -> omegasf 's[la] = 's[conj_intpartn la].
End Omega.
#[local] Close Scope Combi_scope.
Definition sympolyf_eval : {mpoly R[m]} -> {sympoly R[m]} :=
mmap (GRing.in_alg {sympoly R[m]}) (fun i : 'I_m => 'e_i.+1).
Lemma sympolyf_evalE (q : {mpoly R[m]}) :
q \mPo [tuple sympol 'e_i.+1 | i < m] = sympolyf_eval q.
Lemma sympolyfK p : sympolyf_eval (sympolyf p) = p.
Lemma sympolyf_evalK q : sympolyf (sympolyf_eval q) = q.
Fact esympolyf_eval_is_linear : linear sympolyf_eval.
Fact esympolyf_eval_is_multiplicative : multiplicative sympolyf_eval.
Lemma sympolyf_evalX (i : 'I_m) : sympolyf_eval 'X_i = 'e_i.+1.
End SymPolF.
Section Omega.
Variable R : comRingType.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Implicit Type p : {sympoly R[n]}.
#[local] Notation SF p := (sym_fundamental (sympolP p)).
Fact omegasf_is_symmetric p :
(sympolyf p) \mPo [tuple sympol 'h_i.+1 | i < n] \is @symmetric n R.
Definition omegasf p : {sympoly R[n]} := SymPoly (omegasf_is_symmetric p).
Lemma val_omegasf p :
sympol (omegasf p) = (sympolyf p) \mPo [tuple sympol 'h_i.+1 | i < n].
Fact omegasf_is_linear : linear omegasf.
Fact omegasf_is_multiplicative : multiplicative omegasf.
Lemma omegasf_syme i : i <= n -> omegasf 'e_i = 'h_i.
Lemma omegasf_symh i : i <= n -> omegasf 'h_i = 'e_i.
Lemma omegasfK : involutive omegasf.
Lemma omegasf_symp i : 0 < i <= n -> omegasf 'p_i = (-1) ^+ i.+1 *: 'p_i.
Lemma omegasf_homog d :
{homo omegasf: p / sympol p \in [in R[n], d.-homog]}.
Lemma omegasf_homogE d :
{mono omegasf: p / sympol p \in [in R[n], d.-homog]}.
Notation S := ([tuple sympol 'h_i.+1 | i < n] : n.-tuple {mpoly R[n]}).
Notation E := ([tuple sympol 'e_i.+1 | i < n] : n.-tuple {mpoly R[n]}).
Lemma msym_fundamental_symh_un (t1 t2 : {mpoly R[n]}) :
t1 \mPo S = t2 \mPo S -> t1 = t2.
Lemma omegasf_sympolyf_eval q :
sympol (omegasf (sympolyf_eval q)) = q \mPo [tuple sympol 'h_i.+1 | i < n].
Lemma omegasf_compsymh p q :
(sympol p == q \mPo [tuple sympol 'h_i.+1 | i < n]) =
(sympol (omegasf p) == q \mPo [tuple sympol 'e_i.+1 | i < n]).
Lemma sym_fundamental_symh_homog (p : {mpoly R[n]}) (d : nat) :
p \is symmetric -> p \is d.-homog ->
{ t | t \mPo S = p /\ t \is d.-homog for mnmwgt }.
Lemma sym_fundamental_symh (p : {mpoly R[n]}) :
p \is symmetric -> { t | t \mPo S = p }.
Variable (d : nat).
Implicit Type (la : 'P_d).
Lemma omegasf_prodsyme la : head 0%N la <= n -> omegasf 'e[la] = 'h[la].
Lemma omegasf_prodsymh la : head 0%N la <= n -> omegasf 'h[la] = 'e[la].
Lemma exp1sumnDsize la :
(-1) ^+ (d - size la) = \prod_(i <- la) (-1) ^+ i.+1 :> R.
Lemma omegasf_prodsymp la :
head 0%N la <= n -> omegasf 'p[la] = (-1) ^+ (d - size la) *: 'p[la].
Lemma omegasf_syms la : d <= n -> omegasf 's[la] = 's[conj_intpartn la].
End Omega.
#[local] Close Scope Combi_scope.
Section ChangeNVar.
Variable R : comRingType.
Variable m0 n0 : nat.
#[local] Notation m := m0.+1.
#[local] Notation n := n0.+1.
#[local] Notation SF p := (sym_fundamental (sympolP p)).
#[local] Notation E := [tuple sympol 'e_(i.+1) : {mpoly R[n]} | i < m].
Lemma cnvarsym_subproof (p : {sympoly R[m]}) : sympolyf p \mPo E \is symmetric.
Definition cnvarsym p : {sympoly R[n]} := SymPoly (cnvarsym_subproof p).
Fact cnvarsym_is_linear : linear cnvarsym.
Fact cnvarsym_is_multiplicative : multiplicative cnvarsym.
Lemma cnvar_leq_symeE i : i <= m -> cnvarsym 'e_i = 'e_i.
Lemma cnvar_syme i : (i <= m) || (n <= m) -> cnvarsym 'e_i = 'e_i.
Lemma cnvar_symh i : (i <= m) || (n <= m) -> cnvarsym 'h_i = 'h_i.
Lemma cnvar_symp i : (i < m) || (n <= m) -> cnvarsym 'p_i.+1 = 'p_i.+1.
Section ProdGen.
Variable Gen : forall nvar d : nat, {sympoly R[nvar]}.
Hypothesis Hcnvargen :
forall d : nat, (d < m) || (n <= m) -> cnvarsym (Gen m d.+1) = (Gen n d.+1).
Lemma cnvar_prodgen d (la : 'P_d) :
(d <= m) || (n <= m) ->
cnvarsym (prod_gen (Gen m) la) = prod_gen (Gen n) la.
End ProdGen.
Variable d : nat.
Hypothesis Hd : (d <= m) || (n <= m).
Lemma cnvar_prodsyme (la : 'P_d) : cnvarsym 'e[la] = 'e[la].
Lemma cnvar_prodsymh (la : 'P_d) : cnvarsym 'h[la] = 'h[la].
Lemma cnvar_prodsymp (la : 'P_d) : cnvarsym 'p[la] = 'p[la].
Lemma cnvar_syms (la : 'P_d) : cnvarsym 's[la] = 's[la].
Lemma cnvar_symm (la : 'P_d) : cnvarsym 'm[la] = 'm[la].
End ChangeNVar.
Section CategoricalSystems.
Variable R : comRingType.
Lemma cnvarsym_id n : @cnvarsym R n n =1 id.
Lemma cnvarsym_leq_trans m n p :
(m <= n) -> (n <= p) ->
@cnvarsym R n p \o @cnvarsym R m n =1 @cnvarsym R m p.
Lemma cnvarsym_geq_trans m n p :
(m >= n) -> (n >= p) ->
@cnvarsym R n p \o @cnvarsym R m n =1 @cnvarsym R m p.
End CategoricalSystems.
Variable R : comRingType.
Variable m0 n0 : nat.
#[local] Notation m := m0.+1.
#[local] Notation n := n0.+1.
#[local] Notation SF p := (sym_fundamental (sympolP p)).
#[local] Notation E := [tuple sympol 'e_(i.+1) : {mpoly R[n]} | i < m].
Lemma cnvarsym_subproof (p : {sympoly R[m]}) : sympolyf p \mPo E \is symmetric.
Definition cnvarsym p : {sympoly R[n]} := SymPoly (cnvarsym_subproof p).
Fact cnvarsym_is_linear : linear cnvarsym.
Fact cnvarsym_is_multiplicative : multiplicative cnvarsym.
Lemma cnvar_leq_symeE i : i <= m -> cnvarsym 'e_i = 'e_i.
Lemma cnvar_syme i : (i <= m) || (n <= m) -> cnvarsym 'e_i = 'e_i.
Lemma cnvar_symh i : (i <= m) || (n <= m) -> cnvarsym 'h_i = 'h_i.
Lemma cnvar_symp i : (i < m) || (n <= m) -> cnvarsym 'p_i.+1 = 'p_i.+1.
Section ProdGen.
Variable Gen : forall nvar d : nat, {sympoly R[nvar]}.
Hypothesis Hcnvargen :
forall d : nat, (d < m) || (n <= m) -> cnvarsym (Gen m d.+1) = (Gen n d.+1).
Lemma cnvar_prodgen d (la : 'P_d) :
(d <= m) || (n <= m) ->
cnvarsym (prod_gen (Gen m) la) = prod_gen (Gen n) la.
End ProdGen.
Variable d : nat.
Hypothesis Hd : (d <= m) || (n <= m).
Lemma cnvar_prodsyme (la : 'P_d) : cnvarsym 'e[la] = 'e[la].
Lemma cnvar_prodsymh (la : 'P_d) : cnvarsym 'h[la] = 'h[la].
Lemma cnvar_prodsymp (la : 'P_d) : cnvarsym 'p[la] = 'p[la].
Lemma cnvar_syms (la : 'P_d) : cnvarsym 's[la] = 's[la].
Lemma cnvar_symm (la : 'P_d) : cnvarsym 'm[la] = 'm[la].
End ChangeNVar.
Section CategoricalSystems.
Variable R : comRingType.
Lemma cnvarsym_id n : @cnvarsym R n n =1 id.
Lemma cnvarsym_leq_trans m n p :
(m <= n) -> (n <= p) ->
@cnvarsym R n p \o @cnvarsym R m n =1 @cnvarsym R m p.
Lemma cnvarsym_geq_trans m n p :
(m >= n) -> (n >= p) ->
@cnvarsym R n p \o @cnvarsym R m n =1 @cnvarsym R m p.
End CategoricalSystems.