proposition: Lemma Ptype_core_coherence : coherent (S_ H0C') M^# tau.
proof: Proof. have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM. have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU. have nsCU: C <| U := normalS sCU (joing_subl _ _) nsCUW1. have [_ nCU] := andP nsCU; have sC'C: C^`(1)%g \subset C := der_sub 1 _. have coHC := coprimegS sCU coHU; have coH0C := coprimeSg sH0H coHC. have [nsH0C_M nsHC_M nsH0U'_M nsH0C'_M] := nsH0xx_M; have [_ nH0H]:= andP nsH0H. have nH0HU := subset_trans sHUM nH0M; have nH0U := subset_trans sUHU nH0HU. have nH0C := subset_trans sCU nH0U; have nH0C' := subset_trans sC'C nH0C. have sHCHU: HC \subset HU by rewrite join_subG sHHU (subset_trans sCU). have [nsHCHU nHC] := (normalS sHCHU sHUM nsHC_M, subset_trans sCU nHU). have tiHCbar: Hbar :&: (C / H0)%g = 1%g by rewrite coprime_TIg ?coprime_morph. have defHCbar: Hbar \x (C / H0) = (HC / H0)%g. by rewrite dprodEY ?quotientY // [C]unlock/= astabQ quotient_setIpre subsetIr. have{tiHCbar} defHC'bar: (HC / H0)^`(1)%g = (C^`(1) / H0)%g. by rewrite -(der_dprod 1 defHCbar) (derG1P abHbar) dprod1g quotient_der. have sU'U := der_sub 1 U; have nH0U' := subset_trans sU'U nH0U. have sU'C: U' \subset C. by rewrite [C]unlock subsetI sub_astabQ sU'U nH0U' quotient_cents. have uS0: uniq (S_ H0C') by apply: seqInd_uniq. have [rmR scohS0]: exists R : 'CF(M) -> seq 'CF(G), subcoherent (S_ H0C') tau R. move: (FTtypeP_coh_base _ _) (FTtypeP_subcoherent maxM MtypeP) => R scohR. exists R; apply: (subset_subcoherent scohR). split=> //; last exact: cfAut_seqInd. by apply: seqIndS; rewrite Iirr_kerDS ?sub1G ?Fcore_sub_FTcore. have [GalM | Gal'M] := boolP typeP_Galois. have [_ XOC'u _ _] := typeP_Galois_characters GalM. apply: uniform_degree_coherence scohS0 _. apply: all_pred1_constant (#|M : HU| * u)%:R _ _; rewrite all_map. by apply/allP=> _ /seqIndP[s /XOC'u[s1u _] ->] /=; rewrite natrM cfInd1 ?s1u. have:= typeP_nonGalois_characters Gal'M. set U1 := 'C_U(_ | _); set a := #|_ : _|. case: (_ Gal'M) => /= H1 [oH1 nH1U _ defHbar aP] in U1 a *. rewrite -/U1 -/a in aP; case: aP => a_gt1 a_dv_p1 cycU1 _. case=> [a_dv_XH0 [nb_mu IndHCmu] has_irrHC lb_Sqa]; rewrite -[S_ _]/(S_ H0C'). have defHb1 := defHbar; rewrite (big_setD1 1%g) ?group1 ?conjsg1 //= in defHb1. have [[_ H1c _ defH1c] _ _ _] := dprodP defHb1; rewrite defH1c in defHb1. have [nsH1H _] := dprod_normal2 defHb1; have [sH1H _] := andP nsH1H. have nsU1U: U1 <| U; last have [sU1U nU1U] := andP nsU1U. by rewrite norm_normalI // astabQ norm_quotient_pre ?norms_cent. have Da: a = #|HU : H <*> U1|. rewrite /a -!divgS /= ?join_subG ?sHHU ?norm_joinEr ?(subset_trans sU1U) //=. by rewrite -(sdprod_card defHU) coprime_cardMg ?(coprimegS sU1U) ?divnMl. have sCU1: C \subset U1 by rewrite [C]unlock setIS ?astabS. have a_dv_u: a %| u by rewrite Da Du indexgS ?genS ?setUS. have [a_gt0 q_gt0 u_gt0 p1_gt0]: [/\ 0 < a, 0 < q, 0 < u & 0 < p.-1]%N. rewrite !cardG_gt0 ltnW // -subn1 subn_gt0 prime_gt1 //. have [odd_p odd_q odd_a]: [/\ odd p, odd q & odd a]. by rewrite mFT_odd -oH1 (oddSg sH1H) ?(dvdn_odd a_dv_u) ?mFT_quo_odd. have Dp: p = (2 * p.-1./2 + 1)%N. by rewrite mul2n -[p]odd_double_half odd_p half_double addn1. pose S1 := filter [pred zeta : 'CF(M) | zeta 1%g == (q * a)%:R] (S_ H0C'). have ntS1: (0 < size S1)%N. have [lb_dv lbS1] := lb_Sqa; apply: leq_trans (leq_trans lbS1 _). by rewrite ltn_divRL // mul0n muln_gt0 p1_gt0 cardG_gt0. rewrite -size_filter uniq_leq_size ?filter_uniq ?seqInd_uniq // => chi. rewrite !mem_filter -andbA /= => /and3P[_ ->]. by apply: seqIndS; rewrite Iirr_kerDS // genS ?setUS ?dergS ?subsetIl. have sS10: cfConjC_subset S1 (S_ H0C'). split=> [||chi]; first by rewrite filter_uniq. by apply: mem_subseq; apply: filter_subseq. rewrite !mem_filter !inE cfunE /= => /andP[/eqP <- S0chi]. by rewrite cfAut_seqInd // andbT conj_Cnat ?(Cnat_seqInd1 S0chi). have cohS1: coherent S1 M^# tau. apply: uniform_degree_coherence (subset_subcoherent scohS0 sS10) _. by apply: all_pred1_constant (q * a)%:R _ _; rewrite all_map filter_all. pose S3 := filter [predC S1] (S_ H0C'); move: {2}_.+1 (ltnSn (size S3)) => nS. move: @S3 (sS10) (cohS1); have: {subset S1 <= S1} by []. elim: nS {-1}S1 => // nS IHnS S2 => sS12 S3 sS20 cohS2; rewrite ltnS => leS3nS. have [ntS3|] := boolP (size S3 > 0)%N; last first. rewrite size_filter -has_count has_predC negbK => /allP sS02. exact: subset_coherent sS02 cohS2. suff [chi]: exists2 chi, chi \in S3 & coherent (chi :: chi^* :: S2)%CF M^# tau. rewrite mem_filter => /andP[/= S2'chi S0chi]; have [uS2 sS2S0 ccS2] := sS20. move/IHnS; apply=> [psi /sS12 S1psi||]; first by rewrite 2?mem_behead. split. - rewrite /= !inE negb_or S2'chi (contra (ccS2 _)) ?cfConjCK // eq_sym. by rewrite (seqInd_conjC_neq _ _ _ S0chi) ?mFT_odd. - by apply/allP; rewrite /= S0chi cfAut_seqInd //=; apply/allP. apply/allP; rewrite /= !inE cfConjCK !eqxx orbT /=. by apply/allP=> psi /ccS2; rewrite !inE orbA orbC => ->. apply: leq_trans leS3nS; rewrite ltnNge; apply: contra S2'chi. case/uniq_min_size=> [|psi|_ /(_ chi)]; first by rewrite filter_uniq. by rewrite !mem_filter !inE orbA negb_or -andbA => /andP[]. by rewrite !mem_filter !inE eqxx S0chi !andbT => /esym/negbFE. clear nS IHnS leS3nS. without loss [[eqS12 irrS1 H0C_S1] [Da_p defC] [S3qu ne_qa_qu] [oS1 oS1ua]]: / [/\ [/\ S1 =i S2, {subset S1 <= irr M} & {subset S1 <= S_ H0C}], a = p.-1./2 /\ C :=: U', (forall chi, chi \in S3 -> chi 1%g == (q * u)%:R) /\ (q * u != q * a)%N & size S1 = (p.-1 * u %/ a ^ 2)%N /\ size S1 = (2 * u %/ a)%N]. - move=> IHwlog; have{sS20} [[uS2 sS20 ccS2] [uS1 _ _]] := (sS20, sS10). pose is_qu := [pred chi : 'CF(M) | chi 1%g == (q * u)%:R]. pose isn't_qu := [pred chi | is_qu chi ==> all is_qu S3]. have /hasP[chi S3chi qu'chi]: has isn't_qu S3. rewrite /isn't_qu; have [_|] := boolP (all _ _); last by rewrite has_predC. by rewrite (eq_has (fun _ => implybT _)) has_predT. have [S2'chi S0chi]: chi \notin S2 /\ chi \in S_ H0C'. by apply/andP; rewrite mem_filter in S3chi. have [s X0C's Dchi] := seqIndP S0chi. have Dchi1: chi 1%g = q%:R * 'chi_s 1%g. by rewrite Dchi cfInd1 // -(index_sdprod defM). pose lb0 := (2 * q * a)%:R * chi 1%g. pose lb1 : algC := (2 * a * q ^ 2 * u)%:R. pose lb2 : algC := (p.-1 * q ^ 2 * u)%:R. pose lb3 : algC := (p.-1 * q ^ 2 * #|U : U'|)%:R. pose S1' := filter [predI irr M & S_ H0U'] S1. pose szS1' := ((p.-1 * #|U : U'|) %/ a ^ 2)%N; set lbS1' := _ %/ _ in lb_Sqa. pose Snorm (psi : 'CF(M)) := psi 1%g ^+ 2 / '[psi]. pose sumnS Si := \sum_(psi <- Si) Snorm psi. have lb01: lb0 <= lb1 ?= iff (chi 1%g == (q * u)%:R). rewrite /lb1 mulnA -mulnA natrM /lb0 mulnAC mono_leif; last first. by apply: ler_pM2l; rewrite ltr0n !muln_gt0 a_gt0. apply: leif_eq; rewrite Dchi1 natrM ler_pM2l ?gt0CG //. have [KsH0C' _] := setDP X0C's; rewrite inE in KsH0C'. have [t sHCt] := constt_cfRes_irr HC s. have KtH0C': H0C' \subset cfker 'chi_t. apply: subset_trans (cfker_constt (cfRes_char _ (irr_char s)) sHCt). by rewrite cfker_Res ?irr_char // subsetI genS ?setUSS. rewrite -constt_Ind_Res in sHCt. apply: le_trans (char1_ge_constt (cfInd_char _ (irr_char t)) sHCt) _. rewrite cfInd1 // -Du lin_char1 ?mulr1 // lin_irr_der1. apply: subset_trans KtH0C'; rewrite /= (norm_joinEr nH0C') /= -/C. rewrite -quotientSK ?(subset_trans (der_sub _ _)) ?(subset_trans sHCHU) //. by rewrite -defHC'bar quotient_der ?(subset_trans sHCHU). have lb12: lb1 <= lb2 ?= iff (a == p.-1./2). rewrite -(@eqn_pmul2l 2) // -(canLR (addnK 1) Dp) subn1 leif_nat_r. rewrite !(mono_leqif (fun _ _ => leq_pmul2r _)) ?expn_gt0 ?q_gt0 //. apply: leqif_eq; rewrite dvdn_leq // Gauss_dvd //. by rewrite {1}Dp addn1 dvdn_mulr. by rewrite prime_coprime ?dvdn2 ?negbK. have lb23: lb2 <= lb3 ?= iff (C :==: U') :> algC. rewrite leif_nat_r [u]card_quotient //. rewrite (mono_leqif (fun _ _ => leq_pmul2l _)) ?muln_gt0 ?p1_gt0 ?q_gt0 //. rewrite -(mono_leqif (fun _ _ => leq_pmul2l (cardG_gt0 C))) Lagrange //. rewrite -(Lagrange sU'U) (mono_leqif (fun _ _ => leq_pmul2r _)) //. by rewrite eq_sym; apply: subset_leqif_cards. have lb3S1': lb3 <= sumnS S1' ?= iff (size S1' == szS1'). rewrite /szS1' -(divnMr (cardG_gt0 U')) mulnAC -mulnA Lagrange // -/lbS1'. have{lb_Sqa} [dv_lb lbSqa] := lb_Sqa; rewrite [sumnS S1']big_seq. rewrite (eq_bigr (fun _ => ((q * a) ^ 2)%:R)) => [|psi]; last first. rewrite !mem_filter -!andbA => /and4P[/irrP[r ->] _ /=/eqP r1qa _]. by rewrite /Snorm cfnorm_irr divr1 r1qa natrX. rewrite -big_seq (big_nth 0) -natr_sum sum_nat_const_nat subn0. rewrite mulnC natrM [*%R]lock /lb3 natrM natf_indexg ?der_sub // mulrA. rewrite -natrM mulnAC -(divnK dv_lb) mulnAC mulnA natrM mulfK ?neq0CG //. rewrite -/lbS1' -mulnA -expnMn natrM mulrC -lock mono_leif; last first. by apply: ler_pM2l; rewrite ltr0n !muln_gt0 a_gt0 q_gt0. rewrite eq_sym leif_nat_r; apply: leqif_eq; rewrite (leq_trans lbSqa) //. rewrite -size_filter uniq_leq_size ?filter_uniq ?seqInd_uniq // => psi. rewrite !mem_filter -!andbA /= => /and3P[-> -> S0psi]; rewrite S0psi. by apply: seqIndS S0psi; rewrite Iirr_kerDS //= genS ?setUS ?dergS. have lbS1'2: sumnS S1' <= sumnS S2 ?= iff ~~ has [predC S1'] S2. have Ds2: perm_eq S2 (S1' ++ filter [predC S1'] S2). rewrite -(perm_filterC (mem S1')) perm_cat2r. rewrite uniq_perm ?filter_uniq // => psi. by rewrite mem_filter andb_idr //= mem_filter => /andP[_ /sS12]. rewrite [sumnS S2](perm_big _ Ds2) big_cat /= -/(sumnS S1') big_filter. rewrite -all_predC -big_all_cond !(big_tnth _ _ S2) big_andE. rewrite -{1}[_ S1']addr0 mono_leif; last exact: lerD2l. set sumS2' := \sum_(i | _) _; rewrite -[0]/(sumS2' *+ 0) -sumrMnl. apply: leif_sum => i _; apply/leifP; rewrite lt0r !mulf_eq0 invr_eq0. set psi := tnth _ i; have Spsi := sS20 psi (mem_tnth _ _). rewrite !negb_or (seqInd1_neq0 _ Spsi) //= (cfnorm_seqInd_neq0 _ Spsi) //=. by rewrite divr_ge0 ?exprn_ge0 ?cfnorm_ge0 ?Cnat_ge0 ?(Cnat_seqInd1 Spsi). have [lb0S2 | ] := boolP (lb0 < sumnS S2). exists chi => //; have /hasP[xi S1xi _]: has predT S1 by rewrite has_predT. have xi1: xi 1%g = (q * a)%:R. by rewrite mem_filter in S1xi; have [/eqP] := andP S1xi. apply: (extend_coherent scohS0 _ (sS12 _ S1xi)) => //. split=> //; last by rewrite mulrAC xi1 -natrM mulnA. rewrite xi1 Dchi1 irr1_degree -natrM dvdC_nat dvdn_pmul2l ?cardG_gt0 //. rewrite -dvdC_nat /= !nCdivE -irr1_degree a_dv_XH0 //. by rewrite (subsetP (Iirr_kerDS _ _ _) _ X0C's) ?joing_subl. have lb1S2 := leif_trans lb12 (leif_trans lb23 (leif_trans lb3S1' lbS1'2)). rewrite lt_neqAle !(leif_trans lb01 lb1S2) andbT has_predC !negbK. case/and5P=> /eqP-chi1qu /eqP-Da_p /eqP-defC /eqP-sz_S1' /allP/=sS21'. have defS1': S1' = S1. apply/eqP; rewrite -(geq_leqif (size_subseq_leqif (filter_subseq _ S1))). by rewrite uniq_leq_size // => psi /sS12/sS21'. apply: IHwlog; split=> //. + split=> psi; do 1?[rewrite -defS1' mem_filter andbC => /and3P[_ _] //=]. by apply/idP/idP=> [/sS12 | /sS21']; rewrite ?defS1'. by congr (_ \in S_ _); apply/group_inj; rewrite /= defC. + split; first by apply/allP; apply: contraLR qu'chi; rewrite /= chi1qu eqxx. rewrite -eqC_nat -chi1qu; apply: contra S2'chi => chi1qa. by rewrite sS12 // mem_filter /= chi1qa. rewrite -defS1' sz_S1' /szS1' -defC -card_quotient // -/u. by split=> //; rewrite -mulnn {1}Dp addn1 -Da_p mulnAC divnMr. have nCW1: W1 \subset 'N(C). by rewrite (subset_trans (joing_subr U W1)) ?normal_norm. clear sS20 cohS2 sS12 has_irrHC lb_Sqa sU'C. have [tiU1 le_u_a2]: {in W1^#, forall w, U1 :&: U1 :^ w = C} /\ (u <= a ^ 2)%N. have tiU1 w: w \in W1^# -> U1 :&: U1 :^ w = C; last split => //. case/setD1P=> ntw W1w; have nH0w := subsetP (subset_trans sW1M nH0M) w W1w. pose wb := coset H0 w; have W1wb: wb \in W1bar^#. rewrite !inE mem_quotient ?(contraNneq _ ntw) // => /coset_idr H0w. rewrite -in_set1 -set1gE -tiHUW1 inE (subsetP sHHU) // (subsetP sH0H) //. by rewrite H0w. have ntH1 w1: H1 :^ w1 :!=: 1%g by rewrite -cardG_gt1 cardJg oH1 prime_gt1. pose t_ w1 := if pred2 1%g wb w1 then sval (has_nonprincipal_irr (ntH1 w1)) else 0. pose theta := cfDprodl defHCbar (cfBigdprod defHbar (fun w1 => 'chi_(t_ w1))). have lin_theta : theta \is a linear_char. rewrite cfDprodl_lin_char ?cfBigdprod_lin_char // => w1 _. by rewrite irr_prime_lin ?cardJg ?oH1. have nsH0HC: H0 <| HC. by rewrite /normal join_subG nH0H sub_gen ?subsetU ?sH0H. move defK: H0C => K. have kerK: K \subset cfker (theta %% H0). rewrite -defK sub_cfker_mod ?join_subG ?normG ?quotientYidl //. exact: cfker_sdprod. have sKHC: K \subset HC by rewrite -defK genS ?setSU. have nsKHC: K <| HC by rewrite (normalS sKHC (normal_sub nsHC_M)) -?defK. have sH0K: H0 \subset K by rewrite -defK joing_subl. have nsKHU: K <| HU. by rewrite (normalS (subset_trans sKHC sHCHU) sHUM) -?defK. have [t2 Dt2]: {t2 : Iirr (HC / K) | 'chi_t2 %% K = theta %% H0}%CF. exists (cfIirr ((theta %% H0) / K)). by rewrite cfIirrE ?cfQuoK ?cfQuo_irr ?cfMod_irr ?lin_char_irr. have nsHChatHU: HC / K <| HU / K by rewrite quotient_normal. have sHChatHU := normal_sub nsHChatHU. pose That := 'I_(HU / K)['chi_t2]%G. have sThatHU: That \subset (HU / K)%G := Inertia_sub _ _. have abThatHC: abelian (That / (HC / K)). rewrite (abelianS (quotientS _ sThatHU)) //. rewrite (isog_abelian (third_isog _ _ _)) // defC. rewrite -(isog_abelian (quotient_sdprodr_isog defHU _)) ?gFnormal //. by rewrite sub_der1_abelian. have hallHChat: Hall That (HC / K). rewrite /Hall -(card_isog (third_isog sH0K nsH0HC nsKHC)) /=. rewrite sub_Inertia // -[in #|_|]defK /= quotientYidl //. rewrite -(card_isog (sdprod_isog (dprodWsdC defHCbar))). apply: coprime_dvdr (indexSg (sub_Inertia _ sHChatHU) sThatHU) _. apply: coprime_dvdr (index_quotient _) _. by rewrite subIset // normal_norm. by rewrite -Du coprime_morphl // coprime_morphr. have [s t2HUs] := constt_cfInd_irr t2 sHChatHU. have s_1: ('chi_s %% K)%CF 1%g = #|U : U1 :&: U1 :^ w|%:R. rewrite cfMod1. have [||_ _ ->] // := cfInd_Hall_central_Inertia _ abThatHC. rewrite -cfMod1 Dt2 cfMod1 lin_char1 //= mulr1 -inertia_mod_quo // Dt2. rewrite index_quotient_eq ?normal_norm ?Inertia_sub ?setIS //; last first. by rewrite (subset_trans sKHC) ?sub_inertia. rewrite /= inertia_morph_pre //= -quotientE inertia_dprodl; first 1 last. - by rewrite quotient_norms ?normal_norm. - rewrite /= -(quotientYidl nH0C) quotient_norms ?normal_norm //. by rewrite -defK in nsKHU. have nH1wHU w1: w1 \in (W1 / H0)%g -> (HU / H0)%g \subset 'N(H1 :^ w1). move=> W1w1; rewrite -(normsP (quotient_norms H0 nHUW1) _ W1w1) normJ. rewrite conjSg /= -(sdprodW defHU) quotientMl ?mul_subG //. exact: normal_norm. rewrite indexgI /= inertia_bigdprod_irr // (big_setD1 1%g) ?group1 //=. rewrite 2!{1}setIA setIid (bigD1 wb) //= {1 2}/t_ /= !eqxx ?orbT /=. rewrite !(inertia_irr_prime _ p_pr) ?cardJg //=; try by case: (has_nonprincipal_irr _). rewrite conjsg1 centJ setIA -setIIr /=. elim/big_rec: _ => [|w1 Uk /andP[/setD1P[ntw1 Ww1] w'w1] IHk]; last first. rewrite /t_ -if_neg negb_or ntw1 w'w1 irr0 Inertia1 -?setIIr 1?setIA //. rewrite /normal nH1wHU //= -(normsP (quotient_norms H0 nHUW1) _ Ww1). by rewrite conjSg (subset_trans sH1H) ?quotientS. rewrite setIT !morphpreI morphpreJ ?(subsetP nH0W1) //= -astabQ. rewrite quotientGK //; last by rewrite /normal (subset_trans sH0H). rewrite -(sdprodWY (sdprod_modl defHU _)); last first. rewrite subsetI -sub_conjgV. rewrite (normsP (gFnorm _ _)) ?groupV ?(subsetP sW1M) //= andbb. by rewrite sub_astabQ nH0H sub_abelian_cent. rewrite -(index_sdprodr defHU) ?subsetIl // conjIg (normsP nUW1) //. by rewrite -setIIr. apply/esym/eqP; rewrite eqEcard subsetI -sub_conjgV. rewrite (normsP _ _ (groupVr W1w)) ?sCU1 /=; last first. by rewrite (subset_trans (joing_subr U W1)) ?normal_norm. have{s_1} : pred2 u a #|U : U1 :&: U1 :^ w|. rewrite /= -!eqC_nat -{}s_1 -mod_IirrE //. pose phi := 'Ind[M] 'chi_(mod_Iirr s). have Sphi: phi \in S_ H0C'. rewrite mem_seqInd ?gFnormal // !inE mod_IirrE //. rewrite andbC (subset_trans _ (cfker_mod _ _)) //=; last first. by rewrite -defK genS ?setUS ?der_sub. rewrite sub_cfker_mod ?(subset_trans sHHU) ?normal_norm //. have sHHC: H \subset HC by rewrite joing_subl. rewrite -(sub_cfker_constt_Ind_irr t2HUs) ?quotientS //; last first. by rewrite quotient_norms ?normal_norm. rewrite -sub_cfker_mod ?(subset_trans sHHU (normal_norm nsKHU)) //. rewrite Dt2 sub_cfker_mod //. apply: contra (valP (has_nonprincipal_irr (ntH1 1%g))). move/eq_cfker_Res; rewrite cfDprodlK => kerHbar. have:= sH1H; rewrite -{1}(conjsg1 H1) -kerHbar => /eq_cfker_Res. by rewrite cfBigdprodKabelian ?group1 // /t_ /= eqxx -subGcfker => ->. have [/S3qu | ] := boolP (phi \in S3). rewrite cfInd1 // natrM -(index_sdprod defM). by rewrite (inj_eq (mulfI (neq0CG _))) => ->. rewrite mem_filter Sphi andbT negbK /= -eqS12 mem_filter Sphi andbT /=. rewrite cfInd1 // natrM -(index_sdprod defM) (inj_eq (mulfI (neq0CG _))). by rewrite orbC => ->. case/pred2P=> [iUCu | iUCa]. rewrite -(leq_pmul2r u_gt0) -{1}iUCu /u card_quotient ?Lagrange //. by rewrite /= -setIA subsetIl. rewrite subset_leq_card // subIset // [C]unlock subsetI subsetIl sub_astabQ. rewrite subIset ?nH0U //= centsC -(bigdprodWY defHbar) gen_subG. apply/orP; left; apply/bigcupsP=> w1 Ww1; rewrite centsC centJ -sub_conjgV. rewrite (normsP _ _ (groupVr Ww1)) ?quotient_norms //. by rewrite /U1 astabQ quotient_setIpre subsetIr. rewrite prime_meetG //; apply/trivgPn; exists w; rewrite // !inE W1w. rewrite (sameP setIidPr eqP) eqEcard subsetIr /= cardJg. by rewrite -(leq_pmul2r a_gt0) -{2}iUCa !Lagrange //= -setIA subsetIl. have /trivgPn[w W1w ntw]: W1 :!=: 1%g by rewrite -cardG_gt1 prime_gt1. rewrite -(leq_pmul2l u_gt0) mulnn. have nCU1 := subset_trans sU1U nCU. have {1}->: u = (#|(U1 / C)%g| * a)%N. by rewrite mulnC /u !card_quotient // Lagrange_index. rewrite expnMn leq_pmul2r ?expn_gt0 ?orbF // -mulnn. rewrite -{2}[U1](conjsgK w) quotientJ ?groupV ?(subsetP nCW1) //. rewrite cardJg -TI_cardMg /= -/U1 ?subset_leq_card //. rewrite mul_subG ?quotientS ?subsetIl //. by rewrite -(normsP nUW1 w W1w) conjSg subsetIl. by rewrite -quotientGI // tiU1 ?trivg_quotient // !inE ntw. pose S4 := filter [predD S_ H0C & redM] S3. have sS43: {subset S4 <= S3} by apply: mem_subseq; apply: filter_subseq. have nsHM: H <| M by apply: gFnormal. have oS4: (q * u * size S4 + p.-1 * (q + u))%N = (p ^ q).-1. rewrite mulnAC {1}[q](index_sdprod defM) -[S4]filter_predI. rewrite (size_irr_subseq_seqInd _ (filter_subseq _ _)) //; last first. by move=> xi; rewrite mem_filter -!andbA negbK => /andP[]. set Xn := finset _; pose sumH0C := \sum_(s in X_ H0C) 'chi_s 1%g ^+ 2. have /eqP: sumH0C = (q * size S1 * a ^ 2 + (#|Xn| + p.-1) * u ^ 2)%:R. rewrite [q](index_sdprod defM) natrD natrM natrX. rewrite (size_irr_subseq_seqInd _ (filter_subseq _ _)) //= -/S1. have sH0CC': {subset S_ H0C <= S_ H0C'}. by apply: seqIndS; rewrite Iirr_kerDS // genS ?setUS ?der_sub. rewrite [sumH0C](big_setID [set s | 'Ind 'chi_s \in S1]) /=; congr (_ + _). rewrite mulr_natl -[rhs in _ = rhs]sumr_const; apply: eq_big => s. by rewrite in_setI inE andb_idl // => /H0C_S1; rewrite mem_seqInd. rewrite 2!inE mem_filter andbCA /= cfInd1 // -(index_sdprod defM) natrM. by case/andP=> /eqP/(mulfI (neq0CG _))->. rewrite (eq_bigr (fun _ => u%:R ^+ 2)) => [|s]; last first. rewrite 2!inE eqS12 => /andP[S2's H0Cs]; congr (_ ^+ 2). have /S3qu/eqP: 'Ind 'chi_s \in S3. by rewrite mem_filter /= S2's sH0CC' ?mem_seqInd. by rewrite natrM cfInd1 // -(index_sdprod defM) => /(mulfI (neq0CG _)). rewrite sumr_const -mulr_natl natrM natrX -nb_mu; congr (_%:R * _). have [_ s_mu_H0C] := nb_redM_H0. rewrite (size_red_subseq_seqInd_typeP MtypeP _ s_mu_H0C); last first. - by apply/allP; apply: filter_all. - by rewrite filter_uniq ?seqInd_uniq. rewrite -/mu_ -[#|_|](cardsID Xn) (setIidPr _); last first. apply/subsetP=> s; rewrite inE in_setD mem_filter /= -!andbA -eqS12. rewrite mem_seqInd ?gFnormal // => /and4P[_ -> S1'xi _]. by rewrite inE S1'xi. congr (_ + _)%N; apply: eq_card => i; rewrite inE -/mu_ 2!inE. rewrite -[seqInd M _]/(S_ H0C') mem_filter /= andbC 2!inE eqS12 -!andbA. rewrite -(mem_seqInd nsHUM) // -/(S_ H0C); set xi := 'Ind _. apply/idP/idP=> [/and3P[-> H0Cxi] | mu_xi]. rewrite H0Cxi sH0CC' //= andbT negbK mem_filter unfold_in => ->. by rewrite (seqIndS _ H0Cxi) // Iirr_kerDS ?joing_subl. have [xi1u H0Cxi _] := IndHCmu _ mu_xi. rewrite H0Cxi -eqS12 mem_filter sH0CC' //= !andbT xi1u eqC_nat ne_qa_qu. by rewrite andbT negbK mem_filter in mu_xi *; case/andP: mu_xi. rewrite oS1 -mulnA divnK ?dvdn_mul // !mulnA -mulnDl mulnC natrM {}/sumH0C. rewrite /X_ -Iirr_kerDY joingC joingA (joing_idPl sH0H) /=. rewrite sum_Iirr_kerD_square ?genS ?setSU //; last first. by apply: normalS nsH0C_M; rewrite // -(sdprodWY defHU) genS ?setUSS. rewrite -Du (inj_eq (mulfI (neq0CG _))) -(prednK (indexg_gt0 _ _)). rewrite mulrSr addrK eqC_nat addnC mulnDl addnAC (mulnC q) -addnA -mulnDr. move/eqP <-; congr _.-1. have nH0HC: HC \subset 'N(H0) by rewrite join_subG nH0H. rewrite -(index_quotient_eq _ _ nH0HC) ?genS ?setSU //; last first. by rewrite setIC subIset ?joing_subl. rewrite quotientYidl // -(index_sdprod (dprodWsdC defHCbar)). by case: Ptype_Fcore_factor_facts. have /hasP[psi1 S1psi1 _]: has predT S1 by rewrite has_predT. pose gamma := 'Ind[M, H <*> U1] 1; pose alpha := gamma - psi1. pose nm_alpha : algC := a%:R + 1 + (q.-1 * a ^ 2)%:R / u%:R. have [Aalpha Nalpha]: alpha \in 'CF(M, 'A(M)) /\ '[alpha] = nm_alpha. have sHU1_HU: H <*> U1 \subset HU by rewrite -(sdprodWY defHU) genS ?setUS. have sHU1_M := subset_trans sHU1_HU sHUM. have sHU1_A1: H <*> U1 \subset 1%g |: 'A(M). pose pi := \pi(H); rewrite -subDset; apply/subsetP=> y /setD1P[nty HU1y]. apply/bigcupP; rewrite notMtype1 /=; have sHMs := Fcore_sub_FTcore maxM. have defHU1: H ><| U1 = H <*> U1 := sdprod_subr defHU sU1U. have nsH_HU1: H <| H <*> U1 by have [] := sdprod_context defHU1. have [HUy [_ nH_HU1]] := (subsetP sHU1_HU y HU1y, normalP nsH_HU1). have hallH: pi.-Hall(H <*> U1) H. by rewrite Hall_pi // -(coprime_sdprod_Hall_l defHU1) (coprimegS sU1U). have hallU1: pi^'.-Hall(H <*> U1) U1. by rewrite -(compl_pHall _ hallH) sdprod_compl. have [pi'y | pi_y] := boolP (pi^'.-elt y); last first. exists y.`_pi; last by rewrite 3!inE nty HUy cent1C groupX ?cent1id. rewrite !inE (sameP eqP constt1P) pi_y (subsetP sHMs) //. by rewrite (mem_normal_Hall hallH) ?groupX ?p_elt_constt. have solHU1: solvable (H <*> U1) by rewrite (solvableS sHU1_M) ?mmax_sol. have [||z HU1z U1yz] := Hall_Jsub _ hallU1 _ pi'y; rewrite ?cycle_subG //. have /trivgPn[x /setIP[Hx cxyz] ntx]: 'C_H[y ^ z] != 1%g. apply: contraTneq (prime_gt1 p_pr) => regHy; rewrite -oH1 cardG_gt1 negbK. move: U1yz; rewrite -cycleJ subsetI sub_astabQ => /and3P[sYU nHY cH1Y]. rewrite centsC in cH1Y; rewrite -(setIidPl cH1Y) -(setIidPl sH1H) -setIA. rewrite -coprime_quotient_cent ?(coprimegS sYU) // cent_cycle regHy. by rewrite quotient1 setIg1. exists (x ^ z^-1)%g; last by rewrite 3!inE nty HUy cent1J mem_conjgV cent1C. by rewrite 2!inE conjg_eq1 ntx (subsetP sHMs) // -mem_conjg nH_HU1. have{sHU1_A1} Aalpha: alpha \in 'CF(M, 'A(M)). have A'1: 1%g \notin 'A(M) by have /subsetD1P[] := FTsupp_sub M. rewrite -['A(M)](setU1K A'1) cfun_onD1 !cfunE subr_eq0 cfInd1 // cfun11. rewrite mulr1 -(Lagrange_index sHUM) // -(index_sdprod defM) -/q. rewrite -(index_sdprodr defHU) ?subsetIl // -/a eq_sym andbC. have:= S1psi1; rewrite mem_filter /= => /andP[-> _] /=. rewrite rpredB //. apply: cfun_onS (cfInd_on sHU1_M (cfun_onG _)). rewrite class_supportEr; apply/bigcupsP=> w Mw. by rewrite sub_conjg conjUg conjs1g (normsP (FTsupp_norm M)) ?groupV. have /seqIndP[s /setDP[_ ker'H ] ->] := H0C_S1 _ S1psi1. rewrite (prDade_Ind_irr_on (FT_prDade_hypF maxM MtypeP)) //. by rewrite inE in ker'H. have ->: '[alpha] = '[gamma] + 1. have /irrP[t Dt] := irrS1 _ S1psi1. rewrite cfnormBd; first by rewrite Dt cfnorm_irr. have /seqIndP[s /setDP[_ ker'H ] Dpsi1] := H0C_S1 _ S1psi1. apply: contraNeq ker'H; rewrite Dt /gamma -irr0 -irr_consttE => tHU1_0. rewrite inE -(sub_cfker_Ind_irr _ sHUM) ?gFnorm // -Dpsi1 Dt. rewrite -(sub_cfker_constt_Ind_irr tHU1_0) ?gFnorm ?joing_subl //. by rewrite irr0 cfker_cfun1 joing_subl. split=> //; rewrite /nm_alpha addrAC natrM mulrAC mulrC; congr (_ + 1). rewrite -{1}(mulnK a a_gt0) natf_div ?dvdn_mull // -mulrDr mulnn natrX. have /sdprod_isom[nH_UW1 isomMH]: H ><| (U <*> W1) = M. rewrite sdprodEY ?join_subG ?nHU ?(subset_trans sW1M) ?gFnorm //. by rewrite joingA (sdprodWY defHU) (sdprodWY defM). rewrite /= -(setIidPl sHHU) norm_joinEr // setIAC -setIA -group_modl //. by rewrite (setIC W1) tiHUW1 mulg1. have sU1_UW1: U1 \subset U <*> W1 by rewrite subIset ?joing_subl. rewrite /gamma -(cfMod_cfun1 _ H) cfIndMod ?joing_subl //. rewrite cfMod_iso //= quotientYidl ?(subset_trans sU1_UW1) //. rewrite -(restrm_quotientE _ sU1_UW1) -(cfIsom_cfun1 (restr_isom _ isomMH)). rewrite (cfIndIsom isomMH) // {nH_UW1 isomMH}cfIsom_iso. rewrite -(cfIndInd _ (joing_subl U W1)) // cfInd_cfun1 //= -/U1 -/a. rewrite linearZ cfnormZ normr_nat /=; congr (_ * _). have defUW1: U ><| W1 = U <*> W1. by rewrite sdprodEY // -(setIidPl sUHU) -setIA tiHUW1 setIg1. apply: canLR (mulKf (neq0CG _)) _; rewrite -(sdprod_card defUW1) natrM -/q. rewrite mulrAC mulrDr mulrCA -{1}(Lagrange sU1U) /= -/U1 -/a -(Lagrange sCU). rewrite -card_quotient // !natrM !mulfK ?neq0CiG ?neq0CG //. transitivity (\sum_(x in U <*> W1) \sum_(w1 in W1) \sum_(w2 in W1) (x ^ w1 \in U1 :&: U1 :^ w2)%g%:R : algC). - apply: eq_bigr => x _; rewrite (cfIndEsdprod _ _ defUW1) mulr_suml. apply: eq_bigr => w1 W1w1; rewrite rmorph_sum mulr_sumr. rewrite (reindex_inj invg_inj) (eq_bigl _ _ (groupV W1)) /=. rewrite (reindex_acts 'R _ (groupVr W1w1)) ?astabsR //=. apply: eq_bigr => w2 _; rewrite inE !cfuniE // rmorph_nat -natrM mulnb. by congr (_ && _)%:R; rewrite invMg invgK conjgM -mem_conjg. rewrite exchange_big /= mulr_natr -sumr_const; apply: eq_bigr => w1 W1w1. transitivity (\sum_(w in W1) #|U1 :&: U1 :^ w|%:R : algC). rewrite exchange_big /=; apply: eq_bigr => w W1w. rewrite (reindex_acts 'J _ (groupVr W1w1)) ?astabsJ ?normsG ?joing_subr //=. symmetry; rewrite big_mkcond -sumr_const /= big_mkcond /=. apply: eq_bigr => x _; rewrite conjgKV. by case: setIP => [[/(subsetP sU1_UW1)-> //] | _]; rewrite if_same. rewrite (big_setD1 1%g) //= conjsg1 setIid; congr (_ + _). rewrite [q](cardsD1 1%g) group1 /= mulr_natl -sumr_const. by apply: eq_bigr => w W1w; rewrite tiU1. have [gtS4alpha s4gt0]: (size S4)%:R > '[alpha] /\ (size S4 > 0)%N. suffices gtS4alpha: (size S4)%:R > '[alpha]. by split=> //; rewrite -ltC_nat (le_lt_trans (cfnorm_ge0 alpha)). rewrite Nalpha -(@ltr_pM2r _ u%:R) ?ltr0n // mulrDl divfK ?neq0CG //. rewrite -(ltr_pM2l (gt0CG W1)) -/q -mulrSr -!(natrM, natrD) ltC_nat. rewrite mulnA mulnAC -(ltn_add2r (p.-1 * (q + u))) oS4 {1}Dp addn1 -Da_p /=. apply: leq_ltn_trans (_ : q.+2 * a ^ 3 + q ^ 2 * a ^ 2 + 2 * q * a < _)%N. rewrite (addnC q) 2!mulnDr addnA (mulnAC _ a q) leq_add2r. rewrite mulnA addnAC -mulnDl mulnS -addnA -mulnDl addn2 mulnCA -mulnA. rewrite -[q in (_ <= _ + q * _)%N](prednK q_gt0) (mulSn q.-1) addnA. by rewrite leq_add2r mulnA -mulnDl addnC leq_mul. have q_gt2: (2 < q)%N. by rewrite ltn_neqAle prime_gt1 ?(contraTneq _ odd_q) => // <-. apply: leq_trans (_ : a.*2 ^ q + 'C(q, 2) * a.*2 ^ 2 + q * a.*2 <= _)%N. rewrite -mul2n (mulnCA q) (mulnA 2%N) ltn_add2r !expnMn -addSn leq_add //. apply: leq_ltn_trans (_ : q.-1.*2.+1 * a ^ q < _)%N. rewrite leq_mul ?leq_pexp2l //. by rewrite -(subnKC q_gt2) -addnn !addnS !ltnS leq_addl. rewrite ltn_pmul2r ?expn_gt0 ?a_gt0 // -doubleS. by rewrite -(prednK q_gt0) expnS mul2n leq_double ltn_expl. rewrite mulnA leq_pmul2r ?expn_gt0 ?a_gt0 // -(subnKC q_gt2). rewrite mulnCA mulnA addSn -mul_bin_diag bin1 -mulnA leq_pmul2l //. by rewrite mulnS -addSnnS leq_addr. rewrite Dp -Da_p mul2n (addnC a.*2) expnDn -(subnKC q_gt2) !addSn add0n. rewrite 3!big_ord_recl big_ord_recr /= !exp1n /= bin1 binn !mul1n /bump /=. by do 2!rewrite addnC leq_add2l; apply: leq_addl. have{cohS1} [tau1 cohS1] := cohS1; have [[Itau1 Ztau1] Dtau1] := cohS1. have sS30: cfConjC_subset S3 (S_ H0C'). split=> [|chi|chi]; first by rewrite filter_uniq ?seqInd_uniq. by rewrite mem_filter => /andP[]. rewrite !mem_filter /= -!eqS12 => /andP[S1'chi S_chi]. rewrite cfAut_seqInd // (contra _ S1'chi) //. by have [_ _ ccS1] := sS10; move/ccS1; rewrite cfConjCK. have scohS3: subcoherent S3 tau rmR := subset_subcoherent scohS0 sS30. have [tau3 cohS3]: coherent S3 M^# tau. apply: uniform_degree_coherence scohS3 _. apply: all_pred1_constant (q * u)%:R _ _. by rewrite all_map; apply/allP=> chi /S3qu. have [IZtau3 Dtau3] := cohS3; have [Itau3 Ztau3] := IZtau3. have notA1: 1%g \notin 'A(M) by have /subsetD1P[] := FTsupp_sub M. have sS0_1A: {subset S_ H0C' <= 'CF(M, 1%g |: 'A(M))}. move=> _ /seqIndP[s /setDP[_ ker'H] ->]; rewrite inE in ker'H. by rewrite (prDade_Ind_irr_on (FT_prDade_hypF maxM MtypeP)). have sS0A: {subset 'Z[S_ H0C', M^#] <= 'Z[irr M, 'A(M)]}. move=> chi; rewrite (zcharD1_seqInd_Dade _ notA1) //. by apply: zchar_sub_irr; apply: seqInd_vcharW. have Zalpha: alpha \in 'Z[irr M]. rewrite rpredB ?char_vchar ?cfInd_char ?rpred1 //. exact: seqInd_char (H0C_S1 _ S1psi1). have ZAalpha: alpha \in 'Z[irr M, 'A(M)] by rewrite zchar_split Zalpha. have [Itau Ztau]: {in 'Z[irr M, 'A(M)], isometry tau, to 'Z[irr G]}. apply: sub_iso_to (Dade_Zisometry _); last exact: zcharW. by apply: zchar_onS; apply: FTsupp_sub0. have oSgamma: {in S_ H0C', forall lam, '[gamma, lam] = 0}. move=> _ /seqIndP[s /setDP[_ ker'H ] ->]. rewrite ['Ind _]cfun_sum_constt cfdot_sumr big1 // => t sMt. rewrite cfdotZr [gamma]cfun_sum_constt cfdot_suml big1 ?mulr0 // => t0 gMt0. rewrite cfdotZl cfdot_irr (negPf (contraNneq _ ker'H)) ?mulr0 // => Dt0. rewrite inE (sub_cfker_constt_Ind_irr sMt) ?gFnorm // -Dt0. rewrite /gamma -irr0 in gMt0. rewrite -(sub_cfker_constt_Ind_irr gMt0) ?gFnorm ?joing_subl //. by rewrite irr0 cfker_cfun1 joing_subl. by rewrite (subset_trans _ sHUM) // join_subG sHHU subIset ?sUHU. have [/eqP psi1qa Spsi1]: psi1 1%g == (q * a)%:R /\ psi1 \in S_ H0C'. by move: S1psi1; rewrite mem_filter => /andP[]. have o_alpha_S3: orthogonal alpha^\tau (map tau3 S3). rewrite /orthogonal /= andbT all_map. apply: contraFT (lt_geF gtS4alpha) => /allPn[lam0 S3lam0 /= alpha_lam0]. set ca := '[_, _] in alpha_lam0; pose al0 := (-1) ^+ (ca < 0)%R *: alpha. have{alpha_lam0} al0_lam0: '[al0^\tau, tau3 lam0] > 0. have Zca: ca \in Cint by rewrite Cint_cfdot_vchar ?Ztau // Ztau3 ?mem_zchar. by rewrite linearZ cfdotZl (canLR (signrMK _) (CintEsign Zca)) normr_gt0. rewrite -Itau // -(cfnorm_sign (ca < 0)%R) -linearZ /= -/al0. have S4_dIirrK: {in map tau3 S4, cancel (dirr_dIirr id) (@dchi _ _)}. apply: dirr_dIirrPE => _ /mapP[lam S4lam ->]. rewrite mem_filter -andbA negbK in S4lam. have [/irrP[i Dlam] _ S3lam] := and3P S4lam. by rewrite dirrE Itau3 ?Ztau3 ?mem_zchar //= Dlam cfnorm_irr. rewrite -(size_map tau3) -(size_map (dirr_dIirr id)). rewrite -(card_uniqP _); last first. rewrite !map_inj_in_uniq ?filter_uniq ?seqInd_uniq //. apply: sub_in2 (Zisometry_inj Itau3) => lam. by rewrite mem_filter => /andP[_ /mem_zchar->]. exact: can_in_inj S4_dIirrK. apply: le_trans (_ : #|dirr_constt al0^\tau|%:R <= _); last first. have Zal0: al0^\tau \in 'Z[irr G] by rewrite Ztau ?rpredZsign. rewrite cnorm_dconstt // -sumr_const ler_sum // => i al0_i. by rewrite sqr_Cint_ge1 ?gt_eqF -?dirr_consttE // Cint_Cnat ?Cnat_dirr. rewrite leC_nat subset_leq_card //; apply/subsetP=> _ /mapP[nu S4nu ->]. rewrite dirr_consttE S4_dIirrK //; congr (_ > 0): al0_lam0. rewrite {al0}linearZ !cfdotZl /=; congr (_ * _) => {ca}; apply/eqP. have{nu S4nu} [lam S4lam ->] := mapP S4nu. rewrite mem_filter in S4lam; have{S4lam} [_ S3lam] := andP S4lam. have Zdlam: lam0 - lam \in 'Z[S3, M^#]. rewrite zcharD1E rpredB ?mem_zchar //= !cfunE subr_eq0. by have [/eqP->] := (S3qu _ S3lam, S3qu _ S3lam0). rewrite -subr_eq0 -cfdotBr -raddfB Dtau3 //. rewrite Itau // ?sS0A //; last exact: zchar_filter Zdlam. suffices{lam S3lam Zdlam} oS3a: {in S3, forall lam, '[alpha, lam] = 0}. by rewrite cfdotBr subr_eq0 !oS3a. move=> lam; rewrite mem_filter /= -eqS12 => /andP[S1'lam H0C'lam]. by rewrite cfdotBl oSgamma // (seqInd_ortho _ Spsi1) ?(memPn S1'lam) // subr0. have{s4gt0 gtS4alpha} /hasP[lam1 S4lam1 _]: has predT S4 by rewrite has_predT. have [/irrP[l1 Dl1] S3lam1]: lam1 \in irr M /\ lam1 \in S3. by move: S4lam1; rewrite mem_filter -andbA negbK => /and3P[]. have [S1'lam1 Slam1]: lam1 \notin S1 /\ lam1 \in S_ H0C'. by move: S3lam1; rewrite mem_filter eqS12 => /andP[]. have S3lam1s: lam1^*%CF \in S3 by have [[_ _ ->]] := scohS3. have ZS3dlam1: lam1 - lam1^*%CF \in 'Z[S3, M^#]. rewrite zcharD1E rpredB ?mem_zchar //. by have:= seqInd_sub_aut_zchar nsHUM conjC Slam1; rewrite zcharD1 => /andP[]. have ZAdlam1: lam1 - lam1^*%CF \in 'Z[irr M, 'A(M)]. rewrite sS0A // zchar_split rpredB ?mem_zchar ?cfAut_seqInd //. by rewrite (zchar_on ZS3dlam1). pose beta := lam1 - (u %/ a)%:R *: psi1. have ZAbeta: beta \in 'Z[irr M, 'A(M)]. apply: sS0A; rewrite zcharD1E rpredB ?scaler_nat ?rpredMn ?mem_zchar //=. by rewrite !cfunE subr_eq0 psi1qa -natrM mulnCA divnK // S3qu. have [_ _ poSS _ _] := scohS0; have [_ oSS] := pairwise_orthogonalP poSS. have o1S1: orthonormal S1. rewrite orthonormalE filter_pairwise_orthogonal // andbT. by apply/allP=> _ /irrS1/irrP[t ->]; rewrite /= cfnorm_irr. have o1S4: orthonormal S4. rewrite orthonormalE !filter_pairwise_orthogonal // andbT. apply/allP=> nu; rewrite mem_filter /= -andbA negbK. by case/andP=> /irrP[t ->]; rewrite cfnorm_irr. have n1psi1: '[psi1] = 1 by have [_ -> //] := orthonormalP o1S1; rewrite eqxx. have n1lam1: '[lam1] = 1 by have [_ -> //] := orthonormalP o1S4; rewrite eqxx. have oS14tau: orthogonal (map tau1 S1) (map tau3 S4). apply/orthogonalP=> psi _ S1psi /mapP[lam /sS43 S3lam ->]. apply: {psi lam S3lam}orthogonalP S1psi (map_f tau3 S3lam). apply: (coherent_ortho scohS0 sS10 cohS1 sS30 cohS3) => psi /=. by rewrite mem_filter !inE eqS12 => /andP[-> _]. have [Gamma [S4_Gamma normGamma [b Dbeta]]]: exists Gamma, [/\ Gamma \in 'Z[map tau3 S4], '[Gamma] = 1 & exists b : bool, beta^\tau = Gamma - (u %/ a)%:R *: tau1 psi1 + b%:R *: \sum_(psi <- S1) tau1 psi]. - have [G S4G [G' [Dbeta _ oG'4]]] := orthogonal_split (map tau3 S4) beta^\tau. have [B S1B [Delta [dG' _ oD1]]] := orthogonal_split (map tau1 S1) G'. have sZS43: {subset 'Z[S4] <= 'Z[S3]} := zchar_subset sS43. have [Itau34 Ztau34] := sub_iso_to sZS43 sub_refl IZtau3. have Z_G: G \in 'Z[map tau3 S4]. have [_ -> ->] := orthonormal_span (map_orthonormal Itau34 o1S4) S4G. rewrite big_seq rpred_sum // => xi S4xi; rewrite rpredZ_Cint ?mem_zchar //. rewrite -(addrK G' G) -Dbeta cfdotBl (orthoPl oG'4) // subr0. rewrite Cint_cfdot_vchar ?Ztau //. by have{xi S4xi} [xi S4xi ->] := mapP S4xi; rewrite Ztau34 ?mem_zchar. have oD4: orthogonal Delta (map tau3 S4). apply/orthoPl=> xi S4xi; rewrite -(addKr B Delta) addrC -dG' cfdotBl. by rewrite (orthoPl oG'4) // (span_orthogonal oS14tau) ?subrr // memv_span. have [_ -> dB] := orthonormal_span (map_orthonormal Itau1 o1S1) S1B. pose b := (u %/ a)%:R + '[B, tau1 psi1]. have betaS1_B: {in S1, forall psi, '[beta^\tau, tau1 psi] = '[B, tau1 psi]}. move=> psi S1psi; rewrite Dbeta dG' !cfdotDl (orthoPl oD1) ?map_f // addr0. rewrite cfdotC (span_orthogonal oS14tau) ?rmorph0 ?add0r //. by rewrite memv_span ?map_f. have Zb: b \in Cint. rewrite rpredD ?rpred_nat // -betaS1_B // Cint_cfdot_vchar ?Ztau //. by rewrite Ztau1 ?mem_zchar. have{} dB: B = - (u %/ a)%:R *: tau1 psi1 + b *: \sum_(psi <- S1) tau1 psi. rewrite dB big_map !(big_rem _ S1psi1) /= scalerDr addrA -scalerDl addKr. rewrite scaler_sumr; congr (_ + _); apply: eq_big_seq => psi. rewrite mem_rem_uniq ?filter_uniq ?seqInd_uniq // => /andP[/= psi_1' S1psi]. apply/esym/eqP; rewrite -subr_eq0 -scalerBl -addrA -!betaS1_B // -cfdotBr. have [/eqP psi_qa Spsi]: psi 1%g == (q * a)%:R /\ psi \in S_ H0C'. by move: S1psi; rewrite mem_filter => /andP[]. have Z1dpsi: psi1 - psi \in 'Z[S1, M^#]. by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE psi1qa psi_qa subrr. rewrite -raddfB Dtau1 // Itau //; last first. by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi). rewrite cfdotC cfdotBr cfdotZr !cfdotBl 2?oSS ?(memPn S1'lam1) // subrr. by rewrite add0r n1psi1 oSS // subr0 mulr1 rmorphN conjCK subrr scale0r. have Gge1: 1 <= '[G] ?= iff ('[G] == 1). rewrite eq_sym; apply: leif_eq. have N_G: '[G] \in Cnat. apply: Cnat_cfnorm_vchar; apply: zchar_sub_irr Z_G => _ /mapP[nu S4nu ->]. by rewrite Ztau34 ?mem_zchar. rewrite -(truncCK N_G) ler1n lt0n -eqC_nat truncCK {N_G}// cfnorm_eq0. have: '[beta^\tau, (lam1 - lam1^*%CF)^\tau] != 0. rewrite Itau // cfdotBl cfdotZl !cfdotBr n1lam1. rewrite (seqInd_conjC_ortho _ _ _ Slam1) ?mFT_odd // subr0. rewrite !oSS ?cfAut_seqInd -?(inv_eq (@cfConjCK _ _)) ?(memPn S1'lam1) //. by rewrite !(subr0, mulr0) oner_eq0. by have [_ _ ->] := sS10. rewrite Dbeta -Dtau3 //; apply: contraNneq => ->. rewrite add0r raddfB cfdotBr !(orthoPl oG'4) ?map_f ?subr0 //. move: S4lam1; rewrite ![_ \in S4]mem_filter /= !negbK /= cfAut_irr S3lam1s. by case/andP=> /andP[-> /cfAut_seqInd->]. have ubG: '[G] + (b ^+ 2 - b) * (u %/ a).*2%:R + '[Delta] = 1. apply: (addrI ((u %/ a) ^ 2)%:R); transitivity '[beta^\tau]. rewrite -!addrA [LHS]addrCA Dbeta cfnormDd; last first. by rewrite cfdotC (span_orthogonal oG'4) ?rmorph0 // memv_span ?inE. congr (_ + _); rewrite !addrA dG' cfnormDd; last first. by rewrite cfdotC (span_orthogonal oD1) ?rmorph0 // memv_span ?inE. congr (_ + _); rewrite dB scaleNr [- _ + _]addrC cfnormB !cfnormZ. rewrite normr_nat Cint_normK // scaler_sumr cfdotZr rmorph_nat. rewrite cfnorm_map_orthonormal // cfproj_sum_orthonormal //. rewrite Itau1 ?mem_zchar// n1psi1 mulr1 rmorphM/= rmorph_nat conj_Cint //. rewrite -mulr2n oS1ua -muln_divA // mul2n -addrA addrCA -natrX mulrBl. by congr (_ + (_ - _)); rewrite -mulrnAl -mulrnA muln2 mulrC. rewrite Itau // cfnormBd; last first. by rewrite cfdotZr oSS ?mulr0 // (memPnC S1'lam1). by rewrite cfnormZ normr_nat n1psi1 n1lam1 mulr1 addrC -natrX. have ubDelta: '[G] <= '[G] + '[Delta] ?= iff (Delta == 0). rewrite addrC -leifBLR subrr -cfnorm_eq0 eq_sym. by apply: leif_eq; apply: cfnorm_ge0. have{ubG} ubDeltaG: '[G] + '[Delta] <= 1 ?= iff pred2 0 1 b. rewrite -{1}ubG addrAC [_ + _ + _] addrC -leifBLR subrr /=. set n := _%:R; rewrite mulrC -{1}(mulr0 n) mono_leif; last first. by apply: ler_pM2l; rewrite ltr0n double_gt0 divn_gt0 // dvdn_leq. rewrite /= -(subr_eq0 b 1) -mulf_eq0 mulrBr mulr1 eq_sym. apply: leif_eq; rewrite subr_ge0. have [-> | nz_b] := eqVneq b 0; first by rewrite expr2 mul0r. rewrite (le_trans (real_ler_norm _)) ?Creal_Cint // -[`|b|]mulr1. by rewrite -Cint_normK // ler_pM2l ?normr_gt0 // norm_Cint_ge1. have [_ /esym] := leif_trans Gge1 (leif_trans ubDelta ubDeltaG). rewrite eqxx => /and3P[/eqP normG1 /eqP Delta0 /pred2P b01]. exists G; split=> //; exists (b != 0). rewrite Dbeta dG' Delta0 addr0 dB scaleNr addrA; congr (_ + _ *: _). by case: b01 => ->; rewrite ?eqxx ?oner_eq0. have alpha_beta: '[alpha^\tau, beta^\tau] = (u %/ a)%:R. rewrite Itau // cfdotBr cfdotZr rmorph_nat !cfdotBl !oSgamma // !sub0r. by rewrite n1psi1 mulrN opprK mulr1 addrC oSS ?subr0 // (memPn S1'lam1). have [X S1X [Delta [Dalpha _ oD1]]]:= orthogonal_split (map tau1 S1) alpha^\tau. pose x := 1 + '[X, tau1 psi1]. have alphaS1_X: {in S1, forall psi, '[alpha^\tau, tau1 psi] = '[X, tau1 psi]}. by move=> psi S1psi; rewrite Dalpha cfdotDl (orthoPl oD1) ?map_f // addr0. have Zx: x \in Cint. rewrite rpredD ?rpred1 // -alphaS1_X // Cint_cfdot_vchar ?Ztau //. by rewrite Ztau1 ?mem_zchar. have{alphaS1_X S1X} defX: X = x *: (\sum_(psi <- S1) tau1 psi) - tau1 psi1. have [_ -> ->] := orthonormal_span (map_orthonormal Itau1 o1S1) S1X. rewrite addrC -scaleN1r big_map !(big_rem _ S1psi1) /= scalerDr addrA. rewrite -scalerDl addKr scaler_sumr; congr (_ + _); apply: eq_big_seq => psi. rewrite mem_rem_uniq ?filter_uniq ?seqInd_uniq // => /andP[/= psi_1' S1psi]. apply/esym/eqP; rewrite -subr_eq0 -scalerBl -addrA -!alphaS1_X // -cfdotBr. have [/eqP psi_qa Spsi]: psi 1%g == (q * a)%:R /\ psi \in S_ H0C'. by move: S1psi; rewrite mem_filter => /andP[]. have Z1dpsi: psi1 - psi \in 'Z[S1, M^#]. by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE psi1qa psi_qa subrr. rewrite -raddfB Dtau1 // Itau //; last first. by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi). rewrite cfdotBr !cfdotBl !oSgamma // n1psi1 cfdotC oSS // rmorph0. by rewrite !subr0 add0r subrr scale0r. have{x Zx X defX Delta Dalpha oD1} b_mod_ua: (b == 0 %[mod u %/ a])%C. rewrite -oppr0 -eqCmodN (eqCmod_trans _ (eqCmodm0 _)) // {2}nCdivE. rewrite -alpha_beta Dbeta -addrA cfdotDr. rewrite (span_orthogonal o_alpha_S3) ?add0r; first 1 last. - by rewrite memv_span ?inE. - apply: subvP (zchar_span S4_Gamma); apply: sub_span; apply: mem_subseq. by rewrite map_subseq ?filter_subseq. rewrite Dalpha addrC cfdotDl (span_orthogonal oD1); first 1 last. - by rewrite memv_span ?inE. - rewrite addrC rpredB ?rpredZ //; last by rewrite memv_span ?map_f. by rewrite big_seq rpred_sum // => psi S1psi; rewrite memv_span ?map_f. rewrite add0r addrC defX cfdotBr cfdotBl cfdotZl cfdotZr !scaler_sumr. rewrite cfdotZr !rmorph_nat cfdotBl Itau1 ?mem_zchar // n1psi1. rewrite cfnorm_map_orthonormal // cfdotC !cfproj_sum_orthonormal //. rewrite rmorph_nat oS1ua -muln_divA // natrM !mulrA addrC mulrC addrA. rewrite -mulNr -mulrDl eqCmod_sym eqCmod_addl_mul // addrC !rpredB ?rpred1 //. by rewrite !rpredM ?rpred_nat. have{b_mod_ua alpha_beta} b0: b = 0%N :> nat. have:= b_mod_ua; rewrite /eqCmod subr0 dvdC_nat => /eqnP. rewrite modn_small // (leq_ltn_trans (leq_b1 b)) // ltn_divRL // mul1n. by rewrite ltn_neqAle -(eqn_pmul2l q_gt0) eq_sym ne_qa_qu dvdn_leq. exists lam1 => //; suffices: coherent (lam1 :: lam1^* :: S1)%CF M^# tau. by apply: subset_coherent => phi; rewrite !inE eqS12. move: Dbeta; rewrite b0 scale0r addr0. apply: (extend_coherent_with scohS0 sS10 cohS1); first by []. rewrite rpred_nat psi1qa -natrM mulnCA (eqP (S3qu _ S3lam1)) divnK //. rewrite cfdotC (span_orthogonal oS14tau) ?(zchar_span S4_Gamma) ?conjC0 //. by rewrite rpredZ ?memv_span ?map_f. Qed.
imports: HB(structures) 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 cyclic commutator center gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection8)