proposition: Lemma FTtypeP_bridge_facts (V_S := class_support (cyclicTIset defW) S) : [/\ [/\ forall j, j != 0 -> beta_ j \in 'CF(S, 'A0(S)) & forall j, j != 0 -> beta_ j \in 'CF(S, P^# :|: V_S)], forall j, j != 0 -> '[beta_ j] = (u.-1 %/ q + 2)%:R, [/\ forall j, j != 0 -> tau (beta_ j) - 1 + eta_ 0 j = Gamma, '[Gamma, 1] = 0 & cfReal Gamma], forall X Y : 'CF(G), Gamma = X + Y -> '[X, Y] = 0 -> orthogonal Y (map sigma (irr W)) -> '[Y] <= (u.-1 %/ q)%:R & q %| u.-1].
proof: Proof. have [_ sW1S _ nPUW1 tiPUW1] := sdprod_context defS. have /mulG_sub[sPPU sUPU] := sdprodW defPU. have sPW1S: P <*> W1 \subset S by rewrite join_subG gFsub. have /= defS_P := Ptype_Fcore_sdprod StypeP; have nsPS: P <| S := gFnormal _ _. have defPW1: P ><| W1 = P <*> W1 := sdprod_subr defS_P (joing_subr U W1). pose W1bar := (W1 / P)%g; pose Sbar := (S / P)%g; pose Ubar := (U / P)%g. pose gamma := 'Ind[Sbar, W1bar] 1. have Dgamma: 'Ind[S, P <*> W1] 1 = (gamma %% P)%CF. rewrite -(rmorph1 _ : 1 %% P = 1)%CF cfIndMod ?joing_subl //. by rewrite quotientYidl //; have [] := sdprodP defPW1. have gamma1: gamma 1%g = u%:R. rewrite -cfMod1 -Dgamma cfInd1 // cfun11 -divgS // -(sdprod_card defPW1). by rewrite mulr1 -(sdprod_card defS) -(sdprod_card defPU) divnMr // mulKn. have frobUW1: [Frobenius U <*> W1 = U ><| W1] by have [[]] := Sfacts. have q_dv_u1: q %| u.-1 := Frobenius_dvd_ker1 frobUW1. have [nP_UW1 /isomP[/=]] := sdprod_isom defS_P; set h := restrm _ _ => injh hS. have /joing_sub[sUUW1 sW1UW1] := erefl (U <*> W1). have [hU hW1]: h @* U = Ubar /\ h @* W1 = W1bar. by rewrite !morphim_restrm /= !(setIidPr _). have{hS} frobSbar: [Frobenius Sbar = Ubar ><| W1bar]. by rewrite -[Sbar]hS -hU -hW1 injm_Frobenius. have tiW1bar: normedTI W1bar^# Sbar W1bar by have /and3P[] := frobSbar. have gammaW1 xbar: xbar \in W1bar^# -> gamma xbar = 1. move=> W1xbar; have [ntxbar _] := setD1P W1xbar. rewrite cfIndE ?quotientS //; apply: canLR (mulKf (neq0CG _)) _. have ->: #|W1bar| = #|Sbar :&: W1bar| by rewrite (setIidPr _) ?quotientS. rewrite mulr1 cardsE -sumr_const big_mkcondr; apply: eq_bigr => zbar Szbar. have [_ _ W1bar_xJ] := normedTI_memJ_P tiW1bar. by rewrite -mulrb -(W1bar_xJ xbar) // !inE conjg_eq1 ntxbar cfun1E. have PVSbeta j: j != 0 -> beta_ j \in 'CF(S, P^# :|: V_S). move=> nzj; apply/cfun_onP=> z; rewrite !inE => /norP[P'z VS'z]. have [Sz | /cfun0->//] := boolP (z \in S); apply/eqP; rewrite !cfunE subr_eq0. have [[_ mulW12 _ tiW12] C1] := (dprodP defW, FTtypeP_reg_Fcore maxS StypeP). have [PUz {VS'z} | PU'z {P'z}] := boolP (z \in PU). rewrite eq_sym -(cfResE _ _ PUz) ?gFsub // -['Res _](scalerK (neq0CG W1)). rewrite cfRes_prTIirr -cfRes_prTIred -/q cfunE cfResE ?gFsub // mulrC. case/nandP: P'z => [/negbNE/eqP-> | P'z]. rewrite Dgamma cfModE // morph1 gamma1 FTprTIred1 // C1 indexg1. by rewrite natrM mulfK ?neq0CG. have:= seqInd_on (Fitting_normal S) (FTprTIred_Ind_Fitting maxS StypeP nzj). have [/= <- _ _ _] := typeP_context StypeP; rewrite C1 dprodg1 -/(mu_ j). move/cfun_on0->; rewrite // mul0r (cfun_on0 (cfInd_on _ (cfun_onG _))) //. rewrite -(sdprodW defPW1); apply: contra P'z => /imset2P[x t PW1x St Dz]. rewrite Dz !memJ_norm ?(subsetP (gFnorm _ _)) // in PUz *. by rewrite -(mulg1 P) -tiPUW1 setIC group_modl // inE PW1x. have /imset2P[x t /setD1P[ntx W1x] St ->]: z \in class_support W1^# S. have /bigcupP[_ /rcosetsP[x W1x ->]]: z \in cover (rcosets PU W1). by rewrite (cover_partition (rcosets_partition_mul _ _)) (sdprodW defS). have [-> | ntx] := eqVneq x 1%g; first by rewrite mulg1 => /idPn[]. have nPUx: x \in 'N(PU) by rewrite (subsetP nPUW1). have coPUx: coprime #|PU| #[x] by rewrite (coprime_dvdr (order_dvdG W1x)). have [/cover_partition <- _] := partition_cent_rcoset nPUx coPUx. have [_ _ _ [_ _ _ _ prPUW1] _] := StypeP; rewrite {}prPUW1 ?inE ?ntx //. rewrite cover_imset => /bigcupP[t PUt /imsetP[_ /rcosetP[y W2y ->] Dz]]. have{PUt} St: t \in S by rewrite (subsetP _ _ PUt) ?der_sub. have [y1 | nty] := eqVneq y 1%g. by rewrite Dz y1 mul1g memJ_class_support // !inE ntx. rewrite Dz memJ_class_support // !inE groupMr // groupMl // in VS'z. rewrite -(dprodWC defW) mem_mulg // andbT; apply/norP. by rewrite -!in_set1 -set1gE -tiW12 !inE W1x W2y andbT in ntx nty. rewrite !cfunJ // Dgamma cfModE ?(subsetP sW1S) // gammaW1; last first. by rewrite !inE (morph_injm_eq1 injh) ?(subsetP sW1UW1) ?ntx ?mem_quotient. rewrite prTIirr_id ?FTprTIsign // ?scale1r ?dprod_IirrEr; last first. rewrite -in_set1 -set1gE -tiW12 inE W1x /= in ntx. by rewrite inE ntx -mulW12 (subsetP (mulG_subl W2 W1)). by rewrite -[x]mulg1 cfDprodEr ?lin_char1 ?irr_prime_lin. have A0beta j: j != 0 -> beta_ j \in 'CF(S, 'A0(S)). move/PVSbeta; apply: cfun_onS; rewrite (FTtypeP_supp0_def _ StypeP) //. by rewrite setSU ?(subset_trans _ (FTsupp1_sub _)) ?setSD ?Fcore_sub_FTcore. have norm_beta j: j != 0 -> '[beta_ j] = (u.-1 %/ q + 2)%:R. move=> nzj; rewrite cfnormBd ?Dgamma; last first. apply: contraNeq (cfker_prTIres pddS nzj); rewrite -irr_consttE => S1_mu0j. rewrite -(cfRes_prTIirr _ 0) sub_cfker_Res //. rewrite (subset_trans _ (cfker_constt _ S1_mu0j)) ?cfker_mod //. by rewrite -Dgamma cfInd_char ?rpred1. have [[/eqP defUW1 _] [/eqP defSbar _]] := (andP frobUW1, andP frobSbar). rewrite cfnorm_irr cfMod_iso //. rewrite (cfnormE (cfInd_on _ (cfun_onG _))) ?quotientS // -/gamma. rewrite card_quotient ?gFnorm // -(index_sdprod defS_P) -(sdprod_card defUW1). rewrite -/u -/q (big_setD1 1%g) ?mem_class_support ?group1 //=. have{tiW1bar} [_ tiW1bar /eqP defNW1bar] := and3P tiW1bar. rewrite gamma1 normr_nat class_supportD1 big_trivIset //=. rewrite (eq_bigr (fun xbar => #|W1bar|.-1%:R)) ?sumr_const; last first. rewrite (cardsD1 1%g) group1 /= => _ /imsetP[tbar Stbar ->]. rewrite -sumr_const big_imset /=; last exact: in2W (conjg_inj tbar). by apply: eq_bigr => xbar W1xbar; rewrite cfunJ ?gammaW1 // normr1 expr1n. rewrite card_conjugates -divgS ?subsetIl //= -(sdprod_card defSbar) defNW1bar. rewrite mulnK ?cardG_gt0 // -hU -hW1 ?card_injm // -/q -/u natrM invfM mulrC. rewrite -[rhs in _ ^+ 2 + rhs]mulr_natr -mulrDl mulrA mulfK ?neq0CG //. rewrite -subn1 natrB ?cardG_gt0 // addrCA mulrDl divff ?neq0CG //. by rewrite -natrB ?cardG_gt0 // subn1 -natf_div // addrAC addrC natrD. have nzj1: #1 != 0 :> Iirr W2 by apply: Iirr1_neq0. have [_ _ _ _ [_ Dtau]] := Sfacts; pose eta01 := eta_ 0 #1. have oeta01_1: '[eta01, 1] = 0. by rewrite -(cycTIiso1 ctiWG) -(cycTIirr00 defW) cfdot_cycTIiso (negPf nzj1). have Deta01s: eta01^*%CF = eta_ 0 (conjC_Iirr #1). by rewrite cfAut_cycTIiso /w_ !dprod_IirrEr cfAutDprodr aut_IirrE. have oGamma1: '[Gamma, 1] = 0. rewrite cfdotDl cfdotBl cfnorm1 oeta01_1 addr0 Dtau ?A0beta //. rewrite -cfdot_Res_r rmorph1 cfdotBl -cfdot_Res_r rmorph1 cfnorm1. by rewrite -(prTIirr00 ptiWS) cfdot_prTIirr (negPf nzj1) subr0 subrr. have defGamma j: j != 0 -> tau (beta_ j) - 1 + eta_ 0 j = Gamma. move=> nzj; apply/eqP; rewrite -subr_eq0 opprD addrACA opprB !addrA subrK. rewrite -linearB opprD addrACA subrr add0r -opprD linearN /=. move/prDade_sub_TIirr: pddS => -> //; last first. by apply: (mulfI (neq0CG W1)); rewrite -!prTIred_1 !FTprTIred1. by rewrite -/sigma FTprTIsign // scale1r -addrA addNr. have GammaReal: cfReal Gamma. rewrite /cfReal rmorphD/= rmorphB rmorph1 /= Deta01s Dtau ?A0beta // cfAutInd. rewrite rmorphB /= cfAutInd rmorph1 -prTIirr_aut aut_Iirr0 -/(beta_ _). by rewrite -Dtau ?A0beta ?defGamma ?aut_Iirr_eq0. split=> // X Y defXY oXY oYeta; pose a := '[Gamma, eta01]. have Za: a \in Cint. rewrite Cint_cfdot_vchar 1?rpredD ?rpredB ?rpred1 ?cycTIiso_vchar //. by rewrite Dtau ?A0beta // !(cfInd_vchar, rpredB) ?rpred1 ?irr_vchar. have{} oYeta j: '[Y, eta_ 0 j] = 0. by rewrite (orthoPl oYeta) ?map_f ?mem_irr. have o_eta1s1: '[eta01^*, eta01] = 0. rewrite Deta01s cfdot_cycTIiso /= -(inj_eq irr_inj) aut_IirrE. by rewrite odd_eq_conj_irr1 ?mFT_odd // irr_eq1 (negPf nzj1). rewrite -(lerD2r 2%:R) -natrD -(norm_beta #1) //. have ->: '[beta_ #1] = '[Gamma - eta01 + 1]. by rewrite addrK subrK Dade_isometry ?A0beta. rewrite addrA cfnormDd ?cfnorm1 ?lerD2r; last first. by rewrite cfdotBl oeta01_1 oGamma1 subrr. rewrite defXY addrAC addrC cfnormDd ?lerD2r; last first. by rewrite cfdotBl oXY cfdotC oYeta conjC0 subrr. have oXeta j: '[X, eta_ 0 j] = '[Gamma, eta_ 0 j]. by rewrite defXY cfdotDl oYeta addr0. pose X1 := X - a *: eta01 - a *: eta01^*%CF. have ->: X - eta01 = X1 + a *: eta01^*%CF + (a - 1) *: eta01. by rewrite scalerBl scale1r addrA !subrK. rewrite cfnormDd; last first. rewrite cfdotZr subrK cfdotBl oXeta -/a cfdotZl cfnorm_cycTIiso mulr1. by rewrite subrr mulr0. rewrite cfnormDd; last first. rewrite cfdotZr !cfdotBl !cfdotZl Deta01s cfnorm_cycTIiso oXeta -Deta01s. rewrite !cfdot_conjCr o_eta1s1 conjC0 mulr0 ((_ =P Gamma) GammaReal) -/a. by rewrite conj_Cint // mulr1 subr0 subrr mulr0. rewrite -addrA ler_wpDl ?cfnorm_ge0 // !cfnormZ Deta01s !cfnorm_cycTIiso. rewrite !mulr1 !Cint_normK ?rpredB ?rpred1 // sqrrB1 !addrA -mulr2n. by rewrite -subr_ge0 addrK subr_ge0 ler_pMn2r ?Cint_ler_sqr. 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)