proposition: Lemma FTtype1_subcoherent (R1 := sval R1gen) : {R : 'CF(L) -> seq 'CF(G) | [/\ subcoherent calS tau R, {in Iirr_kerD L H 1%G, forall i (phi := 'chi_i), [/\ orthonormal (R1 phi), size (R1 phi) = 2%N & tau (phi - phi^*%CF) = \sum_(mu <- R1 phi) mu]} & forall chi, R chi = flatten [seq R1 'chi_i | i in S_ chi]]}.
proof: Proof. have nrS: ~~ has cfReal calS by apply: seqInd_notReal; rewrite ?mFT_odd. have U_S: uniq calS by apply: seqInd_uniq. have ccS: cfConjC_closed calS by apply: cfAut_seqInd. have conjCS: cfConjC_subset calS (seqIndD H L H 1) by split. case: R1gen @R1 => /= R1 subc1. have [[chi_char nrI ccI] tau_iso oI h1 hortho] := subc1. pose R chi := flatten [seq R1 'chi_i | i in S_ chi]. have memI phi i: phi \in calS -> i \in S_ phi -> 'chi_i \in calI. by move=> Sphi Sphi_i; apply/image_f/FTtype1_irrP; exists phi. have aux phi psi i j mu nu: phi \in calS -> psi \in calS -> i \in S_ phi -> j \in S_ psi -> mu \in R1 'chi_i -> nu \in R1 'chi_j -> orthogonal 'chi_i ('chi_j :: ('chi_j)^*%CF) -> '[mu, nu] = 0. - move=> Sphi Spsi Sphi_i Spsi_j R1i_mu R1i_nu o_ij. apply: orthogonalP R1i_mu R1i_nu. by apply: hortho o_ij; [apply: memI Spsi Spsi_j | apply: memI Sphi Sphi_i]. exists R; split => //= => [| i Ii]; last first. have mem_i := mem_calI Ii; have{h1} [Zirr oR1 tau_im] := h1 _ mem_i. split=> //; apply/eqP; rewrite -eqC_nat -cfnorm_orthonormal // -{}tau_im. have ?: 'chi_i - ('chi_i)^*%CF \in 'Z[calI, L^#]. have hchi : 'chi_i \in 'Z[calI, L] by rewrite mem_zchar_on // cfun_onG. rewrite sub_aut_zchar ?cfAut_zchar // => _ /mapP[j _ ->]. exact: irr_vchar. have [-> // _] := tau_iso; rewrite cfnormBd ?cfnorm_conjC ?cfnorm_irr //. by have [_ ->] := pairwise_orthogonalP oI; rewrite ?ccI // eq_sym (hasPn nrI). have calS_portho : pairwise_orthogonal calS by apply: seqInd_orthogonal. have calS_char : {subset calS <= character} by apply: seqInd_char. have calS_chi_ortho : {in calS &, forall phi psi i j, i \in irr_constt phi -> j \in irr_constt psi -> '[phi, psi] = 0 -> '['chi_i, 'chi_j] = 0}. - by move=> phi psi Sphi Spsi /= i j; apply: constt_ortho_char; apply/calS_char. have ZisoS_tau: {in 'Z[calS, L^#], isometry tau, to 'Z[irr G, G^#]}. apply: (sub_iso_to _ _ (Dade_Zisometry _)) => // phi. have /subsetD1P[_ /setU1K <-] := FTsupp_sub L. rewrite zcharD1E zcharD1 => /andP[S_phi ->]; rewrite andbT. apply: zchar_trans_on phi S_phi => psi calS_psi. have [Dpsi _ hCF] := FTtype1_seqInd_facts calS_psi. by rewrite zchar_split (seqInd_vcharW calS_psi) /= Dpsi rpred_sum. split=> {ZisoS_tau}//= [phi calS_phi | phi psi calS_phi calS_psi]. rewrite /R /[seq _ | i in _]; set e := enum _; have: uniq e := enum_uniq _. have: all (mem (S_ phi)) e by apply/allP=> i; rewrite mem_enum. have ->: phi - phi^*%CF = \sum_(i <- e) ('chi_i - ('chi_i)^*%CF). rewrite big_filter sumrB -rmorph_sum. by have [<-] := FTtype1_seqInd_facts calS_phi. elim: e => /= [_ _ | i e IHe /andP[Si Se] /andP[e'i Ue]]. by rewrite !big_nil /tau linear0. rewrite big_cons [tau _]linearD big_cat /= -/tau orthonormal_cat. have{IHe Ue} [/allP Ze -> ->] := IHe Se Ue. have{} /h1[/allP Z_R1i -> -> /=] := memI _ _ calS_phi Si. split=> //; first by apply/allP; rewrite all_cat Z_R1i. apply/orthogonalP=> mu nu R1i_mu /flatten_mapP[j e_j R1j_nu]. have /= Sj := allP Se j e_j; apply: (aux phi phi i j) => //. rewrite /orthogonal /= !andbT !cfdot_irr mulrb ifN_eqC ?(memPn e'i) ?eqxx //=. rewrite !inE in Si Sj; rewrite -conjC_IirrE; set k := conjC_Iirr j. rewrite (calS_chi_ortho phi phi^*%CF) ?calS_char ?ccS //. by rewrite irr_consttE conjC_IirrE cfdot_conjC fmorph_eq0. by rewrite (seqInd_conjC_ortho _ _ _ calS_phi) ?mFT_odd. case/andP=> /and3P[/eqP opsi_phi /eqP opsi_phiC _] _; apply/orthogonalP. move=> nu mu /flatten_imageP[j Spsi_j R1j_nu] /flatten_imageP[i Sphi_i R1i_mu]. apply: (aux psi phi j i) => //; rewrite /orthogonal /= !andbT -conjC_IirrE. rewrite !inE in Sphi_i Spsi_j; rewrite (calS_chi_ortho psi phi) ?calS_char //. rewrite (calS_chi_ortho psi phi^*%CF) ?calS_char ?ccS ?eqxx //. by rewrite irr_consttE conjC_IirrE cfdot_conjC fmorph_eq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)