proposition: Lemma FTtype5_exclusion_main : FTtype M != 5%N.
proof: Proof. apply/negP=> Mtype5. suffices [tau1]: coherent calS M^# tau by case/FTtype345_noncoherence_main. have [[_ U_M_1] MtypeV] := compl_of_typeV maxM MtypeP Mtype5. have [_ [_ _ _ defH] _ [_ _ _ sW2H' _] _] := MtypeP. have{U_M_1 defH} defMF: M`_\F = H by rewrite /= -defH U_M_1 sdprodg1. have nilH := Fcore_nil M; rewrite defMF -/w1 in MtypeV nilH. without loss [p [pH not_cHH ubHbar not_w1_dv_p1]]: / exists p : nat, [/\ p.-group H, ~~ abelian H, #|H : H'| <= 4 * w1 ^ 2 + 1 & ~ w1 %| p.-1]%N. - have [isoH1 solH] := (quotient1_isog H, nilpotent_sol nilH). have /non_coherent_chief-IHcoh := subset_subcoherent scohS0 sSS0. apply: IHcoh (fun coh _ => coh) _ => // [|[[_ ubH] [p [pH ab'H] /negP-dv'p]]]. split; rewrite ?mFT_odd ?normal1 ?sub1G ?quotient_nil //. by rewrite joingG1 (FrobeniusWker frobMbar). apply; exists p; rewrite (isog_abelian isoH1) (isog_pgroup p isoH1) -subn1. by rewrite /= joingG1 -(index_sdprod defM) in ubH dv'p. have ntH: H :!=: 1%g by apply: contraNneq not_cHH => ->; apply: abelian1. have [sH'H nH'H] := andP nsM''M'; have sW2H := subset_trans sW2H' sH'H. have def_w2: w2 = p by apply/eqP; have:= pgroupS sW2H pH; rewrite pgroupE pnatE. have piHp q: q \in \pi(H) -> q = p. by rewrite /= -(part_pnat_id pH) pi_of_part // => /andP[_ /eqnP]. have [tiHG | [_ /piHp-> []//] | [_ /piHp-> [oH w1_dv_p1 _]]] := MtypeV. suffices [tau1 [Itau1 Dtau1]]: coherent (seqIndD H M H 1) M^# 'Ind[G]. exists tau1; split=> // phi Sphi; rewrite {}Dtau1 //. rewrite zcharD1_seqInd // -subG1 -setD_eq0 -defA in Sphi tiHG ntH. by have Aphi := zchar_on Sphi; rewrite -FT_DadeE // Dade_Ind. apply: (@Sibley_coherence _ [set:_] M H W1); first by rewrite mFT_odd. right; exists W2 => //; exists 'A0(M), W, defW. by rewrite -defA -{2}(group_inj defMs). have [p_pr _ _] := pgroup_pdiv pH ntH; rewrite (pcore_pgroup_id pH) in oH. have{not_cHH} esH: extraspecial H. by apply: (p3group_extraspecial pH); rewrite // oH pfactorK. have oH': #|H'| = p. by rewrite -(card_center_extraspecial pH esH); have [[_ <-]] := esH. have defW2: W2 :=: H' by apply/eqP; rewrite eqEcard sW2H' oH' -def_w2 /=. have iH'H: #|H : H'|%g = (p ^ 2)%N by rewrite -divgS // oH oH' mulKn ?prime_gt0. have w1_gt0: (0 < w1)%N by apply: cardG_gt0. have{ubHbar} [def_p_w1 w1_lt_w2]: (p = 2 * w1 - 1 /\ w1 < w2)%N. have /dvdnP[k def_p]: 2 * w1 %| p.+1. by rewrite Gauss_dvd ?coprime2n ?mFT_odd ?dvdn2 //= -{1}def_w2 mFT_odd. suffices k1: k = 1%N. rewrite k1 mul1n in def_p; rewrite -ltn_double -mul2n -def_p -addn1 addnK. by rewrite -addnS -addnn def_w2 leq_add2l prime_gt1. have [k0 | k_gt0] := posnP k; first by rewrite k0 in def_p. apply/eqP; rewrite eqn_leq k_gt0 andbT -ltnS -ltn_double -mul2n. rewrite -[(2 * k)%N]prednK ?muln_gt0 // ltnS -ltn_sqr 3?leqW //=. rewrite -subn1 sqrnB ?muln_gt0 // expnMn muln1 mulnA ltnS leq_subLR. rewrite addn1 addnS ltnS -mulnSr leq_pmul2l // -(leq_subLR _ 1). rewrite (leq_trans (leq_pmulr _ w1_gt0)) // -(leq_pmul2r w1_gt0). rewrite -mulnA mulnBl mul1n -2!leq_double -!mul2n mulnA mulnBr -!expnMn. rewrite -(expnMn 2 _ 2) mulnCA -def_p -addn1 leq_subLR sqrnD muln1. by rewrite (addnC p) mulnDr addnA leq_add2r addn1 addnS -iH'H. pose S1 := seqIndD H M H H'. have sS1S: {subset S1 <= calS} by apply: seqIndS; rewrite Iirr_kerDS ?sub1G. have irrS1: {subset S1 <= irr M}. move=> _ /seqIndP[s /setDP[kerH' ker'H] ->]; rewrite !inE in kerH' ker'H. rewrite -(quo_IirrK _ kerH') // mod_IirrE // cfIndMod // cfMod_irr //. rewrite (irr_induced_Frobenius_ker (FrobeniusWker frobMbar)) //. by rewrite quo_Iirr_eq0 // -subGcfker. have S1w1: {in S1, forall xi : 'CF(M), xi 1%g = w1%:R}. move=> _ /seqIndP[s /setDP[kerH' _] ->]; rewrite !inE in kerH'. by rewrite cfInd1 // -(index_sdprod defM) lin_char1 ?mulr1 // lin_irr_der1. have sS10: cfConjC_subset S1 calS0. by apply: seqInd_conjC_subset1; rewrite /= defMs. pose S2 := [seq mu_ j | j in predC1 0]. have szS2: size S2 = p.-1. by rewrite -def_w2 size_map -cardE cardC1 card_Iirr_abelian ?cyclic_abelian. have uS2: uniq S2 by apply/dinjectiveP; apply: in2W (prTIred_inj pddM). have redS2: {subset S2 <= [predC irr M]}. by move=> _ /imageP[j _ ->]; apply: (prTIred_not_irr pddM). have sS2S: {subset S2 <= calS} by move=> _ /imageP[j /calSmu Smu_j ->]. have S1'2: {subset S2 <= [predC S1]}. by move=> xi /redS2; apply: contra (irrS1 _). have w1_dv_p21: w1 %| p ^ 2 - 1 by rewrite (subn_sqr p 1) addn1 dvdn_mull. have [j nz_j] := has_nonprincipal_irr ntW2. have [Dmu2_1 Ddelta_ lt1d Nn] := FTtype345_constants. have{lt1d} [defS szS1 Dd Ddel Dn]: [/\ perm_eq calS (S1 ++ S2), size S1 = (p ^ 2 - 1) %/ w1, d = p, delta = -1 & n = 2%:R]. - pose X_ (S0 : seq 'CF(M)) := [set s | 'Ind[M, H] 'chi_s \in S0]. pose sumX_ cS0 := \sum_(s in X_ cS0) 'chi_s 1%g ^+ 2. have defX1: X_ S1 = Iirr_kerD H H H'. by apply/setP=> s; rewrite !inE mem_seqInd // !inE. have defX: X_ calS = Iirr_kerD H H 1%g. by apply/setP=> s; rewrite !inE mem_seqInd ?normal1 //= !inE. have sumX1: sumX_ S1 = (p ^ 2)%:R - 1. by rewrite /sumX_ defX1 sum_Iirr_kerD_square // iH'H indexgg mul1r. have ->: size S1 = (p ^ 2 - 1) %/ w1. apply/eqP; rewrite eqn_div // -eqC_nat mulnC [w1](index_sdprod defM). rewrite (size_irr_subseq_seqInd _ (subseq_refl S1)) //. rewrite natrB ?expn_gt0 ?prime_gt0 // -sumr_const -sumX1. apply/eqP/esym/eq_bigr => s. by rewrite defX1 !inE -lin_irr_der1 => /and3P[_ _ /eqP->]; rewrite expr1n. have oX2: #|X_ S2| = p.-1. by rewrite -(size_red_subseq_seqInd_typeP MtypeP uS2 sS2S). have sumX2: (p ^ 2 * p.-1)%:R <= sumX_ S2 ?= iff (d == p). rewrite /sumX_ (eq_bigr (fun _ => d%:R ^+ 2)) => [|s]; last first. rewrite inE => /imageP[j1 nz_j1 Dj1]; congr (_ ^+ 2). apply: (mulfI (neq0CiG M H)); rewrite -cfInd1 // -(index_sdprod defM). by rewrite Dj1 (prTIred_1 pddM) Dmu2_1. rewrite sumr_const oX2 mulrnA (mono_leif (ler_pMn2r _)); last first. by rewrite -def_w2 -(subnKC w2gt2). rewrite natrX (mono_in_leif ler_sqr) ?rpred_nat // eq_sym leif_nat_r. apply/leqif_eq; rewrite dvdn_leq 1?ltnW //. have: (mu2_ 0 j 1%g %| (p ^ 3)%N)%C. by rewrite -(cfRes1 H) cfRes_prTIirr -oH dvd_irr1_cardG. rewrite Dmu2_1 // dvdC_nat => /dvdn_pfactor[//|[_ d1|e _ ->]]. by rewrite d1 in lt1d. by rewrite expnS dvdn_mulr. pose S3 := filter [predC S1 ++ S2] calS. have sumX3: 0 <= sumX_ S3 ?= iff nilp S3. rewrite /sumX_; apply/leifP. have [-> | ] := altP nilP; first by rewrite big_pred0 // => s; rewrite !inE. rewrite -lt0n -has_predT => /hasP[xi S3xi _]. have /seqIndP[s _ Dxi] := mem_subseq (filter_subseq _ _) S3xi. rewrite (bigD1 s) ?inE -?Dxi //= ltr_pwDl ?sumr_ge0 // => [|s1 _]. by rewrite exprn_gt0 ?irr1_gt0. by rewrite ltW ?exprn_gt0 ?irr1_gt0. have [_ /esym] := leifD sumX2 sumX3. have /(canLR (addKr _)) <-: sumX_ calS = sumX_ S1 + (sumX_ S2 + sumX_ S3). rewrite [sumX_ _](big_setID (X_ S1)); congr (_ + _). by apply: eq_bigl => s; rewrite !inE andb_idl // => /sS1S. rewrite (big_setID (X_ S2)); congr (_ + _); apply: eq_bigl => s. by rewrite !inE andb_idl // => S2s; rewrite [~~ _]S1'2 ?sS2S. by rewrite !inE !mem_filter /= mem_cat orbC negb_or andbA. rewrite sumX1 /sumX_ defX sum_Iirr_kerD_square ?sub1G ?normal1 // indexgg. rewrite addr0 mul1r indexg1 oH opprD addrACA addNr addr0 addrC. rewrite (expnSr p 2) -[p in (_ ^ 2 * p)%:R - _]prednK ?prime_gt0 // mulnSr. rewrite natrD addrK eqxx => /andP[/eqP Dd /nilP S3nil]. have uS12: uniq (S1 ++ S2). by rewrite cat_uniq seqInd_uniq uS2 andbT; apply/hasPn. rewrite uniq_perm ?seqInd_uniq {uS12}// => [|xi]; last first. apply/idP/idP; apply: allP xi; last by rewrite all_cat !(introT allP _). by rewrite -(canLR negbK (has_predC _ _)) has_filter -/S3 S3nil. have: (w1 %| d%:R - delta)%C. by rewrite unfold_in pnatr_eq0 eqn0Ngt w1_gt0 rpred_Cnat. rewrite /n Dd def_p_w1 /delta; case: (Idelta _) => [_|/idPn[] /=]. by rewrite opprK -(natrD _ _ 1) subnK ?muln_gt0 // natrM mulfK ?neq0CG. rewrite mul2n -addnn -{1}(subnKC (ltnW w1gt2)) !addSn mulrSr addrK dvdC_nat. by rewrite add0n dvdn_addl // -(subnKC w1gt2) gtnNdvd // leqW. have scohS1 := subset_subcoherent scohS0 sS10. have o1S1: orthonormal S1. rewrite orthonormalE andbC; have [_ _ -> _ _] := scohS1. by apply/allP=> xi /irrS1/irrP[t ->]; rewrite /= cfnorm_irr. have [tau1 cohS1]: coherent S1 M^# tau. apply: uniform_degree_coherence scohS1 _; apply: all_pred1_constant w1%:R _ _. by rewrite all_map; apply/allP=> xi /S1w1/= ->. have [[Itau1 Ztau1] Dtau1] := cohS1. have o1S1tau: orthonormal (map tau1 S1) by apply: map_orthonormal. have S1zeta: zeta \in S1. by have:= Szeta; rewrite (perm_mem defS) mem_cat => /orP[//|/redS2/negP]. have Dalpha i (al_ij := alpha_ i j) : al_ij^\tau = delta *: (eta_ i j - eta_ i 0) - n *: tau1 zeta. - have [Y S1_Y [X [Dal_ij _ oXY]]] := orthogonal_split (map tau1 S1) al_ij^\tau. have [a_ Da_ defY] := orthonormal_span o1S1tau S1_Y. have oXS1 lam : lam \in S1 -> '[X, tau1 lam] = 0. by move=> S1lam; rewrite (orthoPl oXY) ?map_f. have{} Da_ lam : lam \in S1 -> a_ (tau1 lam) = '[al_ij^\tau, tau1 lam]. by move=> S1lam; rewrite Dal_ij cfdotDl oXS1 // addr0 Da_. pose a := n + a_ (tau1 zeta); have [_ oS1S1] := orthonormalP o1S1. have Da_z: a_ (tau1 zeta) = - n + a by rewrite addKr. have Za: a \in Cint. rewrite rpredD ?Dn ?rpred_nat // Da_ // Cint_cfdot_vchar ?Zalpha_tau //=. by rewrite Ztau1 ?mem_zchar. have Da_z' lam: lam \in S1 -> lam != zeta -> a_ (tau1 lam) = a. move=> S1lam zeta'lam; apply: canRL (subrK _) _. rewrite !Da_ // -cfdotBr -raddfB. have S1dlam: lam - zeta \in 'Z[S1, M^#]. by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE !S1w1 ?subrr. rewrite Dtau1 // Dade_isometry ?alpha_on ?tauM' //; last first. by rewrite -zcharD1_seqInd ?(zchar_subset sS1S). have o_mu2_lam k: '[mu2_ i k, lam] = 0 by rewrite o_mu2_irr ?sS1S ?irrS1. rewrite !cfdotBl !cfdotZl !cfdotBr !o_mu2_lam !o_mu2_zeta !(subr0, mulr0). by rewrite irrWnorm ?oS1S1 // eq_sym (negPf zeta'lam) !add0r mulrN1 opprK. have lb_n2alij: (a - n) ^+ 2 + (size S1 - 1)%:R * a ^+ 2 <= '[al_ij^\tau]. rewrite Dal_ij cfnormDd; last first. by rewrite cfdotC (span_orthogonal oXY) ?rmorph0 // memv_span1. rewrite ler_wpDr ?cfnorm_ge0 // defY cfnorm_sum_orthonormal //. rewrite (big_rem (tau1 zeta)) ?map_f //= le_eqVlt; apply/predU1P; left. congr (_ + _). by rewrite Da_z addrC Cint_normK 1?rpredD // rpredN Dn rpred_nat. rewrite (eq_big_seq (fun _ => a ^+ 2)) => [|tau1lam]; last first. rewrite rem_filter ?free_uniq ?orthonormal_free // filter_map. case/mapP=> lam; rewrite mem_filter /= andbC => /andP[S1lam]. rewrite (inj_in_eq (Zisometry_inj Itau1)) ?mem_zchar // => zeta'lam ->. by rewrite Da_z' // Cint_normK. rewrite big_tnth sumr_const card_ord size_rem ?map_f // size_map. by rewrite mulr_natl subn1. have{lb_n2alij} ub_a2: (size S1)%:R * a ^+ 2 <= 2%:R * a * n + 2%:R. rewrite norm_alpha // addrC sqrrB !addrA lerD2r in lb_n2alij. rewrite mulr_natl -mulrSr lerBlDl subn1 in lb_n2alij. by rewrite -mulrA !mulr_natl; case: (S1) => // in S1zeta lb_n2alij *. have{ub_a2} ub_8a2: 8%:R * a ^+ 2 <= 4%:R * a + 2%:R. rewrite mulrAC Dn -natrM in ub_a2; apply: le_trans ub_a2. rewrite -Cint_normK // ler_wpM2r ?exprn_ge0 ?normr_ge0 // leC_nat szS1. rewrite (subn_sqr p 1) def_p_w1 subnK ?muln_gt0 // mulnA mulnK // mulnC. by rewrite -subnDA -(mulnBr 2%N _ 1%N) mulnA (@leq_pmul2l 4 2) ?ltn_subRL. have Z_4a1: 4%:R * a - 1%:R \in Cint by rewrite rpredB ?rpredM ?rpred_nat. have{ub_8a2} ub_4a1: `|4%:R * a - 1| < 3%:R. rewrite -ltr_sqr ?rpred_nat ?qualifE/= ?normr_ge0 // -natrX Cint_normK //. rewrite sqrrB1 exprMn -natrX -mulrnAl -mulrnA (natrD _ 8 1) ltrD2r. rewrite (natrM _ 2 4) (natrM _ 2 8) -!mulrA -mulrBr ltr_pM2l ?ltr0n //. by rewrite ltrBlDl (le_lt_trans ub_8a2) // ltrD2l ltr_nat. have{ub_4a1} a0: a = 0. apply: contraTeq ub_4a1 => a_nz; have:= norm_Cint_ge1 Za a_nz. rewrite real_ltr_norml ?real_ler_normr ?Creal_Cint //; apply: contraL. case/andP; rewrite ltrBlDr -(natrD _ 3 1) gtr_pMr ?ltr0n //. rewrite ltrNl opprB -mulrN => /lt_le_trans/=/(_ _ (leC_nat 3 5)). by rewrite (natrD _ 1 4) ltrD2l gtr_pMr ?ltr0n //; do 2!move/lt_geF->. apply: (def_tau_alpha cohS1 sS10 nz_j S1zeta). by rewrite -Da_ // Da_z a0 addr0. have o_eta__zeta i j1: '[tau1 zeta, eta_ i j1] = 0. by rewrite (coherent_ortho_cycTIiso _ sS10 cohS1) ?mem_irr. have Dmu0zeta: (mu_ 0 - zeta)^\tau = \sum_i eta_ i 0 - tau1 zeta. have A0mu0tau: mu_ 0 - zeta \in 'CF(M, 'A0(M)). rewrite /'A0(M) defA; apply: (cfun_onS (subsetUl _ _)). rewrite cfun_onD1 [mu_ 0](prTIred0 pddM) !cfunE zeta1w1 cfuniE // group1. by rewrite mulr1 subrr rpredB ?rpredZnat ?cfuni_on ?(seqInd_on _ Szeta) /=. have [chi [Dmu0 Zchi n1chi o_chi_w]] := FTtype345_Dade_bridge0 w1_lt_w2. have dirr_chi: chi \in dirr G by rewrite dirrE Zchi n1chi /=. have dirr_zeta: tau1 zeta \in dirr G. by rewrite dirrE Ztau1 ?Itau1 ?mem_zchar //= irrWnorm. have: '[(alpha_ 0 j)^\tau, (mu_ 0 - zeta)^\tau] == - delta + n. rewrite Dade_isometry ?alpha_on // !cfdotBl !cfdotZl !cfdotBr. rewrite !o_mu2_zeta 2!cfdot_prTIirr_red (negPf nz_j) cfdotC o_mu_zeta. by rewrite eqxx irrWnorm // conjC0 !(subr0, add0r) mulr1 mulrN1 opprK. rewrite Dalpha // Dmu0 !{1}(cfdotBl, cfdotZl) !cfdotBr 2!{1}(cfdotC _ chi). rewrite !o_chi_w conjC0 !cfdot_sumr big1 => [|i]; first last. by rewrite (cfdot_cycTIiso pddM) (negPf nz_j) andbF. rewrite (bigD1 0) //= cfdot_cycTIiso big1 => [|i nz_i]; first last. by rewrite cfdot_cycTIiso eq_sym (negPf nz_i). rewrite big1 // !subr0 !add0r addr0 mulrN1 mulrN opprK (can_eq (addKr _)). rewrite {2}Dn -mulr_natl Dn (inj_eq (mulfI _)) ?pnatr_eq0 //. by rewrite cfdot_dirr_eq1 // => /eqP->. have [] := uniform_prTIred_coherent pddM nz_j; rewrite -/sigma. have ->: uniform_prTIred_seq pddM j = S2. congr (map _ _); apply: eq_enum => k; rewrite !inE -!/(mu_ _). by rewrite andb_idr // => nz_k; rewrite 2!{1}prTIred_1 2?Dmu2_1. case=> _ _ ccS2 _ _ [tau2 Dtau2 cohS2]. have{} cohS2: coherent_with S2 M^# tau tau2 by apply: cohS2. have sS20: cfConjC_subset S2 calS0. by split=> // xi /sS2S Sxi; have [_ ->] := sSS0. rewrite perm_sym perm_catC in defS; apply: perm_coherent defS _. suffices: (mu_ j - d%:R *: zeta)^\tau = tau2 (mu_ j) - tau1 (d%:R *: zeta). apply: (bridge_coherent scohS0 sS20 cohS2 sS10 cohS1) => [phi|]. by apply: contraL => /S1'2. rewrite cfunD1E !cfunE zeta1w1 prTIred_1 mulrC Dmu2_1 // subrr. by rewrite image_f // rpredZnat ?mem_zchar. have sumA: \sum_i alpha_ i j = mu_ j - delta *: mu_ 0 - (d%:R - delta) *: zeta. rewrite !sumrB sumr_const /= -scaler_sumr; congr (_ - _ - _). rewrite card_Iirr_abelian ?cyclic_abelian // -/w1 -scaler_nat. by rewrite scalerA mulrC divfK ?neq0CG. rewrite scalerBl opprD opprK addrACA in sumA. rewrite -{sumA}(canLR (addrK _) sumA) opprD opprK -scalerBr. rewrite linearD linearZ linear_sum /= Dmu0zeta scalerBr. rewrite (eq_bigr _ (fun i _ => Dalpha i)) sumrB sumr_const nirrW1. rewrite -!scaler_sumr sumrB addrAC !addrA scalerBr subrK -addrA -opprD. rewrite raddfZnat Dtau2 Ddelta_ //; congr (_ - _). by rewrite addrC -scaler_nat scalerA mulrC divfK ?neq0CG // -scalerDl subrK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly 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 mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum algC classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9)