proposition: Lemma FTtypeP_min_typeII : FTtype T == 2%N.
proof: Proof. apply: contraLR v1p_gt_u1q => notTtype2; rewrite -leqNgt -leC_nat. have [o_betaT0_eta _ [Ttype3 _]] := FTtype34_structure maxT TtypeP notTtype2. have Ttype_gt2: (2 < FTtype T)%N by rewrite (eqP Ttype3). have [[_ _ frobVW2 cVV] _ _ _ _] := FTtypeP_facts _ TtypeP. pose calT1 := seqIndD QV T QV Q; have sT10: cfConjC_subset calT1 calT0. by apply/seqInd_conjC_subset1; rewrite /= FTcore_eq_der1. rewrite (FTtypeP_reg_Fcore maxT TtypeP) (group_inj (joingG1 _)) in o_betaT0_eta. do [rewrite -/calT1; set eta_0 := \sum_j _] in o_betaT0_eta. have scohT1: subcoherent calT1 tauT rmR_T := subset_subcoherent scohT0 sT10. have [nsQQV sVQV _ _ _] := sdprod_context defQV. have nsQVT: QV <| T := der_normal 1 T. have calT1_1p zeta: zeta \in calT1 -> zeta 1%g = p%:R. case/seqIndP=> s /setDP[kerQs _] -> /=; rewrite inE in kerQs. rewrite cfInd1 ?gFsub // -(index_sdprod defT) lin_char1 ?mulr1 //. rewrite lin_irr_der1 (subset_trans _ kerQs) // der1_min ?normal_norm //. by rewrite -(isog_abelian (sdprod_isog defQV)). have [tau1T cohT1]: coherent calT1 T^# tauT. apply/(uniform_degree_coherence scohT1)/(@all_pred1_constant _ p%:R). by apply/allP=> _ /mapP[zeta T1zeta ->]; rewrite /= calT1_1p. have irrT1: {subset calT1 <= irr T}. move=> _ /seqIndP[s /setDP[kerQs nz_s] ->]; rewrite inE in kerQs. rewrite inE subGcfker in nz_s; rewrite -(quo_IirrK nsQQV kerQs) mod_IirrE //. rewrite cfIndMod ?normal_sub ?cfMod_irr ?gFnormal //. rewrite irr_induced_Frobenius_ker ?quo_Iirr_eq0 //=. have /sdprod_isom[nQ_VW1 /isomP[injQ <-]] := Ptype_Fcore_sdprod TtypeP. have ->: (QV / Q)%g = (V / Q)%g by rewrite -(sdprodW defQV) quotientMidl. have ->: (V / Q)%g = restrm nQ_VW1 (coset Q) @* V. by rewrite morphim_restrm (setIidPr _) // joing_subl. by rewrite injm_Frobenius_ker // (FrobeniusWker frobVW2). have [[A0betaS PVbetaS] _ [_]] := FTtypeP_bridge_facts maxS StypeP. rewrite -/q -/u; set Gamma := FTtypeP_bridge_gap _ _ => oGa1 R_Ga lb_Ga _. have oT1eta: orthogonal (map tau1T calT1) (map sigma (irr W)). apply/orthogonalP=> _ _ /mapP[zeta T1zeta ->] /mapP[omega Womega ->]. have{omega Womega} [i [j ->]] := cycTIirrP defW Womega. by rewrite (cycTIisoC _ pddT) (coherent_ortho_cycTIiso _ sT10 cohT1) ?irrT1. have [[Itau1T Ztau1T] Dtau1T] := cohT1. have nzT1_Ga zeta: zeta \in calT1 -> `|'[Gamma, tau1T zeta]| ^+ 2 >= 1. have Z_Ga: Gamma \in 'Z[irr G]. rewrite rpredD ?cycTIiso_vchar // rpredB ?rpred1 ?Dade_vchar // zchar_split. by rewrite A0betaS ?Iirr1_neq0 // rpredB ?cfInd_vchar ?rpred1 ?irr_vchar. move=> T1zeta; rewrite expr_ge1 ?normr_ge0 // norm_Cint_ge1 //. by rewrite Cint_cfdot_vchar ?Ztau1T ?(mem_zchar T1zeta). suffices: ('[Gamma, tau1T zeta] == 1 %[mod 2])%C. by apply: contraTneq => ->; rewrite (eqCmod_nat 2 0 1). pose betaT0 := nu_ 0 - zeta. have{o_betaT0_eta} o_eta0_betaT0 j: '[eta_ 0 j, tauT betaT0] = (j == 0)%:R. transitivity '[eta_ 0 j, eta_0]; rewrite (cycTIisoC _ pddT). apply/eqP; rewrite -subr_eq0 -cfdotBr cfdotC. by rewrite (orthoPl (o_betaT0_eta _ _)) ?conjC0 // map_f ?mem_irr. rewrite cfdot_sumr (bigD1 0) //= cfdot_cycTIiso andbT big1 ?addr0 //. by move=> i /negPf nz_i; rewrite cfdot_cycTIiso andbC eq_sym nz_i. have QVbetaT0: betaT0 \in 'CF(T, QV^#). rewrite cfun_onD1 rpredB ?(seqInd_on _ T1zeta) //=; last first. by rewrite /nu_ -cfInd_prTIres cfInd_normal. by rewrite !cfunE prTIred_1 prTIirr0_1 mulr1 calT1_1p ?subrr. have A0betaT0: betaT0 \in 'CF(T, 'A0(T)). by rewrite (cfun_onS (FTsupp1_sub0 _)) // /'A1(T) ?FTcore_eq_der1. have ZbetaT0: betaT0 \in 'Z[irr T]. by rewrite rpredB ?char_vchar ?(seqInd_char T1zeta) ?prTIred_char. pose Delta := tauT betaT0 - 1 + tau1T zeta. have nz_i1: #1 != 0 := Iirr1_neq0 ntW2. rewrite -(canLR (addKr _) (erefl Delta)) opprB cfdotDr cfdotBr oGa1 add0r. rewrite cfdotDl cfdotBl -/betaS o_eta0_betaT0 (negPf nz_i1) // addr0 opprB. rewrite -(cycTIiso1 pddS) -(cycTIirr00 defW) {}o_eta0_betaT0 mulr1n. have QV'betaS: tauS betaS \in 'CF(G, ~: class_support QV^# G). have [_ [pP _] _ _ [_ ->]] := FTtypeP_facts _ StypeP; rewrite ?A0betaS //. apply: cfun_onS (cfInd_on (subsetT S) (PVbetaS _ nz_i1)). apply/subsetP=> x PWx; rewrite inE. have{PWx}: p \in \pi(#[x]). case/imset2P: PWx => {}x y PWx _ ->; rewrite {y}orderJ. case/setUP: PWx => [/setD1P[ntx Px] | /imset2P[{}x y Wx _ ->]]. rewrite -p_rank_gt0 -rank_pgroup ?rank_gt0 ?cycle_eq1 //. exact: mem_p_elt (abelem_pgroup pP) Px. case/setDP: Wx; rewrite {y}orderJ; have [_ <- cW12 _] := dprodP defW. case/mulsgP=> {}x y W1x W2y ->; have cyx := centsP cW12 _ W2y _ W1x. have [-> | nty _] := eqVneq y 1%g; first by rewrite inE mulg1 W1x. have p'x: p^'.-elt x. by rewrite (mem_p_elt _ W1x) /pgroup ?pnatE ?inE ?ltn_eqF. have p_y: p.-elt y by rewrite (mem_p_elt (pnat_id _)). rewrite -cyx orderM ?(pnat_coprime p_y) // pi_ofM // inE /=. by rewrite -p_rank_gt0 -rank_pgroup // rank_gt0 cycle_eq1 nty. apply: contraL => /imset2P[z y /setD1P[_ QVz] _ ->]; rewrite {x y}orderJ. rewrite -p'natEpi // [_.-nat _](mem_p_elt _ QVz) // /pgroup ?p'natE //. rewrite -prime_coprime // coprime_sym (coprime_sdprod_Hall_r defT). by have [[]] := TtypeP. have [_ _ _ _ [_ -> //]] := FTtypeP_facts _ TtypeP. rewrite (cfdotElr QV'betaS (cfInd_on _ QVbetaT0)) ?subsetT //=. rewrite setIC setICr big_set0 mulr0 subr0 addrC /eqCmod addrK. rewrite cfdot_real_vchar_even ?mFT_odd ?oGa1 ?rpred0 //; split. rewrite rpredD ?Ztau1T ?(mem_zchar T1zeta) // rpredB ?rpred1 //. by rewrite Dade_vchar // zchar_split ZbetaT0. rewrite /cfReal -subr_eq0 opprD opprB rmorphD /= rmorphB rmorph1 /= addrACA. rewrite !addrA subrK -Dade_aut -linearB /= -/tauT rmorphB opprB /=. rewrite -prTIred_aut aut_Iirr0 -/nu_ [sum in tauT sum]addrC addrA subrK. rewrite -Dtau1T; last first. by rewrite (zchar_onS _ (seqInd_sub_aut_zchar _ _ _)) // setSD ?der_sub. rewrite raddfB -addrA addrC addrA subrK subr_eq0. by rewrite (cfConjC_Dade_coherent cohT1) ?mFT_odd ?irrT1. have [Y T1_Y [X [defGa oYX oXT1]]] := orthogonal_split (map tau1T calT1) Gamma. apply: le_trans (lb_Ga X Y _ _ _); first 1 last; rewrite 1?addrC //. - by rewrite cfdotC oYX conjC0. - by apply/orthoPl=> eta Weta; rewrite (span_orthogonal oT1eta) // memv_span. have ->: v.-1 = (p * size calT1)%N; last rewrite mulKn ?prime_gt0 //. rewrite [p](index_sdprod defT); have isoV := sdprod_isog defQV. rewrite [v](card_isog isoV) -card_Iirr_abelian -?(isog_abelian isoV) //. rewrite -(card_imset _ (can_inj (mod_IirrK nsQQV))) (cardD1 0) /=. rewrite -{1}(mod_Iirr0 QV Q) imset_f //=. rewrite (size_irr_subseq_seqInd _ (subseq_refl _)) //=. apply: eq_card => s; rewrite !inE mem_seqInd ?gFnormal // !inE subGcfker. congr (_ && _); apply/idP/idP=> [/imsetP[r _ ->] | kerQs]. by rewrite mod_IirrE ?cfker_mod. by rewrite -(quo_IirrK nsQQV kerQs) imset_f. have o1T1: orthonormal (map tau1T calT1). rewrite map_orthonormal ?(sub_orthonormal irrT1) ?seqInd_uniq //. exact: irr_orthonormal. have [_ -> ->] := orthonormal_span o1T1 T1_Y. rewrite cfnorm_sum_orthonormal // big_map -sum1_size natr_sum !big_seq. apply: ler_sum => // zeta T1zeta; rewrite -(canLR (addrK X) defGa). by rewrite cfdotBl (orthoPl oXT1) ?subr0 ?nzT1_Ga ?map_f. 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)