proposition: Lemma FTtype2_support_coherence : (u.-1 %/ q < h.-1 %/ e)%N -> (v.-1 %/ p < h.-1 %/ e)%N -> [/\ e = (p * q)%N & exists nb, exists2 chi, chi = tau1L phi \/ chi = - tau1L phi^*%CF & tauL betaL = \sum_ij (-1)^+ nb ij *: sigma 'chi_ij - chi].
proof: Proof. move=> ub_u ub_v; have nsHL : H <| L := gFnormal _ _. have pairST := of_typeP_pair maxS StypeP maxT TtypeP. have [//|frobL sUH defL] := FTtypeII_support_facts maxS StypeP _ pairST maxNU_L. have Ltype1 := FT_Frobenius_type1 maxL frobL. have irr_phi: phi \in irr L by apply: FTtype1_Ind_irr Lphi. have betaL_P := FTtypeI_bridge_facts _ _ Ltype1 cohL Lphi phi1. have e_dv_h1: e %| h.-1 by apply: Frobenius_ker_dvd_ker1. pose a i j := '[tauL betaL, sigma (w_ i j)]. have a0j j: j != 0 -> (a 0 j == 1 %[mod 2])%C. rewrite /a => nz_j; case/betaL_P: StypeP => _ _ -> //. by case=> [[_ /idPn[]] | [//]]; rewrite -natf_div // leC_nat -ltnNge. have ai0 i: i != 0 -> (a i 0 == 1 %[mod 2])%C. rewrite /a (cycTIisoC _ pddT) => nz_i; case/betaL_P: TtypeP => _ _ -> //. by case=> [[_ /idPn[]] | [//]]; rewrite -natf_div // leC_nat -ltnNge. have HbetaL: betaL \in 'CF(L, H^#) by apply: cfInd1_sub_lin_on Lphi phi1. have betaL_W_0: {in cyclicTIset defW, tauL betaL =1 \0}. move=> z; case/betaL_P: StypeP => tiAM_W _ _ _. rewrite !inE -(setCK W) inE => /andP[_]; apply: cfun_onP z. apply: cfun_onS (Dade_cfunS _ _); rewrite FT_DadeF_supportE -disjoints_subset. rewrite -FTsupp_Frobenius // -setI_eq0 -subset0 -tiAM_W setIS //. by rewrite setUC subsetU ?sub_class_support. have calL_gt1: (1 < size calL)%N. by apply: seqInd_nontrivial Lphi; rewrite ?mFT_odd. have [] := Dade_Ind1_sub_lin cohL calL_gt1 irr_phi Lphi phi1; rewrite -/betaL. rewrite -/calL odd_Frobenius_index_ler ?mFT_odd //= -/e -/h. case=> _ a00 ZbetaL [Gamma [o_tau1_Ga o_1_Ga [aa Zaa Dbeta] []// _ ubGa _]]. have{} a00: a 0 0 = 1 by rewrite /a /w_ cycTIirr00 cycTIiso1. have{a0j ai0} a_odd i j: (a i j == 1 %[mod 2%N])%C. have [[-> | /ai0 ai01] [-> | /a0j a0j1] //] := (eqVneq i 0, eqVneq j 0). by rewrite a00 (eqCmod_nat 2 1 1). by rewrite -(eqCmodDr _ 1) -{1}a00 cycTIiso_cfdot_exchange // eqCmodD. have [_ o_tauLeta _ _] := FTtypeI_bridge_facts _ StypeP Ltype1 cohL Lphi phi1. pose etaW := map sigma (irr W). have o1eta: orthonormal etaW := cycTIiso_orthonormal _. have [X etaX [Y [defGa oXY oYeta]]] := orthogonal_split etaW (Gamma + 1). have lbY: 0 <= '[Y] ?= iff (Y == 0). by split; rewrite ?cfnorm_ge0 // eq_sym cfnorm_eq0. have [b Db defX] := orthonormal_span o1eta etaX. do [rewrite addrC !addrA addrAC -addrA; set Z := _ - _] in Dbeta. have oZeta: orthogonal Z etaW. apply/orthoPl=> xi /memv_span; apply: {xi}(span_orthogonal o_tauLeta). rewrite rpredB ?rpredZ ?big_seq ?rpred_sum ?memv_span ?map_f // => xi Lxi. by rewrite rpredZ ?memv_span ?map_f. have lb_b ij (b_ij := b (sigma 'chi_ij)): 1 <= `|b_ij| ^+ 2 ?= iff [exists n : bool, b_ij == (-1) ^+ n]. - have /codomP[[i j] Dij] := dprod_Iirr_onto defW ij. have{b_ij} ->: b_ij = a i j. rewrite /a /w_ -Dij Dbeta defGa 2!cfdotDl. have ->: '[X, sigma 'chi_ij] = b_ij by rewrite /b_ij Db. by rewrite (orthoPl oYeta) ?(orthoPl oZeta) ?map_f ?mem_irr // !addr0. have Zaij: a i j \in Cint by rewrite Cint_cfdot_vchar ?cycTIiso_vchar. rewrite Cint_normK //; split. rewrite sqr_Cint_ge1 //; apply: contraTneq (a_odd i j) => ->. by rewrite (eqCmod_nat 2 0 1). apply/eqP/exists_eqP=> [a2_1|[n ->]]; last by rewrite sqrr_sign. rewrite (CintEsign Zaij) normC_def conj_Cint // -expr2 -a2_1 sqrtC1 mulr1. by exists (a i j < 0). have ub_e: e%:R <= #|Iirr W|%:R ?= iff (e == p * q)%N :> algC. rewrite leif_nat_r card_Iirr_cyclic //; last by have [] := ctiWG. rewrite -(dprod_card xdefW); apply: leqif_eq. case: defL => [|[y Qy]] defL; rewrite /e -(index_sdprod defL). by rewrite leq_pmull ?cardG_gt0. suffices /normP <-: y \in 'N(W1). by rewrite -conjYg !cardJg (dprodWY defW) -(dprod_card xdefW). have cQQ: abelian T`_\F by have [_ [/and3P[]]] := FTtypeP_facts maxT TtypeP. have sW1Q: W1 \subset T`_\F by have [_ _ _ []] := TtypeP. by rewrite (subsetP _ y Qy) // sub_abelian_norm. have /(_ predT) := leifD (leif_sum (in1W lb_b)) lbY. rewrite sumr_const addr0 => /(leif_trans ub_e)/ge_leif/esym. have ->: \sum_i `|b (sigma 'chi_i)| ^+ 2 = '[X]. rewrite defX cfnorm_sum_orthonormal // big_map (big_nth 0) big_mkord. by rewrite size_tuple; apply: eq_bigr => ij _; rewrite -tnth_nth. rewrite -cfnormDd // -defGa cfnormDd // cfnorm1 -lerBrDr ubGa. case/and3P=> /eqP-De /'forall_exists_eqP/fin_all_exists[/= n Dn] /eqP-Y0. pose chi := X - tauL betaL; split=> //; exists n, chi; last first. apply: canRL (addrK _) _; rewrite addrC subrK defX big_map (big_nth 0). by rewrite big_mkord size_tuple; apply: eq_bigr => ij; rewrite -tnth_nth Dn. have Z1chi: chi \in dirr G. rewrite dirrE rpredB //=; last first. rewrite defX big_map (big_nth 0) big_mkord size_tuple rpred_sum //= => ij. have [_ Zsigma] := cycTI_Zisometry ctiWG. by rewrite -tnth_nth Dn rpredZsign ?Zsigma ?irr_vchar. apply/eqP/(addIr '[X]); rewrite -cfnormBd; last first. rewrite /chi Dbeta defGa Y0 addr0 opprD addNKr cfdotNl. by rewrite (span_orthogonal oZeta) ?oppr0 // memv_span ?mem_head. rewrite addrAC subrr add0r cfnormN Dade_isometry // cfnormBd; last first. by rewrite cfdotC (seqInd_ortho_Ind1 _ _ Lphi) ?conjC0. rewrite cfnorm_Ind_cfun1 // -/e irrWnorm // addrC; congr (1 + _). rewrite defX cfnorm_sum_orthonormal // big_map big_tuple. rewrite De (dprod_card xdefW) -card_Iirr_cyclic //; last by have[]:= ctiWG. by rewrite -sumr_const; apply: eq_bigr => ij _; rewrite Dn normr_sign expr1n. have [[Itau1 Ztau1] Dtau1] := cohL. suffices /cfdot_add_dirr_eq1: '[tau1L phi - tau1L phi^*%CF, chi] = 1. rewrite -(cfConjC_Dade_coherent cohL) ?mFT_odd // rpredN dirr_aut. by apply; rewrite // dirrE Ztau1 ?Itau1 ?mem_zchar ?irrWnorm /=. rewrite cfdotBr (span_orthogonal o_tauLeta) ?add0r //; last first. by rewrite rpredB ?memv_span ?map_f ?cfAut_seqInd. have Zdphi := seqInd_sub_aut_zchar nsHL conjC Lphi. rewrite -raddfB Dtau1 ?zcharD1_seqInd // Dade_isometry ?(zchar_on Zdphi) //. rewrite cfdotBr !cfdotBl cfdot_conjCl cfAutInd rmorph1 irrWnorm //. rewrite (seqInd_ortho_Ind1 _ _ Lphi) // conjC0 subrr add0r opprK. by rewrite cfdot_conjCl (seqInd_conjC_ortho _ _ _ Lphi) ?mFT_odd ?conjC0 ?subr0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16 BGappendixC) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12 PFsection13)