proposition: Lemma extend_coherent_with S1 (tau1 : {additive 'CF(L) -> 'CF(G)}) chi phi a X : cfConjC_subset S1 S -> coherent_with S1 L^# tau tau1 -> [/\ phi \in S1, chi \in S & chi \notin S1] -> [/\ a \in Cint, chi 1%g = a * phi 1%g & '[X, a *: tau1 phi] = 0] -> tau (chi - a *: phi) = X - a *: tau1 phi -> coherent (chi :: chi^*%CF :: S1) L^# tau.
proof: Proof. set beta := _ - _ => sS10 cohS1 [S1phi Schi S1'chi] [Za chi1 oXaphi] tau_beta. have [[uS1 sS1S ccS1] [[Itau1 Ztau1] _]] := (sS10, cohS1). have [[N_S nrS ccS] ZItau _ R_P _] := cohS; have [Itau Ztau] := ZItau. have [Sphi [ZR o1R sumR]] := (sS1S _ S1phi, R_P _ Schi). have Zbeta: beta \in 'Z[S, L^#]. by rewrite zcharD1E !cfunE -chi1 subrr rpredB ?scale_zchar ?mem_zchar /=. have o_aphi_R: orthogonal (a *: tau1 phi) (R chi). have /orthogonalP oS1R := coherent_ortho_supp sS10 cohS1 Schi S1'chi. by apply/orthoPl=> xi Rxi; rewrite cfdotZl oS1R ?map_f ?mulr0. have /orthoPl o_chi_S1: orthogonal chi S1. by rewrite orthogonal_sym subset_ortho_subcoherent. have Zdchi: chi - chi^*%CF \in 'Z[S, L^#]. by rewrite sub_aut_zchar ?zchar_onG ?mem_zchar ?ccS // => xi /N_S/char_vchar. have [||_] := subcoherent_norm _ _ (erefl _) (And3 tau_beta oXaphi o_aphi_R). - rewrite Schi rpredZ_Cint ?char_vchar ?N_S /orthogonal //= !cfdotZr. by rewrite cfdot_conjCl !o_chi_S1 ?ccS1 // conjC0 !mulr0 !eqxx. - apply: sub_iso_to ZItau; [apply: zchar_trans_on; apply/allP | exact: zcharW]. by rewrite /= Zbeta Zdchi. case=> [|nX _ [e Re defX]]; first by rewrite !cfnormZ Itau1 ?mem_zchar. have uR: uniq (R chi) by have [] := orthonormalP o1R. have{uR} De: e = filter (mem e) (R chi) by apply/subseq_uniqP. pose ec := filter [predC e] (R chi); pose Xc := - \sum_(xi <- ec) xi. have defR: perm_eq (e ++ ec) (R chi) by rewrite De perm_filterC. pose S2 := chi :: chi^*%CF; pose X2 := X :: Xc. have{nrS} uS2: uniq S2 by rewrite /= andbT inE eq_sym (hasPn nrS). have sS20: cfConjC_subset S2 S. by split=> //; apply/allP; rewrite /= ?cfConjCK ?inE ?eqxx ?orbT // ccS Schi. have oS2: pairwise_orthogonal S2 by have [] := subset_subcoherent sS20. have nz_chi: chi != 0 by rewrite eq_sym; have [/norP[]] := andP oS2. have o_chi_chic: '[chi, chi^*] = 0 by have [_ /andP[/andP[/eqP]]] := and3P oS2. have def_XXc: X - Xc = tau (chi - chi^*%CF). by rewrite opprK defX -big_cat sumR; apply: perm_big. have oXXc: '[X, Xc] = 0. have /span_orthogonal o_e_ec: orthogonal e ec. by move: o1R; rewrite -(eq_orthonormal defR) orthonormal_cat => /and3P[]. by rewrite defX /Xc !big_seq o_e_ec ?rpredN ?rpred_sum // => xi /memv_span. have{o_chi_chic} nXc: '[Xc] = '[chi^*]. by apply: (addrI '[X]); rewrite -cfnormBd // nX def_XXc Itau // cfnormBd. have{oXXc} oX2: pairwise_orthogonal X2. rewrite /pairwise_orthogonal /= oXXc eqxx !inE !(eq_sym 0) -!cfnorm_eq0. by rewrite nX nXc cfnorm_conjC cfnorm_eq0 orbb nz_chi. have{nX nXc} nX2: map cfnorm X2 = map cfnorm S2 by congr [:: _; _]. have [|tau2 [tau2X tau2Xc] Itau2] := Zisometry_of_cfnorm oS2 oX2 nX2. apply/allP; rewrite /= defX De rpredN !big_seq. by rewrite !rpred_sum // => xi; rewrite mem_filter => /andP[_ /ZR]. have{Itau2} cohS2: coherent_with S2 L^# tau tau2. split=> // psi; rewrite zcharD1E => /andP[/zchar_expansion[//|z Zz ->]]. rewrite big_cons big_seq1 !cfunE/= conj_Cnat ?Cnat_char1 ?N_S // addrC addr_eq0. rewrite -mulNr (inj_eq (mulIf _)) ?char1_eq0 ?N_S // => /eqP->. by rewrite scaleNr -scalerBr !raddfZ_Cint // raddfB /= tau2X tau2Xc -def_XXc. have: tau beta = tau2 chi - tau1 (a *: phi) by rewrite tau2X raddfZ_Cint. apply: (bridge_coherent sS20 cohS2 sS10 cohS1) => //. by apply/hasPn; rewrite has_sym !negb_or S1'chi (contra (ccS1 _)) ?cfConjCK. by rewrite mem_head (zchar_on Zbeta) rpredZ_Cint ?mem_zchar. 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)