proposition: Lemma FTtypeI_bridge_facts : [/\ 'A~(L) :&: (class_support P G :|: class_support W G) = set0, orthogonal (map tau1 calL) (map sigma (irr W)), forall j, j != 0 -> '[tauL betaL, eta_ 0 j] = '[tauL betaL, eta01] & ('[tau betaS, tau1 phi] == 1 %[mod 2])%C /\ #|H|.-1%:R / e%:R <= (u.-1 %/ q)%:R :> algC \/ ('[tauL betaL, eta01] == 1 %[mod 2])%C /\ (p <= e)%N].
proof: Proof. have nsHL: H <| L := gFnormal _ L; have [sHL nHL] := andP nsHL. have coHr T r: T \in 'M -> FTtype T != 1%N -> r.-abelem T`_\F -> coprime #|H| r. move=> maxT notTtype1 /andP[rR _]. have [_ _ [n oR]] := pgroup_pdiv rR (mmax_Fcore_neq1 maxT). rewrite -(coprime_pexpr _ r (ltn0Sn n)) -oR /= -FTcore_type1 //. apply: coprimegS (Fcore_sub_FTcore maxT) _. have [_ -> //] := FT_Dade_support_partition gT. by apply: contra notTtype1 => /imsetP[y _ ->] /=; rewrite FTtypeJ. have coHp: coprime #|H| p by apply: (coHr S) => //; have [_ []] := Sfacts. have{coHr} coHq: coprime #|H| q. have [T pairST [xdefW [V TtypeP]]] := FTtypeP_pair_witness maxS StypeP. have [[_ _ maxT] _ _ _ _] := pairST; have Ttype'1 := FTtypeP_neq1 maxT TtypeP. by rewrite (coHr T) ?Ttype'1 //; have [_ []] := FTtypeP_facts maxT TtypeP. have defA: 'A(L) = H^# := FTsupp_Frobenius maxL frobL. set PWG := class_support P G :|: class_support W G. have tiA_PWG: 'A~(L) :&: PWG = set0. apply/setP=> x; rewrite !inE; apply/andP=> [[Ax PWGx]]. suffices{Ax}: \pi(H)^'.-elt x. have [y Ay /imset2P[_ t /rcosetP[z Rz ->] _ ->]] := bigcupP Ax => H'zyt. do [rewrite -def_FTsignalizer //; set ddL := FT_Dade_hyp maxL] in Rz. have /setD1P[nty Hy]: y \in H^# by rewrite -defA. have /idPn[]: (z * y).`_\pi('C_H[y]) == 1%g. rewrite (constt1P _) // -(p_eltJ _ _ t); apply: sub_in_pnat H'zyt => r _. by apply: contra; apply: piSg; apply: subsetIl. rewrite consttM; last first. exact: cent1P (subsetP (Dade_signalizer_cent _ y) z Rz). rewrite (constt1P (mem_p_elt _ Rz)) ?mul1g; last first. rewrite /pgroup -coprime_pi' ?cardG_gt0 // coprime_sym. by rewrite (coprimegS _ (Dade_coprime _ Ay Ay)) ?setSI. by rewrite (constt_p_elt (mem_p_elt (pgroup_pi _) _)) // inE Hy cent1id. suffices /pnat_dvd: #[x] %| #|P| * #|W|. have [_ [_ ->] _ _ _] := Sfacts; rewrite -(dprod_card defW) -/p -/q. by apply; rewrite !pnatM pnatX -!coprime_pi' ?cardG_gt0 ?coHp ?coHq. case/orP: PWGx => /imset2P[y z PWy _ ->]; rewrite {z}orderJ. by rewrite dvdn_mulr ?order_dvdG. by rewrite dvdn_mull ?order_dvdG. have ZsubL psi: psi \in calL -> psi - psi^*%CF \in 'Z[calL, L^#]. have ZcalL: {subset calL <= 'Z[irr L]} by apply: seqInd_vcharW. by move=> Lpsi; rewrite sub_aut_zchar ?zchar_onG ?mem_zchar ?cfAut_seqInd. have mem_eta j: eta_ 0 j \in map sigma (irr W) by rewrite map_f ?mem_irr. have otau1eta: orthogonal (map tau1 calL) (map sigma (irr W)). apply/orthogonalP=> _ _ /mapP[psi Lpsi ->] /mapP[w irr_w ->]. have{w irr_w} [i [j ->]] := cycTIirrP defW irr_w; rewrite -/(w_ i j). pose Psi := tau1 (psi - psi^*%CF); pose NC := cyclicTI_NC ctiWG. have [[Itau1 Ztau1] Dtau1] := cohL. have Lpsis: psi^*%CF \in calL by rewrite cfAut_seqInd. have Z1dpsi := ZsubL _ Lpsi; have Zdpsi := zcharW Z1dpsi. have{Dtau1} PsiV0: {in V, Psi =1 \0}. move=> x /setDP[Wx _]; rewrite /Psi Dtau1 ?(cfun_on0 (Dade_cfunS _ _)) //. rewrite FT_DadeF_supportE -defA; apply: contra_eqN tiA_PWG => Ax. by apply/set0Pn; exists x; rewrite !inE Ax orbC mem_class_support. have opsi: '[psi, psi^*] = 0 by apply: seqInd_conjC_ortho (mFT_odd _) _ Lpsi. have n2Psi: '[Psi] = 2%:R. by rewrite Itau1 ?cfnormBd // cfnorm_conjC ?irrWnorm ?irrL. have NC_Psi: (NC Psi < minn q p)%N. by rewrite (@leq_ltn_trans 2) ?leq_min ?qgt2 // cycTI_NC_norm ?Ztau1 ?n2Psi. apply: contraTeq (NC_Psi) => t1psi_eta; rewrite -leqNgt cycTI_NC_minn //. rewrite mul2n -addnn (leq_trans NC_Psi) ?leq_addl // andbT card_gt0. suffices [b Deta]: exists b : bool, eta_ i j = (-1) ^+ b *: tau1 psi. apply/set0Pn; exists (i, j); rewrite !inE /= /Psi raddfB cfdotBl {2}Deta. by rewrite cfdotZr Itau1 ?mem_zchar // cfdot_conjCl opsi conjC0 mulr0 subr0. exists (tau1 psi == - eta_ i j); apply: (canRL (signrZK _)). move/eqP: t1psi_eta; rewrite cfdot_dirr ?cycTIiso_dirr //; last first. by rewrite dirrE Itau1 ?Ztau1 ?mem_zchar //= irrWnorm ?irrL. by rewrite scaler_sign; do 2!case: eqP => //. have [[A0beta PVbeta] n2beta [defGa Ga1 R_Ga] ubGa dvu] := FTtypeP_bridge_facts. have [_ _ _ _ [_ Dtau]] := Sfacts. have o_tauL_S zeta j: j != 0 -> '[tauL zeta, tau (beta_ j)] = 0. move=> nzj; pose ABS := class_support (P^# :|: class_support V S) G. have ABSbeta: tau (beta_ j) \in 'CF(G, ABS). by rewrite Dtau ?A0beta // cfInd_on ?subsetT ?PVbeta. have{ABSbeta} PWGbeta: tau (beta_ j) \in 'CF(G, PWG). apply: cfun_onS ABSbeta; apply/subsetP=> _ /imset2P[x t PVSx _ ->]. case/setUP: PVSx => [/setD1P[_ Px] | /imset2P[y z /setDP[Wy _] _ ->]]. by rewrite inE memJ_class_support ?inE. by rewrite -conjgM inE orbC memJ_class_support ?inE. rewrite (cfdotElr (Dade_cfunS _ _) PWGbeta) big_pred0 ?mulr0 // => x. by rewrite FT_DadeF_supportE -defA tiA_PWG inE. have betaLeta j: j != 0 -> '[tauL betaL, eta_ 0 j] = '[tauL betaL, eta01]. move=> nzj; apply/eqP; rewrite -subr_eq0 -cfdotBr. rewrite (canRL (addKr _) (defGa j nzj)) !addrA addrK -addrA addrCA. by rewrite opprD subrK cfdotBr !o_tauL_S ?subrr ?Iirr1_neq0. split=> //; have [[[Itau1 Ztau1] Dtau1] irr_phi] := (cohL, irrL Lphi). pose GammaL := tauL betaL - (1 - tau1 phi). have DbetaL: tauL betaL = 1 - tau1 phi + GammaL by rewrite addrC subrK. have RealGammaL: cfReal GammaL. rewrite /cfReal -subr_eq0 !rmorphB rmorph1 /= !opprB !addrA subrK addrC. rewrite -addrA addrCA addrA addr_eq0 opprB -Dade_aut -linearB /= -/tauL. rewrite rmorphB /= cfAutInd rmorph1 addrC opprB addrA subrK. by rewrite (cfConjC_Dade_coherent cohL) ?mFT_odd // -raddfB Dtau1 // ZsubL. have:= Dade_Ind1_sub_lin cohL _ irr_phi Lphi; rewrite -/betaL -/tauL -/calL. rewrite (seqInd_nontrivial _ _ _ Lphi) ?odd_Frobenius_index_ler ?mFT_odd //. case=> // -[o_tauL_1 o_betaL_1 ZbetaL] ub_betaL _. have{o_tauL_1 o_betaL_1} o_GaL_1: '[GammaL, 1] = 0. by rewrite !cfdotBl cfnorm1 o_betaL_1 (orthoPr o_tauL_1) ?map_f ?subr0 ?subrr. have Zt1phi: tau1 phi \in 'Z[irr G] by rewrite Ztau1 ?mem_zchar. have Zeta01: eta01 \in 'Z[irr G] by apply: cycTIiso_vchar. have ZbetaS: tau betaS \in 'Z[irr G]. rewrite Dade_vchar // zchar_split A0beta ?Iirr1_neq0 //. by rewrite rpredB ?irr_vchar ?cfInd_vchar ?rpred1. have Z_Ga: Gamma \in 'Z[irr G] by rewrite rpredD ?rpredB ?rpred1. have Z_GaL: GammaL \in 'Z[irr G] by rewrite !rpredB ?rpred1. have{RealGammaL} Gamma_even: (2 %| '[GammaL, Gamma])%C. by rewrite cfdot_real_vchar_even ?mFT_odd // o_GaL_1 (dvdC_nat 2 0). set bSphi := '[tau betaS, tau1 phi]; set bLeta := '[tauL betaL, eta01]. have [ZbSphi ZbLeta]: bSphi \in Cint /\ bLeta \in Cint. by rewrite !Cint_cfdot_vchar. have{Gamma_even} odd_bSphi_bLeta: (bSphi + bLeta == 1 %[mod 2])%C. rewrite -(conj_Cint ZbSphi) -cfdotC /bLeta DbetaL cfdotDl cfdotBl. have: '[tauL betaL, tau betaS] == 0 by rewrite o_tauL_S ?Iirr1_neq0. have ->: tau betaS = 1 - eta01 + Gamma by rewrite addrCA !addrA !subrK. rewrite !['[tau1 _, _]]cfdotDr 2!cfdotDr !cfdotNr DbetaL. rewrite 2!cfdotDl 2!['[_, eta01]]cfdotDl 2!['[_, Gamma]]cfdotDl !cfdotNl. rewrite cfnorm1 o_GaL_1 ['[1, Gamma]]cfdotC Ga1 conjC0 addr0 add0r. have ->: 1 = eta_ 0 0 by rewrite /w_ cycTIirr00 cycTIiso1. rewrite cfdot_cycTIiso mulrb ifN_eqC ?Iirr1_neq0 // add0r. rewrite 2?(orthogonalP otau1eta _ _ (map_f _ _) (mem_eta _)) // oppr0 !add0r. by rewrite addr0 addrA addrC addr_eq0 !opprB addrA /eqCmod => /eqP <-. have abs_mod2 a: a \in Cint -> {b : bool | a == b%:R %[mod 2%N]}%C. move=> Za; pose n := truncC `|a|; exists (odd n). apply: eqCmod_trans (eqCmod_addl_mul _ (rpred_nat _ n./2) _). rewrite addrC -natrM -natrD muln2 odd_double_half truncCK ?Cnat_norm_Cint //. rewrite -{1}[a]mul1r -(canLR (signrMK _) (CintEsign Za)) eqCmodMr // signrE. by rewrite /eqCmod opprB addrC subrK dvdC_nat dvdn2 odd_double. have [[bL DbL] [bS DbS]] := (abs_mod2 _ ZbLeta, abs_mod2 _ ZbSphi). have{odd_bSphi_bLeta} xor_bS_bL: bS (+) bL. rewrite eqCmod_sym in odd_bSphi_bLeta. have:= eqCmod_trans odd_bSphi_bLeta (eqCmodD DbS DbL). rewrite -natrD eqCmod_sym -(eqCmodDr _ 1) -mulrSr => xor_bS_bL. have:= eqCmod_trans xor_bS_bL (eqCmodm0 _); rewrite /eqCmod subr0. by rewrite (dvdC_nat 2 _.+1) dvdn2 /= negbK oddD !oddb; case: (_ (+) _). have ?: (0 != 1 %[mod 2])%C by rewrite eqCmod_sym /eqCmod subr0 (dvdC_nat 2 1). case is_c1: bS; [left | right]. rewrite is_c1 in DbS; split=> //. pose a_ (psi : 'CF(L)) := psi 1%g / e%:R. have Na_ psi: psi \in calL -> a_ psi \in Cnat by apply: dvd_index_seqInd1. have [X tau1X [D [dGa oXD oDtau1]]] := orthogonal_split (map tau1 calL) Gamma. have oo_L: orthonormal calL. by apply: sub_orthonormal (irr_orthonormal L); rewrite ?seqInd_uniq. have oo_tau1L: orthonormal (map tau1 calL) by apply: map_orthonormal. have defX: X = bSphi *: (\sum_(psi <- calL) a_ psi *: tau1 psi). have [_ -> defX] := orthonormal_span oo_tau1L tau1X. rewrite defX big_map scaler_sumr; apply: eq_big_seq => psi Lpsi. rewrite scalerA; congr (_ *: _); apply/eqP; rewrite -subr_eq0 mulrC. rewrite -[X](addrK D) -dGa cfdotBl (orthoPl oDtau1) ?map_f // subr0. rewrite cfdotC cfdotDr cfdotBr -/betaS -/eta01. have ->: 1 = eta_ 0 0 by rewrite /w_ cycTIirr00 cycTIiso1. rewrite 2?(orthogonalP otau1eta _ _ (map_f _ _) (mem_eta _)) // subrK. rewrite -cfdotC -(conj_Cnat (Na_ _ Lpsi)) -cfdotZr -cfdotBr. rewrite -raddfZ_Cnat ?Na_ // -raddfB cfdotC. rewrite Dtau1; last by rewrite zcharD1_seqInd ?seqInd_sub_lin_vchar. by rewrite o_tauL_S ?Iirr1_neq0 ?conjC0. have nz_bSphi: bSphi != 0 by apply: contraTneq DbS => ->. have ub_a: \sum_(psi <- calL) a_ psi ^+ 2 <= (u.-1 %/ q)%:R. apply: le_trans (ubGa D X _ _ _); first 1 last; first by rewrite addrC. - by rewrite cfdotC oXD conjC0. - apply/orthoPl=> eta Weta; rewrite (span_orthogonal otau1eta) //. exact: memv_span. rewrite defX cfnormZ cfnorm_sum_orthonormal // mulr_sumr !big_seq. apply: ler_sum => psi Lpsi; rewrite -{1}(norm_Cnat (Na_ _ _)) //. by rewrite ler_peMl ?exprn_ge0 ?normr_ge0 // Cint_normK // sqr_Cint_ge1. congr (_ <= _): ub_a; do 2!apply: (mulIf (neq0CiG L H)); rewrite -/e. rewrite divfK ?neq0CiG // -mulrA -expr2 mulr_suml. rewrite -subn1 natrB ?neq0CG // -indexg1 mulrC. rewrite -(sum_seqIndD_square nsHL) ?normal1 ?sub1G // -/calL. apply: eq_big_seq => psi Lpsi; rewrite irrWnorm ?irrL // divr1. by rewrite -exprMn divfK ?neq0CiG. rewrite is_c1 /= in xor_bS_bL; rewrite xor_bS_bL in DbL; split=> //. have nz_bL: bLeta != 0 by apply: contraTneq DbL => ->. have{ub_betaL} [X [otau1X oX1 [a Za defX]] [//|_ ubX]] := ub_betaL. rewrite -/e in defX; rewrite -leC_nat -(lerD2r (-1)); apply: le_trans ubX. pose calX0 := [seq w_ 0 j | j in predC1 0]. have ooX0: orthonormal calX0. apply: sub_orthonormal (irr_orthonormal W). by move=> _ /imageP[j _ ->]; apply: mem_irr. by apply/dinjectiveP=> j1 j2 _ _ /irr_inj/dprod_Iirr_inj[]. have Isigma: {in 'Z[calX0] &, isometry sigma}. by apply: in2W; apply: cycTIisometry. rewrite -[X](subrK (bLeta *: (\sum_(xi <- calX0) sigma xi))). rewrite cfnormDd ?ler_wpDl ?cfnorm_ge0 //; last first. rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 // => xi X0xi. apply/eqP; rewrite cfdotBl scaler_sumr cfproj_sum_orthonormal // subr_eq0. have {xi X0xi}[j nzj ->] := imageP X0xi; rewrite inE /= in nzj. rewrite -[bLeta](betaLeta j nzj) defX cfdotDl -addrA cfdotDl. have ->: 1 = eta_ 0 0 by rewrite /w_ cycTIirr00 cycTIiso1. rewrite cfdot_cycTIiso mulrb (ifN_eqC _ _ nzj) add0r eq_sym -subr_eq0 addrK. rewrite (span_orthogonal otau1eta) //; last by rewrite memv_span ?mem_eta. rewrite big_seq rpredD ?(rpredN, rpredZ, rpred_sum) ?memv_span ?map_f //. by move=> xi Lxi; rewrite rpredZ ?memv_span ?map_f. rewrite cfnormZ cfnorm_map_orthonormal // size_image cardC1 nirrW2. rewrite -(natrB _ (prime_gt0 pr_p)) Cint_normK // subn1. by rewrite ler_peMl ?ler0n ?sqr_Cint_ge1. 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) 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)