proposition: Lemma uniform_degree_coherence : constant [seq chi 1%g | chi : 'CF(L) <- S] -> coherent S L^# tau.
proof: Proof. case defS: {1}S => /= [|chi1 S1] szS; first by rewrite defS; apply nil_coherent. have{szS} unifS xi: xi \in S -> xi 1%g = chi1 1%g. by rewrite defS => /predU1P[-> // | S'xi]; apply/eqP/(allP szS)/map_f. have{S1 defS} Schi1: chi1 \in S by rewrite defS mem_head. have [[N_S nrS ccS] IZtau oS R_P oR] := cohS; have [Itau Ztau] := IZtau. have Zd: {in S &, forall xi1 xi2, xi1 - xi2 \in 'Z[S, L^#]}. move=> xi1 xi2 Sxi1 Sxi2 /=. by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE !unifS ?subrr. pose chi2 := chi1^*%CF; have Schi2: chi2 \in S by rewrite ccS. have ch1'2: chi2 != chi1 by apply/(hasPn nrS). have [_ oSS] := pairwise_orthogonalP oS. pose S1 xi := [predD1 S & xi]; pose S2 xi := [predD1 (S1 xi) & xi^*%CF]. have{} oR xi1 xi2: xi1 \in S -> xi2 \in S2 xi1 -> orthogonal (R xi1) (R xi2). move=> Sxi1 /and3P[/= xi1J'2 xi1'2 Sxi2]. by rewrite orthogonal_sym oR // /orthogonal /= !oSS ?eqxx // ccS. have oSc xi: xi \in S -> '[xi, xi^*] = 0. by move=> Sxi; rewrite oSS ?ccS // eq_sym (hasPn nrS). pose D xi := tau (chi1 - xi). have Z_D xi: xi \in S -> D xi \in 'Z[irr G] by move/(Zd _ _ Schi1)/Ztau/zcharW. have /CnatP[N defN]: '[chi1] \in Cnat by rewrite Cnat_cfdot_char ?N_S. have dotD: {in S1 chi1 &, forall xi1 xi2, '[D xi1, D xi2] = N%:R + '[xi1, xi2]}. move=> xi1 xi2 /andP[ch1'xi1 Sxi1] /andP[chi1'xi2 Sxi2]. rewrite Itau ?Zd // cfdotBl !cfdotBr defN. by rewrite 2?oSS // 1?eq_sym // opprB !subr0. have /R_P[ZRchi oRchi defRchi] := Schi1. have szRchi: size (R chi1) = (N + N)%N. apply: (can_inj natCK); rewrite -cfnorm_orthonormal // -defRchi. by rewrite dotD ?inE ?ccS ?(hasPn nrS) // cfnorm_conjC defN -natrD. pose subRchi1 X := exists2 E, subseq E (R chi1) & X = \sum_(a <- E) a. pose Xspec X := [/\ X \in 'Z[R chi1], '[X] = N%:R & subRchi1 X]. pose Xi_spec (X : 'CF(G)) xi := X - D xi \in 'Z[R xi] /\ '[X, D xi] = N%:R. have haveX xi: xi \in S2 chi1 -> exists2 X, Xspec X & Xi_spec X xi. move=> S2xi; have /and3P[/= chi2'xi ch1'xi Sxi] := S2xi. have [neq_xi' Sxi'] := (hasPn nrS xi Sxi, ccS xi Sxi). have [X RchiX [Y1 defXY1]] := subcoherent_split Schi1 (Z_D _ Sxi). have [[eqXY1 oXY1 oY1chi] sRchiX] := (defXY1, zchar_span RchiX). have Z_Y1: Y1 \in 'Z[irr G]. by rewrite -rpredN -(rpredDl _ (zchar_trans ZRchi RchiX)) -eqXY1 Z_D. have [X1 RxiX1 [Y defX1Y]] := subcoherent_split Sxi Z_Y1. have [[eqX1Y oX1Y oYxi] sRxiX1] := (defX1Y, zchar_span RxiX1). pose Y2 : 'CF(G) := X + Y; pose D2 : 'CF(G) := tau (xi - chi1). have oY2Rxi: orthogonal Y2 (R xi). apply/orthoPl=> phi Rxi_phi; rewrite cfdotDl (orthoPl oYxi) // addr0. by rewrite (span_orthogonal (oR chi1 xi _ _)) // memv_span. have{oY2Rxi} defX1Y2: [/\ D2 = X1 - Y2, '[X1, Y2] = 0 & orthogonal Y2 (R xi)]. rewrite -opprB -addrA -opprB -eqX1Y -eqXY1 -linearN opprB cfdotC. by rewrite (span_orthogonal oY2Rxi) ?conjC0 ?memv_span1 ?(zchar_span RxiX1). have [||minX eqX1] := subcoherent_norm _ _ (erefl _) defXY1. - by rewrite char_vchar ?N_S /orthogonal //= !oSS ?eqxx // eq_sym. - apply: sub_iso_to IZtau; last exact: zcharW. by apply: zchar_trans_on; apply/allP; rewrite /= !Zd. have [||minX1 _]:= subcoherent_norm _ _ (erefl _) defX1Y2. - rewrite char_vchar ?N_S /orthogonal //= !oSS ?eqxx // inv_eq //. exact: cfConjCK. - apply: sub_iso_to IZtau; last exact: zcharW. by apply: zchar_trans_on; apply/allP; rewrite /= !Zd. rewrite eqX1Y cfnormBd // defN in eqX1. have{eqX1} [|nX n_xi defX] := eqX1; first by rewrite ler_wpDr ?cfnorm_ge0. exists X => //; split; last by rewrite eqXY1 cfdotBr oXY1 subr0. suffices Y0: Y = 0 by rewrite eqXY1 eqX1Y Y0 subr0 opprB addrC subrK. apply/eqP; rewrite -cfnorm_eq0 leif_le ?cfnorm_ge0 //. by rewrite -(lerD2l '[X1]) addr0 n_xi. pose XDspec X := {in S2 chi1, forall xi, '[X, D xi] = N%:R}. have [X [RchiX nX defX] XD_N]: exists2 X, Xspec X & XDspec X. have [sSchi | /allPn[xi1 Sxi1]] := altP (@allP _ (pred2 chi1 chi2) S). pose E := take N (R chi1). exists (\sum_(a <- E) a) => [|xi]; last by case/and3P=> ? ? /sSchi/norP[]. have defE: E ++ drop N (R chi1) = R chi1 by rewrite cat_take_drop. have sER: subseq E (R chi1) by rewrite -defE prefix_subseq. split; last by [exists E]; move/mem_subseq in sER. by rewrite big_seq rpred_sum // => a Ea; rewrite mem_zchar ?sER. rewrite cfnorm_orthonormal ?size_takel ?szRchi ?leq_addl //. by have:= oRchi; rewrite -defE orthonormal_cat => /andP[]. case/norP=> chi1'xi1 chi2'xi1'; have S2xi1: xi1 \in S2 chi1 by apply/and3P. pose xi2 := xi1^*%CF; have /haveX[X [RchiX nX defX] [Rxi1X1 XD_N]] := S2xi1. exists X => // xi S2xi; have [chi1'xi chi2'xi /= Sxi] := and3P S2xi. have /R_P[_ _ defRxi1] := Sxi1; have [-> // | xi1'xi] := eqVneq xi xi1. have [sRchiX sRxi1X1] := (zchar_span RchiX, zchar_span Rxi1X1). have [-> | xi2'xi] := eqVneq xi xi2. rewrite /D -[chi1](subrK xi1) -[_ + _ - _]addrA. rewrite linearD cfdotDr XD_N defRxi1 big_seq. rewrite (span_orthogonal (oR chi1 xi1 _ _)) ?addr0 ?rpred_sum //. exact/memv_span. have /haveX[X' [RchiX' nX' _] [Rxi3X' X'D_N]] := S2xi. have [sRchiX' sRxi1X'] := (zchar_span RchiX', zchar_span Rxi3X'). suffices: '[X - X'] == 0 by rewrite cfnorm_eq0 subr_eq0 => /eqP->. have ZXX': '[X, X'] \in Cint by rewrite Cint_cfdot_vchar ?(zchar_trans ZRchi). rewrite cfnormB subr_eq0 nX nX' aut_Cint {ZXX'}//; apply/eqP/esym. congr (_ *+ 2); rewrite -(addNKr (X - D xi1) X) cfdotDl cfdotC. rewrite (span_orthogonal (oR chi1 xi1 _ _)) // conjC0. rewrite -(subrK (D xi) X') cfdotDr cfdotDl cfdotNl opprB subrK. rewrite (span_orthogonal (oR xi1 xi _ _)) //; last exact/and3P. rewrite (span_orthogonal (oR chi1 xi _ _)) // oppr0 !add0r. by rewrite dotD ?oSS ?addr0 1?eq_sym //; apply/andP. have{RchiX} ZX: X \in 'Z[irr G] := zchar_trans ZRchi RchiX. apply: (pivot_coherence cohS Schi1 ZX); rewrite defN //. move=> xi /andP[chi1'xi Sxi]; exists 1; first by rewrite rpred1 mul1r unifS. rewrite scale1r mulN1r -conjC_nat -opprB raddfN cfdotNl cfdotC; congr (- _^*). have [-> /= | chi2'xi] := eqVneq xi chi2; last exact/XD_N/and3P. have{defX}[E ssER defX] := defX; pose Ec := filter [predC E] (R chi1). have eqRchi: perm_eq (R chi1) (E ++ Ec). rewrite -(perm_filterC (mem E)) -(subseq_uniqP _ _) //. exact/free_uniq/orthonormal_free. have /and3P[oE _ oEEc]: [&& orthonormal E, orthonormal Ec & orthogonal E Ec]. by rewrite (eq_orthonormal eqRchi) orthonormal_cat in oRchi. rewrite defRchi (perm_big _ eqRchi) big_cat -defX cfdotDr nX defX !big_seq. by rewrite (span_orthogonal oEEc) ?addr0 ?rpred_sum //; apply: memv_span. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)