proposition: Lemma irr_subcoherent (L G : {group gT}) S tau : cfConjC_subset S (irr L) -> ~~ has cfReal S -> {in 'Z[S, L^#], isometry tau, to 'Z[irr G, G^#]} -> {R | subcoherent S tau R}.
proof: Proof. case=> uniqS irrS ccS nrS [isoL Ztau]. have N_S: {subset S <= character} by move=> _ /irrS/irrP[i ->]; apply: irr_char. have Z_S: {subset S <= 'Z[irr L]} by move=> chi /N_S/char_vchar. have o1S: orthonormal S by apply: sub_orthonormal (irr_orthonormal L). have [[_ dotSS] oS] := (orthonormalP o1S, orthonormal_orthogonal o1S). pose beta chi := tau (chi - chi^*%CF); pose eqBP := _ =P beta _. have Zbeta: {in S, forall chi, chi - (chi^*)%CF \in 'Z[S, L^#]}. move=> chi Schi; rewrite /= zcharD1E rpredB ?mem_zchar ?ccS //= !cfunE. by rewrite subr_eq0/= conj_Cnat // Cnat_char1 ?N_S. pose sum_beta chi R := \sum_(alpha <- R) alpha == beta chi. pose Zortho R := all (mem 'Z[irr G]) R && orthonormal R. have R chi: {R : 2.-tuple 'CF(G) | (chi \in S) ==> sum_beta chi R && Zortho R}. apply: sigW; case Schi: (chi \in S) => /=; last by exists [tuple 0; 0]. move/(_ _ Schi) in Zbeta; have /irrP[i def_chi] := irrS _ Schi. have: '[beta chi] = 2%:R. rewrite isoL // cfnormBd ?dotSS ?ccS ?eqxx // eq_sym -/(cfReal _). by rewrite (negPf (hasPn nrS _ _)). case/zchar_small_norm; rewrite ?(zcharW (Ztau _ _)) // => R [oR ZR sumR]. by exists R; apply/and3P; split; [apply/eqP | apply/allP | ]. exists (fun xi => val (val (R xi))); split=> // [chi Schi | chi phi Schi Sphi]. by case: (R chi) => Rc /=; rewrite Schi => /and3P[/eqBP-> /allP]. case/andP => /and3P[/=/eqP-opx /eqP-opx' _] _. have{opx opx'} obpx: '[beta phi, beta chi] = 0. rewrite isoL ?Zbeta // cfdotBl !cfdotBr -{3}[chi]cfConjCK. by rewrite !cfdot_conjC opx opx' rmorph0 !subr0. case: (R phi) => [[[|a [|b []]] //= _]]. rewrite Sphi => /and3P[/eqBP sum_ab Zab o_ab]. case: (R chi) => [[[|c [|d []]] //= _]]. rewrite Schi => /and3P[/eqBP-sum_cd Zcd o_cd]. suffices: orthonormal [:: a; - b; c; d]. rewrite (orthonormal_cat [:: a; _]) => /and3P[_ _]. by rewrite /orthogonal /= !cfdotNl !oppr_eq0. apply: vchar_pairs_orthonormal 1 (-1) _ _ _ _. - by split; apply/allP; rewrite //= rpredN. - by rewrite o_cd andbT /orthonormal/= cfnormN /orthogonal /= cfdotNr !oppr_eq0. - by rewrite oppr_eq0 oner_eq0 rpredN rpred1. rewrite !(big_seq1, big_cons) in sum_ab sum_cd. rewrite scale1r scaleN1r !opprK sum_ab sum_cd obpx eqxx /=. by rewrite !(cfun_on0 (zchar_on (Ztau _ _))) ?Zbeta ?inE ?eqxx. 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)