proposition: Lemma FTtype34_structure (eta0row := \sum_j eta_ 0 j) : [/\ {in S1, forall zeta, eq_proj_eta (tau (bridge0 zeta)) eta0row}, (p < q)%N & FTtype M == 3%N /\ typeP_Galois MtypeP].
proof: Proof. have sum_etaW F: \sum_(eta <- etaW) F eta = \sum_i \sum_j F (eta_ i j). rewrite big_map big_tuple (reindex (dprod_Iirr defW)) /=. by rewrite pair_bigA; apply: eq_bigr => -[i j]. by exists (inv_dprod_Iirr defW) => ij; rewrite ?dprod_IirrK ?inv_dprod_IirrK. have bridgeS1: {in S1, forall zeta, eq_proj_eta (tau (bridge0 zeta)) eta0row}. move=> zeta S1zeta; set phi := bridge0 zeta; have irr_zeta := irrS1 S1zeta. have [X etaX [chi [Dchi oXchi o_chi_eta]]] := orthogonal_split etaW (tau phi). have [Isigma Zsigma] := cycTI_Zisometry ctiWG. have{} o_chi_eta i j: '[chi, eta_ i j] = 0. by rewrite (orthoPl o_chi_eta) ?map_f ?mem_irr. have o1etaW: orthonormal etaW by rewrite map_orthonormal ?irr_orthonormal. have [a Da defX] := orthonormal_span o1etaW etaX; pose a_ := a (eta_ _ _). have{} Da i j: a_ i j = '[tau phi, eta_ i j]. by rewrite Dchi cfdotDl o_chi_eta addr0 /a_ Da. have Zphi: phi \in 'Z[irr M, HU^#] by apply: Zbridge0. have A0phi: phi \in 'CF(M, 'A0(M)) by apply: A0bridge0. have a00_1 : a_ 0 0 = 1. rewrite Da cycTIirr00 [sigma 1]cycTIiso1. rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE. rewrite rmorph1 /= -(prTIirr00 ptiWM) -/(mu2_ 0 0) cfdotC. by rewrite cfdotBr cfdot_prTIirr_red omu2S1 // subr0 rmorph1. have aut_phi nu: cfAut nu (tau phi) = tau phi + tau (zeta - cfAut nu zeta). rewrite -Dade_aut !rmorphB !raddfB /= !addrA subrK. by rewrite -prTIred_aut aut_Iirr0. have Za i j: a_ i j \in Cint. rewrite Da Cint_cfdot_vchar ?cycTIiso_vchar //. by rewrite Dade_vchar ?(zchar_onS sHU_A0). have [tau1 coh_tau1] := cohS1; have [_ Dtau1] := coh_tau1. have o_tau1_eta := coherent_ortho_cycTIiso MtypeP sS10 coh_tau1. have a_aut nu i j: a (cfAut nu (eta_ i j)) = a_ i j. symmetry; transitivity '[cfAut nu (tau phi), cfAut nu (eta_ i j)]. by rewrite cfdot_aut_vchar ?cycTIiso_vchar // -Da aut_Cint. rewrite aut_phi cfAut_cycTIiso -cycTIirr_aut [a _]Da cfdotDl addrC. rewrite -Dtau1 ?zcharD1_seqInd ?seqInd_sub_aut_zchar // raddfB cfdotBl. by rewrite !o_tau1_eta ?cfAut_seqInd ?cfAut_irr // subr0 add0r. pose a10 := a_ i1 0; pose a01 := a_ 0 j1; pose a11 := a_ i1 j1. have Da10 i: i != 0 -> a_ i 0 = a10. case/(cfExp_prime_transitive pr_q nz_i1) => k co_k_wi1 Dwi. rewrite -(cforder_dprodl defW) -dprod_IirrEl in co_k_wi1. have [[nu eta10nu] _] := cycTIiso_aut_exists ctiWG co_k_wi1. by rewrite /a_ dprod_IirrEl Dwi rmorphXn /= -dprod_IirrEl eta10nu a_aut. have Da01 j: j != 0 -> a_ 0 j = a01. case/(cfExp_prime_transitive pr_p nz_j1) => k co_k_wj1 Dwj. rewrite -(cforder_dprodr defW) -dprod_IirrEr in co_k_wj1. have [[nu eta01nu] _] := cycTIiso_aut_exists ctiWG co_k_wj1. by rewrite /a_ dprod_IirrEr Dwj rmorphXn /= -dprod_IirrEr eta01nu a_aut. have DaB1 i j: a_ i j = a_ i 0 + a_ 0 j - a_ 0 0. apply: (canRL (addrK _)); rewrite !Da cycTIiso_cfdot_exchange // => x Vx. have /setDP[A0x A'x]: x \in 'A0(M) :\: 'A(M). by rewrite (FTsupp0_typeP maxM MtypeP) // mem_class_support. by rewrite Dade_id // (cfun_on0 (zchar_on Zphi)) // -defA. pose p1 : algC := p.-1%:R; pose q1 : algC := q.-1%:R. have normX: '[X] = 1 + q1 * a10 ^+ 2 + p1 * a01 ^+ 2 + p1 * q1 * a11 ^+ 2. transitivity (\sum_i \sum_j a_ i j ^+ 2). rewrite defX cfnorm_sum_orthonormal // sum_etaW. by apply/eq_bigr=> i _; apply/eq_bigr=> j _; rewrite Cint_normK ?Za. rewrite -addrA addrACA (bigD1 0) //= (bigD1 0) //= a00_1 expr1n. rewrite -natrM !mulr_natl mulrnA -mulrnDl. rewrite -nirrW1 -nirrW2 -!(cardC1 0) -!sumr_const. congr (1 + _ + _); first by apply: eq_bigr => j /Da01->. apply: eq_bigr => i /Da10-Dai0; rewrite (bigD1 0) //= Dai0; congr (_ + _). by apply: eq_bigr => j /Da01-Da0j; rewrite DaB1 Dai0 Da0j -DaB1. have normX_le_q: '[X] <= q%:R. rewrite -(lerD2r '[chi]) -cfnormDd // -Dchi -lerBlDl. have ->: '[tau phi] - q%:R = 1. rewrite Dade_isometry ?A0bridge0 // cfnormBd; last by rewrite omuS1. by rewrite cfnorm_prTIred cfdotS1 // eqxx addrC addKr. suffices: '[chi] != 0. suffices /CnatP[nchi ->]: '[chi] \in Cnat by rewrite ler1n lt0n -eqC_nat. rewrite Cnat_cfnorm_vchar // -(canLR (addKr _) Dchi) defX addrC rpredB //. by rewrite Dade_vchar // (zchar_onS (FTsupp_sub0 M)) ?defA. rewrite big_map big_seq rpred_sum // => _ /(cycTIirrP defW)[i [j ->]]. by rewrite rpredZ_Cint ?Za ?cycTIiso_vchar. pose theta := zeta - zeta^*%CF. have Ztheta: theta \in 'Z[S1, HU^#] by apply: seqInd_sub_aut_zchar. have: '[tau phi, tau theta] != 0. rewrite Dade_isometry //; last by rewrite (cfun_onS _ (zchar_on Ztheta)). rewrite cfdotBl !cfdotBr ?omuS1 ?cfAut_seqInd // subr0 add0r oppr_eq0. rewrite irrWnorm // (seqInd_conjC_ortho _ _ _ S1zeta) ?mFT_odd //. by rewrite subr0 oner_eq0. rewrite cfnorm_eq0 Dchi; apply: contraNneq => ->; rewrite addr0 defX. rewrite -Dtau1 ?zcharD1_seqInd //. rewrite cfdot_suml big_map big1_seq // => _ /(cycTIirrP defW)[i [j ->]]. apply/eqP; rewrite cfdotC fmorph_eq0 cfdotZr raddfB cfdotBl. by rewrite !o_tau1_eta ?cfAut_seqInd ?cfAut_irr // subrr mulr0. have a2_ge0 i j: 0 <= a_ i j ^+ 2 by rewrite -realEsqr Creal_Cint. have a11_0: a11 = 0. have: ('[X] < (2 * q.-1)%:R). rewrite (le_lt_trans normX_le_q) // ltC_nat -subn1 mulnBr ltn_subRL. by rewrite !mul2n -!addnn ltn_add2r odd_prime_gt2 ?mFT_odd. apply: contraTeq => nz_a11; rewrite le_gtF // normX ler_wpDl //. by rewrite !mulr_natl ?addr_ge0 ?ler01 ?mulrn_wge0 ?a2_ge0. rewrite -mulr_natl -natrM ?ler_pM ?natr_ge0 ?sqr_Cint_ge1 ?Za //. by rewrite leC_nat leq_mul // -subn1 ltn_subRL odd_prime_gt2 ?mFT_odd. rewrite a11_0 expr0n /= mulr0 addr0 in normX. have a10_a01: a10 + a01 = 1. by apply/eqP; rewrite -subr_eq0 -a00_1 -DaB1 -/a11 a11_0. have{} o_chi_eta: orthogonal chi etaW. by apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->]. have a10_0: a10 = 0. apply: contraNeq (FTtype34_not_ortho_cycTIiso S1zeta) => nz_a10. have a01_0: a01 = 0. apply: contraTeq normX_le_q => nz_a01; rewrite normX lt_geF //. rewrite ltr_pwDr 1?mulr_gt0 ?ltr0n -?subn1 ?subn_gt0 ?prime_gt1 //. by rewrite lt_def sqrf_eq0 nz_a01 a2_ge0. rewrite -lerBlDl -(natrB _ (prime_gt0 pr_q)) subn1 -mulr_natl. by rewrite ler_wpM2l ?ler0n // sqr_Cint_ge1 ?Za. suffices <-: X = eta_col 0 by rewrite Dchi /eq_proj_eta addrC addKr. rewrite defX sum_etaW exchange_big (bigD1 0) //= addrC. rewrite big1 ?add0r => [|j nz_j]; first apply: eq_bigr => i _; last first. rewrite (bigD1 0) // [a _]Da01 //= a01_0 scale0r add0r big1 // => i nz_i. by rewrite [a _]DaB1 Da10 // Da01 // a10_a01 a00_1 subrr scale0r. have [-> | nz_i] := eqVneq i 0; first by rewrite [a _]a00_1 scale1r. by rewrite [a _]Da10 // (canRL (addrK _) a10_a01) a01_0 subr0 scale1r. suffices <-: X = eta0row by rewrite Dchi /eq_proj_eta addrC addKr. rewrite defX sum_etaW (bigD1 0) //= addrC. rewrite big1 ?add0r => [|i nz_i]; first apply: eq_bigr => j _; last first. rewrite (bigD1 0) // [a _]Da10 //= a10_0 scale0r add0r big1 // => j nz_j. by rewrite [a _]DaB1 Da10 // Da01 // a10_a01 a00_1 subrr scale0r. have [-> | nz_j] := eqVneq j 0; first by rewrite [a _]a00_1 scale1r. by rewrite [a _]Da01 // (canRL (addKr _) a10_a01) a10_0 oppr0 add0r scale1r. have [zeta [irr_zeta Szeta zeta1]] := FTtypeP_ref_irr maxM MtypeP. have{zeta1} [S1zeta zeta1]: zeta \in S1 /\ zeta 1%g = q%:R. split=> //; have [k nz_k Dzeta] := seqIndC1P Szeta. rewrite Dzeta mem_seqInd // !inE subGcfker nz_k -defM'' lin_char_der1 //. rewrite -mulr_natl Dzeta cfInd1 //= -(index_sdprod defM) in zeta1. by apply/andP; rewrite irr_char -(mulfI _ zeta1) ?neq0CG. have{Szeta} ltpq: (p < q)%N. rewrite ltn_neqAle neq_pq leqNgt /=. apply: contra (FTtype34_not_ortho_cycTIiso S1zeta) => ltqp. case/(FTtype345_Dade_bridge0 _ MtypeP): Szeta => // chi [-> _ _ o_chi_eta]. rewrite /eq_proj_eta addrC addKr (orthogonal_oppl chi). by apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->]. suffices galM: typeP_Galois MtypeP. have [_ [_ _ _ [/= cycUbar _ _]]] := typeP_Galois_P maxM notMtype5 galM. have{} cycUbar: cyclic (U / U') by rewrite -defU' -defC. have nilU: nilpotent U by have [_ []] := MtypeP. case/orP: Mtype34 => // /(compl_of_typeIV maxM MtypeP)[_ /negP[]]. exact/cyclic_abelian/cyclic_nilpotent_quo_der1_cyclic. apply: contraLR ltpq => gal'M; rewrite -leqNgt (leq_trans _ (leq_pred _)) //. have [_ _ _] := typeP_nonGalois_characters maxM notMtype5 gal'M. case: (_ gal'M) => H1 /= [_ _ nH1U _ []]; set a := #|U : _| => a_gt1. rewrite def_p -/q -defU' -defS2 => a_dv_p1 cycUhat _. set irr_qa := [pred lambda in irr M | lambda 1%g == (q * a)%:R] => S2_qa. have{S2_qa}/hasP[lambda S2lambda /andP[irr_lambda /eqP-lambda1]]: has irr_qa S2. have [a2_dv_pu] := S2_qa; rewrite has_count; apply: leq_trans. rewrite -(@ltn_pmul2r (a ^ 2 * #|C|)); last first. by rewrite !muln_gt0 (ltnW a_gt1) cardG_gt0. by rewrite mul0n divnK // muln_gt0 cardG_gt0 -subn1 subn_gt0 prime_gt1. have{nH1U cycUhat} a_dv_u: a %| u. rewrite /u card_quotient ?normal_norm // indexgS // defU'. rewrite der1_min ?cyclic_abelian // normsI ?normG //. by rewrite (subset_trans nH1U) // astab_norm. pose j := j1; pose psi := mu_ j - (u %/ a)%:R *: lambda. have /andP/=[red_muj S2muj]: mu_ j \in [predD S2 & irr M]. by rewrite memS2red image_f. have S2psi: psi \in 'Z[S2, M^#]. rewrite zcharD1E rpredB ?rpredZnat ?mem_zchar //=. by rewrite !cfunE mu_1 // lambda1 -natrM mulnCA divnK ?subrr. pose phi := tau (mu_ 0 - zeta). have o_phi_psi: '[phi, tau psi] = 0. have Apsi: psi \in 'CF(M, 'A(M)) by rewrite defA (zcharD1_seqInd_on _ S2psi). have [Tzeta Tlambda] := (seqInd_subT S1zeta, seqInd_subT S2lambda). rewrite Dade_isometry ?A0bridge0 ?(cfun_onS (FTsupp_sub0 M)) //. rewrite cfdotBl !cfdotBr !cfdotZr cfdot_prTIred eq_sym (negPf nz_j1) add0r. rewrite !(seqInd_ortho _ Tzeta) ?Tmu ?(memPnC (sS1S2' S1zeta)) // add0r. rewrite (seqInd_ortho _ (Tmu 0)) ?(memPnC (prTIred_not_irr _ _)) // !mulr0. by rewrite subrr. have [tau2 coh_tau2] := cohS2; have [[_ Ztau2] Dtau2] := coh_tau2. have ua_1: (u %/ a)%:R * `|'[phi, tau2 lambda]| == 1. rewrite -normr_nat -normrM mulr_natl -!raddfMn -[_ *+ _](subrK (mu_ j)) /=. rewrite -opprB addrC raddfB cfdotBr -scaler_nat (Dtau2 _ S2psi) o_phi_psi. case: (FTtypeP_coherent_TIred _ coh_tau2 _ S2lambda S2muj) => // -[b k] -> _. rewrite -/(eta_col k) cfdotZr rmorph_sign subr0 normrMsign. rewrite -[phi](subrK eta0row) cfdotDl cfdot_sumr big1 => [|j' _]; last first. by rewrite (orthoPl (bridgeS1 _ _)) ?map_f ?mem_irr. rewrite add0r cfdotC norm_conjC cfdot_sumr (bigD1 k) //= proj_col_eta eqxx. by rewrite big1 ?addr0 ?normr1 // => i k'i; rewrite proj_col_eta (negPf k'i). have Du: u = a. apply/eqP; rewrite -[a]mul1n eqn_mul ?(ltnW a_gt1) // -eqC_nat. move: ua_1; rewrite Cnat_mul_eq1 ?rpred_nat //; first by case/andP. rewrite Cnat_norm_Cint ?Cint_cfdot_vchar //; last by rewrite Ztau2 ?mem_zchar. rewrite Dade_vchar // zchar_split A0bridge0 //. by rewrite rpredB ?char_vchar ?prTIred_char ?irrWchar. have lequ: (q <= u)%N. have u1_gt0: (0 < u.-1)%N by rewrite -subn1 subn_gt0 Du. rewrite (leq_trans _ (leq_pred u)) // dvdn_leq //. suffices ->: q = #|W1 / C|%g by apply: Frobenius_dvd_ker1 frobUW1bar. apply/card_isog/quotient_isog; first by have [] := joing_subP nC_UW1. by rewrite setIAC (coprime_TIg coUq) setI1g. by rewrite (leq_trans lequ) // Du dvdn_leq // -subn1 subn_gt0 prime_gt1. 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 ssrint algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10)