proposition: 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.
proof: Proof. Proof using Hd. have to_p (nu : 'P_d) : ('hsC[nu] : HSC) \in span 'hp. by rewrite (span_basis (symbp_basis Hd _)) //= memvf. have : \sum_(nu : 'P_d) 'hsC[nu](X) * 'hsC[nu](Y) = \sum_(nu : 'P_d) 'hp[nu](X) * ((zcard nu)%:R^-1 *: 'hp[nu](Y)). by rewrite -Cauchy_homsyms_homsyms Cauchy_homsymp_zhomsymp. have sum_coord (p : HSC) : \sum_i homsym (coord 'hp i p *: ('hp)`_i : HSC) = \sum_px coord 'hp (enum_rank px) p *: 'hp[px] :> pol. rewrite (reindex _ (onW_bij _ (@enum_rank_bij _))) /=. rewrite !linear_sum /=; apply eq_bigr => i _. rewrite (nth_map inh) /= -?enum_val_nth // ?enum_rankK //. by rewrite -cardE ltn_ord. rewrite (eq_bigr (fun nu : 'P_d => (\sum_px (coord 'hp (enum_rank px) 'hsC[nu]) *: 'hp[px])(X) * (\sum_py (coord 'hp (enum_rank py) 'hsC[nu]) *: 'hp[py])(Y) )); first last. move=> nu _; rewrite {1 2}(coord_span (to_p nu)). by rewrite linear_sum /= sum_coord. move=> {sum_coord to_p} /(congr1 (co_hpXY la mu)). rewrite !raddf_sum /= => /esym. rewrite (bigD1 la) //= -[(zcard la)%:R^-1 *: 'hp[la](Y)]linearZ /=. rewrite -![prod_gen _ _]/(homsym 'hp[_]). rewrite co_hprXYE linearZ co_hp_hp //. rewrite eq_refl mulr1 !mulrA divff ?mul1r; last by rewrite pnatr_eq0 neq0zcard. rewrite big1 ?addr0; first last => [nu /negbTE Hnu |]. rewrite -![prod_gen _ _]/(homsym 'hp[_]). rewrite -[(zcard nu)%:R^-1 *: 'hp[nu](Y)]linearZ /=. rewrite -![prod_gen _ _]/(homsym 'hp[_]). rewrite co_hprXYE linearZ co_hp_hp //. move: Hnu; rewrite -(inj_eq (@val_inj _ _ _)) /= => ->. by rewrite mulr0 !mul0r. rewrite /= co_hp_hp // => /(congr1 (fun x => (zcard la)%:R^-1 * x)). rewrite mulrA [X in X * _]mulrC divff; last by rewrite pnatr_eq0 neq0zcard. rewrite mul1r !mulr_sumr => -> . apply eq_bigr => nu _. rewrite co_hprXYE. have dot_sumhp (eta tau : 'P_d) : co_hp eta (\sum_px coord 'hp (enum_rank px) 'hsC[tau] *: 'hp[px]) = coord 'hp (enum_rank eta) 'hsC[tau] * (zcard eta)%:R. rewrite !raddf_sum /= (bigD1 eta) //=. rewrite -![prod_gen _ _]/(homsym 'hp[_]). rewrite linearZ /= co_hp_hp // eq_refl mulr1. rewrite big1 ?addr0 // => p => /negbTE Hp. rewrite -![prod_gen _ _]/(homsym 'hp[_]). rewrite linearZ /= co_hp_hp //. move: Hp; rewrite -(inj_eq (@val_inj _ _ _)) /= => ->. by rewrite !mulr0. rewrite !{}dot_sumhp ![_ * (zcard _)%:R]mulrC !mulrA. by rewrite ![_ * (zcard la)%:R]mulrC divff ?mul1r // pnatr_eq0 neq0zcard. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent