proposition: Lemma FtypeI_invDade_ortho_constant (psi : 'CF(G)) : {in calS, forall phi, orthogonal psi (R phi)} -> {in H :\: H' &, forall x y, rho psi x = rho psi y}.
proof: Proof. have [nsH'H nsHL]: H' <| H /\ H <| L by rewrite !gFnormal. have [[sH'H _] [sHL _]] := (andP nsH'H, andP nsHL). case: (Rgen _ _) @R => /= rR [scohS _ _] opsiR; set rpsi := rho psi. have{rR scohS opsiR} o_rpsi_S xi1 xi2: xi1 \in calS -> xi2 \in calS -> xi1 1%g = xi2 1%g -> '[rpsi, xi1 - xi2] = 0. - move=> Sxi1 Sxi2 /eqP deg12. have [calS2 [S2xi1 S2xi2]] := pair_degree_coherence scohS Sxi1 Sxi2 deg12. move=> ccsS2S [tau2 cohS2]; have [[_ Dtau2] [_ sS2S _]] := (cohS2, ccsS2S). have{deg12} L1xi12: (xi1 - xi2) 1%g == 0 by rewrite !cfunE subr_eq0. have{ccsS2S cohS2} tau2E := mem_coherent_sum_subseq scohS ccsS2S cohS2. have o_psi_tau2 xi: xi \in calS2 -> '[psi, tau2 xi] = 0. move=> S2xi; have [e /mem_subseq Re ->] := tau2E xi S2xi. by rewrite cfdot_sumr big1_seq // => _ /Re/orthoPl->; rewrite ?opsiR ?sS2S. have A1xi12: xi1 - xi2 \in 'CF(L, H^#). by rewrite (@zchar_on _ _ calS) ?zcharD1 ?rpredB ?seqInd_zchar. rewrite cfdotC -invDade_reciprocity // -cfdotC. rewrite FT_DadeF_E -?FT_DadeE ?(cfun_onS (Fcore_sub_FTsupp maxL)) //. rewrite -Dtau2; last by rewrite zcharD1E rpredB ?mem_zchar. by rewrite !raddfB /= !o_psi_tau2 ?subrr. pose P_ i : {set Iirr H} := [set j in irr_constt ('Ind[H, H'] 'chi_i)]. pose P : {set {set Iirr H}} := [set P_ i | i : Iirr H']. have tiP: trivIset P. apply/trivIsetP=> _ _ /imsetP[i1 _ ->] /imsetP[i2 _ ->] chi2'1. apply/pred0P=> j; rewrite !inE; apply: contraNF chi2'1 => /andP[i1Hj i2Hj]. case: ifP (cfclass_Ind_cases i1 i2 nsH'H) => _; first by rewrite /P_ => ->. have NiH i: 'Ind[H,H'] 'chi_i \is a character by rewrite cfInd_char ?irr_char. case/(constt_ortho_char (NiH i1) (NiH i2) i1Hj i2Hj)/eqP/idPn. by rewrite cfnorm_irr oner_eq0. have coverP: cover P =i predT. move=> j; apply/bigcupP; have [i jH'i] := constt_cfRes_irr H' j. by exists (P_ i); [apply: imset_f | rewrite inE constt_Ind_Res]. have /(all_sig_cond 0)[lambda lambdaP] A: A \in P -> {i | A = P_ i}. by case/imsetP/sig2_eqW=> i; exists i. pose theta A : Iirr H := odflt 0 [pick j in A :\ 0]; pose psiH := 'Res[H] rpsi. pose a_ A := '[psiH, 'chi_(theta A)] / '['Ind 'chi_(lambda A), 'chi_(theta A)]. pose a := '[psiH, 1 - 'chi_(theta (pblock P 0))]. suffices Da: {in H :\: H', rpsi =1 (fun=> a)} by move=> /= *; rewrite !Da. suffices DpsiH: psiH = \sum_(A in P) a_ A *: 'Ind 'chi_(lambda A) + a%:A. move=> x /setDP[Hx notH'x]; transitivity (psiH x); first by rewrite cfResE. rewrite DpsiH !cfunE sum_cfunE cfun1E Hx mulr1 big1 ?add0r // => A _. by rewrite cfunE (cfun_onP (cfInd_normal _ _)) ?mulr0. apply: canRL (subrK _) _; rewrite [_ - _]cfun_sum_cfdot. rewrite -(eq_bigl _ _ coverP) big_trivIset //=; apply: eq_bigr => A P_A. rewrite {}/a_; set i := lambda A; set k := theta A; pose Ii := 'I_H['chi_i]%G. have /cfInd_central_Inertia[//|e _ [DiH _ DiH_1]]: abelian (Ii / H'). by rewrite (abelianS _ (der_abelian 0 H)) ?quotientS ?subsetIl. have defA: A = P_ i := lambdaP A P_A. have Ak: k \in A; last 1 [have iHk := Ak; rewrite defA inE in Ak]. have [j iHj] := constt_cfInd_irr i sH'H. rewrite {}/k /theta; case: pickP => [k /setDP[]//| /(_ j)/=]. by rewrite defA !in_set iHj andbT => /negbFE/set1P <-. have{} DiH: 'Ind 'chi_i = e *: \sum_(j in A) 'chi_j. by congr (_ = _ *: _): DiH; apply: eq_bigl => j; rewrite [in RHS]defA !inE. rewrite {2}DiH; have{DiH} ->: e = '['Ind 'chi_i, 'chi_k]. rewrite DiH cfdotZl cfdot_suml (bigD1 k) //= cfnorm_irr big1 ?addr0 ?mulr1 //. by move=> j /andP[_ k'j]; rewrite cfdot_irr (negPf k'j). rewrite scalerA scaler_sumr divfK //; apply: eq_bigr => j Aj; congr (_ *: _). rewrite cfdotBl cfdotZl -irr0 cfdot_irr mulr_natr mulrb eq_sym. apply/(canLR (addrK _))/(canRL (addNKr _)); rewrite addrC -cfdotBr. have [j0 | nzj] := altP eqP; first by rewrite j0 irr0 /a -j0 (def_pblock _ P_A). have iHj := Aj; rewrite defA inE in iHj; rewrite cfdot_Res_l linearB /=. do [rewrite o_rpsi_S ?cfInd1 ?DiH_1 //=; apply/seqIndC1P]; first by exists j. by exists k; rewrite // /k /theta; case: pickP => [? | /(_ j)] /setD1P[]. 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)