proposition: Lemma typeP_nonGalois_characters (not_Galois : ~~ typeP_Galois) : let a := #|U : 'C_U(sval (typeP_Galois_Pn not_Galois) | 'Q)| in [/\ {in X_ H0, forall s, (a %| 'chi_s 1%g)%C}, size mu_ = p.-1 /\ {in mu_, forall mu_j, isIndHC mu_j}, exists t, isIndHC 'chi_t & let irr_qa := [pred zeta in irr M | zeta 1%g == (q * a)%:R] in let lb_n := (p.-1 * #|U|)%N in let lb_d := (a ^ 2 * #|U'|)%N in (lb_d %| lb_n /\ lb_n %/ lb_d <= count irr_qa (S_ H0U'))%N].
proof: Proof. case: (typeP_Galois_Pn _) => H1 [oH1 nH1U nH1Uq defHbar aP]; rewrite [sval _]/=. move=> a; case: aP; rewrite -/a => a_gt1 a_dv_p1 cycUb1 isoUb. set part_a := ({in _, _}); pose HCbar := (HC / H0)%G. have [_ /mulG_sub[sHUM sW1M] nHUW1 tiHUW1] := sdprodP defM. have [nsHHU _ /mulG_sub[sHHU sUHU] nHU tiHU] := sdprod_context defHU. have [nH0H nHHU] := (normal_norm nsH0H, normal_norm nsHHU). have sHHC: H \subset HC by rewrite joing_subl. have [nH0HU sCHU] := (subset_trans sHUM nH0M, subset_trans sCU sUHU). have nsH0_HU: H0 <| HU by rewrite /normal (subset_trans sH0H). have nH0C := subset_trans sCHU nH0HU. have [nsH0C_M nsHC_M nsH0U'_M _] := nsH0xx_M; have [sHC_M _] := andP nsHC_M. have nsH0HC: H0 <| HC := normalS (subset_trans sH0H sHHC) sHC_M nsH0M. have defHCbar: Hbar \x (C / H0) = HCbar. rewrite /= quotientY // [C]unlock /= astabQ quotient_setIpre. by rewrite dprodEY ?subsetIr // setIA -quotientGI // tiHU quotient1 setI1g. have sHC_HU: HC \subset HU by rewrite join_subG sHHU. have nsHC_HU: HC <| HU := normalS sHC_HU sHUM nsHC_M. 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 nH1H] := andP nsH1H. have nHW1: W1 \subset 'N(H) := subset_trans sW1M (gFnorm _ _). have nHbW1: W1bar \subset 'N(Hbar) by rewrite quotient_norms. have sH1wH w: w \in W1bar -> H1 :^ w \subset Hbar. by move/(normsP nHbW1) <-; rewrite conjSg. have nsH1wHUb w: w \in W1bar -> H1 :^ w <| HU / H0. move=> W1w; rewrite -(normsP (quotient_norms _ nHUW1) w W1w) normalJ. rewrite /normal (subset_trans sH1H) ?quotientS //. by rewrite -defHU sdprodE // quotientMl // mulG_subG nH1H. have nH1wHUb := normal_norm (nsH1wHUb _ _). have Part_a: part_a. move=> s; rewrite !inE => /andP[kers'H kersH0]. have [t sHt] := constt_cfRes_irr H s; pose theta := ('chi_t / H0)%CF. have{kers'H} t_neq0: t != 0. by rewrite -subGcfker (sub_cfker_constt_Res_irr sHt). have{kersH0} kertH0: H0 \subset cfker 'chi_t. by rewrite (sub_cfker_constt_Res_irr sHt). have Ltheta: theta \is a linear_char. by rewrite /theta -quo_IirrE // (char_abelianP _ _). have Dtheta : _ = theta := cfBigdprod_Res_lin defHbar Ltheta. set T := 'I_HU['chi_t]; have sHT: H \subset T by rewrite sub_Inertia. have sTHU: T \subset HU by rewrite Inertia_sub. suffices{s sHt} a_dv_iTHU: a %| #|HU : T|. have [_ defInd_t _ imInd_t _] := cfInd_sum_Inertia t nsHHU. have /imsetP[r tTr ->]: s \in Ind_Iirr HU @: irr_constt ('Ind[T] 'chi_t). by rewrite imInd_t constt_Ind_Res. by rewrite defInd_t ?cfInd1 // dvdC_mulr ?dvdC_nat // Cint_Cnat ?Cnat_irr1. have /exists_inP[w W1w nt_t_w]: [exists w in W1bar, 'Res[H1 :^ w] theta != 1]. rewrite -negb_forall_in; apply: contra t_neq0 => /forall_inP=> tH1w1. rewrite -irr_eq1 -(cfQuoK nsH0H kertH0) -/theta -Dtheta. rewrite [cfBigdprod _ _]big1 ?rmorph1 // => w /tH1w1/eqP->. by rewrite /cfBigdprodi rmorph1. have defT: H ><| (U :&: T) = T. by rewrite (sdprod_modl defHU) // (setIidPr sTHU). have /irrP[k Dk]: 'Res theta \in irr (H1 :^ w). by rewrite lin_char_irr ?cfRes_lin_char. rewrite -divgS // -(sdprod_card defHU) -(sdprod_card defT) divnMl // divgI. rewrite -indexgI; have ->: a = #|U : 'C_U(H1 :^ w | 'Q)|. have [w1 nH0w1 W1w1 ->] := morphimP W1w; rewrite astabQ centJ morphpreJ //. by rewrite -astabQ indexgI -(normsP nUW1 _ W1w1) indexJg -indexgI. rewrite indexgS ?setIS // sub_astabQ ?(subset_trans sTHU) //= -inertia_quo //. apply: subset_trans (sub_inertia_Res _ (nH1wHUb w W1w)) _. by rewrite Dk (inertia_irr_prime _ p_pr) ?subsetIr ?cardJg // -irr_eq1 -Dk. pose isoJ := conj_isom H1; pose cfJ w i := 'chi_(isom_Iirr (isoJ w) i). pose thetaH (f : {ffun _}) := cfBigdprod defHbar (fun w => cfJ w (f w)). pose theta f := cfDprodl defHCbar (thetaH f). have abH1: abelian H1 by rewrite cyclic_abelian ?prime_cyclic ?oH1. have linH1 i: 'chi[H1]_i \is a linear_char by apply/char_abelianP. have lin_thetaH f: thetaH f \is a linear_char. by apply: cfBigdprod_lin_char => w _; rewrite /cfJ isom_IirrE cfIsom_lin_char. have nz_thetaH f: thetaH f 1%g != 0 by rewrite lin_char_neq0. have Dtheta f: {in W1bar & H1, forall w xb, theta f (xb ^ w) = 'chi_(f w) xb}. move=> w xb W1w H1xb /=; have sHHCb := quotientS H0 sHHC. transitivity ('Res[H1 :^ w] ('Res[Hbar] (theta f)) (xb ^ w)); last first. by rewrite cfDprodlK cfBigdprodKabelian // isom_IirrE cfIsomE. by rewrite cfResRes ?sH1wH // cfResE ?memJ_conjg ?(subset_trans (sH1wH w _)). have lin_theta f: theta f \is a linear_char by rewrite cfDprodl_lin_char. pose Ftheta := pffun_on (0 : Iirr H1) W1bar (predC1 0). have inj_theta: {in Ftheta &, injective theta}. move=> f1 f2 /pffun_onP[/supportP W1f1 _] /pffun_onP[/supportP W1f2 _] eq_f12. apply/ffunP=> w. have [W1w | W1'w] := boolP (w \in W1bar); last by rewrite W1f1 ?W1f2. by apply/irr_inj/cfun_inP=> x H1x; rewrite -!Dtheta ?eq_f12. have irr_thetaH0 f: (theta f %% H0)%CF \in irr HC. by rewrite cfMod_irr ?lin_char_irr. have def_Itheta f: f \in Ftheta -> 'I_HU[theta f %% H0]%CF = HC. case/pffun_onP=> _ nz_fW1; apply/eqP; rewrite eqEsubset sub_Inertia //. rewrite inertia_mod_pre //= -{1}(sdprodW defHU) -group_modl; last first. rewrite (subset_trans sHHC) // -sub_quotient_pre ?normal_norm //. by rewrite sub_Inertia ?quotientS. rewrite -gen_subG genM_join genS ?setUS //= {2}[C]unlock setIS //= astabQ. rewrite morphpreS // centsC -{1}(bigdprodWY defHbar) gen_subG. apply/bigcupsP=> w W1w; rewrite centsC. apply: subset_trans (sub_inertia_Res _ (quotient_norms _ nHHU)) _. rewrite cfDprodlK inertia_bigdprod_irr // subIset // orbC (bigcap_min w) //. rewrite (inertia_irr_prime _ p_pr) ?cardJg ?subsetIr // isom_Iirr_eq0. by apply: nz_fW1; apply: image_f. have irrXtheta f: f \in Ftheta -> 'Ind (theta f %% H0)%CF \in irr HU. move/def_Itheta; rewrite -(cfIirrE (irr_thetaH0 f)) => I_f_HC. by rewrite inertia_Ind_irr ?I_f_HC //. pose Mtheta := [set cfIirr (theta f %% H0)%CF | f in Ftheta]. pose Xtheta := [set cfIirr ('Ind[HU] 'chi_t) | t in Mtheta]. have oXtheta: (u * #|Xtheta| = p.-1 ^ q)%N. transitivity #|Ftheta|; last first. rewrite card_pffun_on cardC1 card_Iirr_abelian // oH1. rewrite -(card_isog (quotient_isog _ _)) ?oW1 ?(subset_trans sW1M) //. by apply/trivgP; rewrite -tiHUW1 setSI ?(subset_trans sH0H). rewrite Du -card_imset_Ind_irr ?card_in_imset //. - move=> f1 f2 Df1 Df2 /(congr1 (tnth (irr HC))); rewrite !{1}cfIirrE //. by move/(can_inj (cfModK nsH0HC)); apply: inj_theta. - by move=> _ /imsetP[f Df ->]; rewrite cfIirrE ?irrXtheta. move=> _ y /imsetP[f /familyP Ff ->] HUy; apply/imsetP. pose yb := inMb y; have HUyb: yb \in (HU / H0)%g by apply: mem_quotient. have nHb_y: inMb y \in 'N(Hbar) by rewrite (subsetP (quotient_norms _ nHHU)). have nH1b_y := subsetP (nH1wHUb _ _) yb HUyb. exists [ffun w => conjg_Iirr (f w) (inMb y ^ w^-1)]. apply/familyP=> w; rewrite ffunE. by case: ifP (Ff w) => _; rewrite !inE conjg_Iirr_eq0. apply: irr_inj; rewrite !(cfIirrE, conjg_IirrE) // (cfConjgMod _ nsHC_HU) //. rewrite cfConjgDprodl //; first congr (cfDprodl _ _ %% H0)%CF; last first. rewrite /= -quotientYidl // (subsetP _ _ HUyb) ?quotient_norms //. by rewrite (subset_trans sHUM) ?normal_norm. rewrite cfConjgBigdprod //; apply: eq_bigr => w W1w; congr (cfBigdprodi _ _). rewrite ffunE /cfJ !isom_IirrE conjg_IirrE. apply/cfun_inP=> _ /imsetP[x Hx ->]; rewrite cfIsomE // cfConjgE ?nH1b_y //. rewrite -conjgM conjgCV conjVg conjgM cfIsomE //; last first. by rewrite -mem_conjg (normP _) // -mem_conjg -normJ ?nH1b_y. by rewrite cfConjgE // -mem_conjg -normJ ?nH1b_y. have sXthXH0C: Xtheta \subset X_ H0C. apply/subsetP=> _ /imsetP[t Mt ->]; have{Mt} [f Ff Dt] := imsetP Mt. rewrite !inE cfIirrE; last by rewrite Dt cfIirrE ?irrXtheta. rewrite !sub_cfker_Ind_irr ?(subset_trans sHUM) ?normal_norm ?gFnormal //. rewrite {t}Dt cfIirrE // join_subG andbCA {1}cfker_mod //. rewrite !{1}sub_cfker_mod //= andbC {1}cfker_sdprod /=. apply: contraL (familyP Ff 1%g) => kerHb; rewrite group1 negbK. have:= sub_cfker_Res (subxx _) kerHb; rewrite cfDprodlK. move/(subset_trans (sH1wH _ (group1 _)))/(sub_cfker_Res (subxx _)). rewrite cfBigdprodKabelian // isom_IirrE cfker_isom morphim_conj /=. by rewrite !conjsg1 subsetIidl subGcfker. pose mu_f (i : Iirr H1) := [ffun w => if w \in W1bar then i else 0]. have Fmu_f (i : Iirr H1): i != 0 -> mu_f i \in Ftheta. by move=> nz_i; apply/familyP=> w; rewrite ffunE; case: ifP; rewrite !inE. pose mk_mu i := 'Ind[HU] (theta (mu_f i) %% H0)%CF. have sW1_Imu i: W1 \subset 'I[theta (mu_f i) %% H0]%CF. apply/subsetP=> w W1w; have Mw := subsetP sW1M w W1w. have nHC_W1 := subset_trans sW1M (normal_norm nsHC_M). rewrite inE (subsetP nHC_W1) ?(cfConjgMod _ nsHC_M) //; apply/eqP. have W1wb: inMb w \in W1bar by rewrite mem_quotient. rewrite cfConjgDprodl ?(subsetP _ _ W1wb) ?quotient_norms //; last first. by rewrite (subset_trans (joing_subr U W1)) ?normal_norm. congr (cfDprodl _ _ %% H0)%CF. apply/cfun_inP=> _ /(mem_bigdprod defHbar)[x [H1x -> _]]. have Hx w1: w1 \in W1bar -> x w1 \in Hbar. by move=> W1w1; rewrite (subsetP (sH1wH w1 _)) ?H1x. rewrite !lin_char_prod ?cfConjg_lin_char //; apply/eq_bigr=> w1 W1w1. rewrite cfConjgE ?(subsetP nHbW1) //. have W1w1w: (w1 * (inMb w)^-1)%g \in W1bar by rewrite !in_group. rewrite -(cfResE _ (sH1wH _ W1w1w)) -?mem_conjg -?conjsgM ?mulgKV ?H1x //. rewrite -(cfResE _ (sH1wH _ W1w1)) ?H1x ?cfBigdprodKabelian //. rewrite !ffunE W1w1 W1w1w -[x w1](conjgKV w1) -(conjgM _ w1) !isom_IirrE. by rewrite !cfIsomE -?mem_conjg ?H1x. have inj_mu: {in predC1 0 &, injective (fun i => cfIirr (mk_mu i))}. move=> i1 i2 nz_i1 nz_i2 /(congr1 (tnth (irr HU))). rewrite !{1}cfIirrE ?irrXtheta ?Fmu_f // /mk_mu. do 2![move/esym; rewrite -{1}(cfIirrE (irr_thetaH0 _))]. move/(cfclass_Ind_irrP _ _ nsHC_HU); rewrite !{1}cfIirrE //. case/cfclassP=> _ /(mem_sdprod defHU)[x [y [Hx Uy -> _]]]. rewrite (cfConjgM _ nsHC_HU) ?(subsetP sHHU x) ?(subsetP sUHU) //. rewrite {x Hx}(cfConjg_id _ (subsetP sHHC x Hx)) => Dth1. suffices /setIP[_ /inertiaJ]: y \in 'I_HU[theta (mu_f i2) %% H0]%CF. rewrite -Dth1 => /(can_inj (cfModK nsH0HC))/inj_theta/ffunP/(_ 1%g). by rewrite !ffunE group1 => -> //; apply: Fmu_f. rewrite def_Itheta ?Fmu_f //= (subsetP (joing_subr _ _)) //. have nCy: y \in 'N(C). by rewrite (subsetP (normal_norm nsCUW1)) ?mem_gen ?inE ?Uy. have [_ _ /trivgPn[wb W1wb ntwb] _ _] := Frobenius_context frobUW1c. have /morphimP[w nCw W1w Dw] := W1wb; have Mw := subsetP sW1M w W1w. rewrite coset_idr //; apply/set1P; rewrite -set1gE; apply: wlog_neg => nty. rewrite -((Frobenius_reg_ker frobUW1c) wb); last by rewrite !inE ntwb. rewrite inE mem_quotient //=; apply/cent1P/commgP. rewrite Dw -morphR //= coset_id //. suffices: [~ y, w] \in U :&: HC. rewrite /= norm_joinEr ?(subset_trans sCU) // -group_modr ?subsetIl //=. by rewrite setIC tiHU mul1g. have Uyw: [~ y, w] \in U; last rewrite inE Uyw. by rewrite {1}commgEl groupMl ?groupV // memJ_norm ?(subsetP nUW1) // Uy. rewrite -(def_Itheta _ (Fmu_f _ nz_i1)) 2!inE /= andbA -in_setI. rewrite (setIidPl (normal_norm nsHC_HU)) (subsetP sUHU) //=. rewrite Dth1 -(cfConjgM _ nsHC_HU) ?(subsetP sUHU) //. have My: y \in M := subsetP (subset_trans sUHU sHUM) y Uy. rewrite mulKVg (cfConjgM _ nsHC_M) ?in_group //. have /inertiaJ-> := subsetP (sW1_Imu i2) _ (groupVr W1w). rewrite (cfConjgM _ nsHC_M) // -Dth1. by have /inertiaJ-> := subsetP (sW1_Imu i1) w W1w. pose Xmu := [set cfIirr (mk_mu i) | i in predC1 0]. have def_IXmu: {in Xmu, forall s, 'I_M['chi_s] = M}. move=> _ /imsetP[i nz_i ->]; apply/setIidPl. rewrite -subsetIidl -{1}(sdprodW defM) mulG_subG sub_Inertia //. rewrite !cfIirrE ?irrXtheta ?Fmu_f //=. apply: subset_trans (sub_inertia_Ind _ (der_norm 1 M)). by rewrite subsetI sW1M /=. pose Smu := [seq 'Ind[M] 'chi_s | s in Xmu]. have sSmu_mu: {subset Smu <= mu_}. move=> _ /imageP[s Xmu_s ->]; rewrite mem_filter /=. rewrite irrEchar cfnorm_Ind_irr ?gFnormal // def_IXmu //. rewrite -(index_sdprod defM) (eqC_nat _ 1) gtn_eqF ?prime_gt1 // andbF. rewrite mem_seqInd ?gFnormal /normal ?(subset_trans sH0H) ?gFsub //=. suffices /(subsetP sXthXH0C): s \in Xtheta. by apply: subsetP; rewrite setSD // Iirr_kerS ?joing_subl. have /imsetP[i nz_i ->] := Xmu_s; rewrite /Xtheta -imset_comp. by apply/imsetP; exists (mu_f i); rewrite /= ?cfIirrE ?Fmu_f. have ResIndXmu: {in Xmu, forall s, 'Res ('Ind[M] 'chi_s) = q%:R *: 'chi_s}. move=> s /def_IXmu Imu_s; rewrite cfResInd_sum_cfclass ?gFnormal ?Imu_s //. by rewrite -(index_sdprod defM) -Imu_s cfclass_inertia big_seq1. have uSmu: uniq Smu. apply/dinjectiveP=> s1 s2 Xs1 Xs2 /(congr1 'Res[HU]); rewrite !ResIndXmu //. by move/(can_inj (scalerK (neq0CG W1)))/irr_inj. have sz_Smu: size Smu = p.-1. by rewrite size_map -cardE card_in_imset // cardC1 card_Iirr_abelian ?oH1. have [sz_mu s_mu_H0C] := nb_redM_H0. have Dmu: Smu =i mu_. by have [|//] := uniq_min_size uSmu sSmu_mu; rewrite sz_mu sz_Smu. split=> {Part_a part_a}//. - split=> // phi mu_phi; have S_HOC_phi := s_mu_H0C _ mu_phi. move: mu_phi; rewrite -Dmu => /imageP[_ /imsetP[i nz_i ->]]. rewrite cfIirrE ?irrXtheta ?Fmu_f // => Dphi. split=> //; rewrite Dphi ?cfInd1 ?cfIndInd //. rewrite -(index_sdprod defM) -/q -Du mulrA -natrM. by rewrite lin_char1 1?cfMod_lin_char ?mulr1. by exists (theta (mu_f i) %% H0)%CF; rewrite 1?cfMod_lin_char. - have /eqVproper: Xmu \subset Xtheta. apply/subsetP=> _ /imsetP[i nz_i ->]; rewrite -[Xtheta]imset_comp /=. by apply/imsetP; exists (mu_f i); rewrite /= ?cfIirrE ?Fmu_f. case=> [defXmu | /andP[_ /subsetPn[s theta_s Xmu'_s]]]; last first. have [_ /imsetP[f Dth_f ->] Ds] := imsetP theta_s; rewrite cfIirrE // in Ds. have /irrP[t Dt]: 'Ind 'chi_s \in irr M; last 1 [exists t; rewrite -{t}Dt]. apply: contraR Xmu'_s => red_Ind_s. have: 'Ind 'chi_s \in mu_. rewrite mem_filter /= red_Ind_s mem_seqInd ?gFnormal //=. apply: subsetP theta_s; rewrite (subset_trans sXthXH0C) ?setSD //. by rewrite Iirr_kerS ?joing_subl. rewrite -Dmu => /imageP[s1 Xmu_s1] /(congr1 (cfdot ('Ind 'chi_s1)))/eqP. rewrite cfnorm_Ind_irr ?gFnormal // eq_sym -cfdot_Res_l. rewrite ResIndXmu // cfdotZl cfdot_irr -natrM mulnC. by case: (s1 =P s) => [<- // | _] /idPn[]; apply: neq0CiG. split; first 2 [by rewrite mem_seqInd ?gFnormal ?(subsetP sXthXH0C)]. rewrite Ds cfIirrE ?irrXtheta ?cfInd1 // -Du -(index_sdprod defM) -/q. by rewrite mulrA -natrM lin_char1 ?cfMod_lin_char ?mulr1. exists (theta f %% H0)%CF; first by rewrite cfMod_lin_char. by rewrite Ds cfIirrE ?irrXtheta //= cfIndInd. suffices /(congr1 odd): u = (p.-1 ^ q.-1)%N. rewrite oddX -(subnKC (prime_gt1 pr_q)) /= -subn1 oddB ?prime_gt0 //. by rewrite -oH1 (oddSg sH1H) ?quotient_odd // mFT_odd. have p1_gt0: (0 < p.-1)%N by rewrite -(subnKC (prime_gt1 p_pr)). apply/eqP; rewrite -(eqn_pmul2r p1_gt0) -expnSr prednK ?prime_gt0 //. by rewrite -oXtheta -defXmu card_in_imset // cardC1 card_Iirr_abelian ?oH1. clear Xmu def_IXmu Smu sSmu_mu ResIndXmu uSmu sz_Smu sz_mu s_mu_H0C Dmu. clear Mtheta Xtheta irrXtheta oXtheta sXthXH0C mu_f Fmu_f mk_mu sW1_Imu inj_mu. clear nz_thetaH lin_thetaH lin_theta Ftheta inj_theta irr_thetaH0 def_Itheta. clear theta Dtheta => irr_qa lb_n lb_d. have sU'U: U' \subset U := der_sub 1 U. have nH0U := subset_trans sUHU nH0HU; have nH0U' := subset_trans sU'U nH0U. have sU'CH1: U' \subset 'C_U(H1 | 'Q). by rewrite subsetI sU'U sub_astabQ nH0U' (centsS sH1H) ?quotient_cents. have sCH1_U: 'C_U(H1 | 'Q) \subset U := subsetIl U _. have dvd_lb: lb_d %| lb_n. rewrite -[lb_d]mulnA dvdn_mul // -(Lagrange sCH1_U). by rewrite mulnC dvdn_pmul2r ?cardSg ?indexg_gt0. split; rewrite ?leq_divLR // /lb_n -(Lagrange sCH1_U) -/a -(Lagrange sU'CH1). rewrite mulnCA -mulnA mulnC !mulnA !leq_pmul2r ?cardG_gt0 ?indexg_gt0 // mulnC. pose H1CH1 := (H1 <*> 'C_(U / H0)(H1))%G; pose HCH1 := (H <*> 'C_U(H1 | 'Q))%G. have defH1CH1: H1 \x 'C_(U / H0)(H1) = H1CH1. rewrite dprodEY ?subsetIr ?coprime_TIg ?(coprimeSg sH1H) //. by rewrite (coprimegS (subsetIl _ _)) ?coprime_morph. have sHCH1_HU: HCH1 \subset HU by rewrite join_subG sHHU (subset_trans sCH1_U). have nsHCH1_HU: HCH1 <| HU. rewrite /normal sHCH1_HU -(sdprodW defHU) mulG_subG normsG ?joing_subl //=. by rewrite normsY // sub_der1_norm. have nsH0_HCH1: H0 <| HCH1. by rewrite (normalS _ sHCH1_HU) // (subset_trans sH0H) ?joing_subl. have nsH1cHU: H1c <| HU / H0. rewrite -(bigdprodWY defH1c) /normal gen_subG norms_gen ?andbT //. by apply/bigcupsP=> w /setD1P[_ /nsH1wHUb/andP[]]. by apply/norms_bigcup/bigcapsP=> w /setD1P[_ /nH1wHUb]. have defHCH1: H1c ><| H1CH1 = (HCH1 / H0)%G. have /sdprodP[_ /mulG_sub[sH1cH _] nH1cH1 tiH1cH1] := dprodWsdC defHb1. rewrite sdprodE /= -(dprodW defH1CH1). - rewrite mulgA (dprodWC defHb1) -morphim_setIpre -astabQ -quotientMl //. by rewrite norm_joinEr // (subset_trans sCH1_U). - rewrite mul_subG ?subIset // (subset_trans (quotientS _ sUHU)) //. exact: normal_norm nsH1cHU. rewrite -(setIidPl sH1cH) setIAC -setIA -group_modl // coprime_TIg ?mulg1 //. by rewrite coprime_sym (coprimegS (subsetIl _ _)) ?coprime_morph. have [nsH1cHCH1 sH1CH1_HCH1 _ nH1cH1C _] := sdprod_context defHCH1. pose Clam := ('C_(U / H0)(H1) / (U' / H0))%G. pose lam (j : Iirr Clam) := 'chi_(mod_Iirr j). pose theta i j := cfSdprod defHCH1 (cfDprod defH1CH1 'chi_i (lam j)). have nsU'CH1: U' <| 'C_U(H1 | 'Q) by rewrite (normalS _ sCH1_U) ?gFnormal. have nsU'CH1b: U' / H0 <| 'C_(U / H0)(H1). by rewrite -morphim_setIpre -astabQ quotient_normal. have abClam: abelian Clam. by rewrite sub_der1_abelian //= quotient_der ?dergS ?subsetIl. have lam_lin j: lam j \is a linear_char. by rewrite /lam mod_IirrE ?cfMod_lin_char //; apply/char_abelianP. have theta_lin i j: theta i j \is a linear_char. by rewrite cfSdprod_lin_char ?cfDprod_lin_char. have <-: #|Clam| = #|'C_U(H1 | 'Q) : U'|. rewrite -card_quotient ?normal_norm //= /= -morphim_setIpre -astabQ. have nsU'U : U' <| U by apply: der_normal. rewrite -(restrmEsub _ _ sCH1_U) -(restrm_quotientE _ sU'U) -morphim_quotm. rewrite card_injm ?quotientS ?injm_quotm ?(isom_inj (quotient_isom _ _)) //. by rewrite coprime_TIg ?(coprimeSg sH0H). pose Mtheta := [set mod_Iirr (cfIirr (theta i j)) | i in [set~ 0], j in setT]. have ->: (p.-1 * #|Clam|)%N = #|Mtheta|. rewrite [Mtheta]curry_imset2X card_imset ?cardsX => [|[i1 j1] [i2 j2] /=/eqP]. by rewrite cardsC1 cardsT !card_Iirr_abelian ?(abelianS sH1H) ?oH1. rewrite (can_eq (mod_IirrK _)) // -(inj_eq irr_inj) !cfIirrE ?lin_char_irr //. rewrite (can_eq (cfSdprodK _)) -!dprod_IirrE (inj_eq irr_inj). by rewrite (can_eq (dprod_IirrK _)) => /eqP[->] /(can_inj (mod_IirrK _))->. have{lam_lin} thetaH1 i j: 'Res[H1] (theta i j) = 'chi_i. rewrite -(cfResRes _ _ sH1CH1_HCH1) ?joing_subl // cfSdprodK cfDprodKl //. exact: lin_char1. have Itheta r: r \in Mtheta -> 'I_HU['chi_r]%CF = HCH1. case/imset2P=> i j; rewrite /= in_setC1 => nz_i _ Dr; apply/eqP. rewrite eqEsubset sub_Inertia //= Dr mod_IirrE // cfIirrE ?lin_char_irr //. rewrite andbT -(quotientSGK _ (normal_sub nsH0_HCH1)) ?subIset ?nH0HU //. rewrite inertia_mod_quo //. apply: subset_trans (sub_inertia_Res _ (nH1wHUb _ (group1 _))) _. rewrite /= conjsg1 thetaH1 (inertia_irr_prime _ p_pr) //. rewrite -quotient_setIpre -astabQ quotientS // -{1}(sdprodW defHU). by rewrite -genM_join sub_gen // group_modl // sub_astabQ nH0H (centsS sH1H). have irr_Xtheta: {in Mtheta, forall r, 'Ind[HU] 'chi_r \in irr HU}. by move=> r Mr; rewrite /= inertia_Ind_irr ?Itheta. pose Xtheta := [set cfIirr ('Ind[HU] 'chi_r) | r in Mtheta]. have Da: a = #|HU : HCH1| by rewrite -(index_sdprodr defHU). have Xtheta_1: {in Xtheta, forall s, 'chi_s 1%g = a%:R}. move=> _ /imsetP[r Mr ->]; have /imset2P[i j _ _ Dr] := Mr. rewrite cfIirrE ?irr_Xtheta ?cfInd1 //= -Da lin_char1 ?mulr1 //. by rewrite Dr mod_IirrE ?cfMod_lin_char // cfIirrE ?lin_char_irr. have nsH0U'HU: H0U' <| HU. by apply: normalS nsH0U'_M; rewrite // -(sdprodWY defHU) genS ?setUSS. have sXthetaXH0U': Xtheta \subset X_ H0U'. apply/subsetP=> _ /imsetP[r Mr ->]; have [i j nz_i _ Dr] := imset2P Mr. rewrite !inE cfIirrE ?irr_Xtheta ?sub_cfker_Ind_irr //= ?normal_norm //. rewrite Dr mod_IirrE // cfIirrE ?lin_char_irr // join_subG andbCA. rewrite {1}cfker_mod //= !{1}sub_cfker_mod //; apply/andP; split; last first. rewrite -(sdprodWY (sdprod_cfker _ _)) sub_gen ?subsetU // orbC. rewrite (subset_trans _ (cfker_dprod _ _ _)) // sub_gen ?subsetU // orbC. by rewrite /lam mod_IirrE ?cfker_mod. apply: contraL nz_i => /(subset_trans sH1H); rewrite !inE negbK. by move/(sub_cfker_Res (subxx _)); rewrite thetaH1 subGcfker. have nsCH1_U: 'C_U(H1 | 'Q) <| U by rewrite sub_der1_normal. have nH1cU: (U / H0)%g \subset 'N(H1c). rewrite -(bigdprodWY defH1c) norms_gen ?norms_bigcup //. apply/bigcapsP=> w /setD1P[_ W1w]. by rewrite normJ -sub_conjgV (normsP (quotient_norms H0 nUW1)) ?groupV. have ->: #|Mtheta| = (#|Xtheta| * a)%N. rewrite Da mulnC -card_imset_Ind_irr // => _ xy /imset2P[i j nz_i _ ->]. case/(mem_sdprod defHU)=> x [y [Hx Uy -> _]]; have HUy := subsetP sUHU y Uy. pose yb := inMb y; have Uyb: yb \in (U / H0)%g by rewrite mem_quotient. pose iy := conjg_Iirr i yb; pose jy := conjg_Iirr j (coset (U' / H0)%g yb). apply/imset2P; exists iy jy; rewrite !inE ?conjg_Iirr_eq0 // in nz_i *. apply: irr_inj; have HCH1x: x \in HCH1 by rewrite mem_gen ?inE ?Hx. rewrite conjg_IirrE (cfConjgM _ nsHCH1_HU) ?(subsetP sHHU x) {Hx}//. rewrite {x HCH1x}(cfConjg_id _ HCH1x) !{1}mod_IirrE //. rewrite !{1}cfIirrE ?lin_char_irr //. rewrite cfConjgMod_norm ?(subsetP nH0U) ?(subsetP (normal_norm nsHCH1_HU)) //. have nCH1_Ub: (U / H0)%g \subset 'N('C_(U / H0)(H1)). by rewrite normsI ?normG ?norms_cent. rewrite cfConjgSdprod ?cfConjgDprod ?(subsetP _ _ Uyb) ?normsY //. rewrite /theta /lam !{1}mod_IirrE // !{1}conjg_IirrE. by rewrite cfConjgMod_norm ?(subsetP _ _ Uyb) // quotient_norms ?gFnorm. rewrite leq_pmul2r ?indexg_gt0 // cardE -(size_map (fun s => 'Ind[M] 'chi_s)). have kerH1c s: s \in Xtheta -> H1c \subset (cfker 'chi_s / H0)%g. case/imsetP=> r Mr {s}->; have [i j _ _ Dr] := imset2P Mr. rewrite -(setIidPr (normal_sub nsH1cHCH1)) -morphim_setIpre quotientS //. rewrite cfIirrE ?irr_Xtheta ?sub_cfker_Ind_irr //; last first. by rewrite normsI ?normal_norm // -(quotientGK nsH0_HU) cosetpre_normal. rewrite Dr mod_IirrE // cfker_morph ?normal_norm // cfIirrE ?lin_char_irr //. by rewrite setIS ?joing_subl ?morphpreS // cfker_sdprod. have injXtheta: {in M & Xtheta &, forall w s1 s2, 'chi_s1 = 'chi_s2 ^ w -> w \in HU}%CF. - move=> _ s1 s2 /(mem_sdprod defM)[y [w [HUy W1w -> _]]] Xs1 Xs2. rewrite groupMl // cfConjgMnorm ?(subsetP (normG _) y) ?(subsetP nHUW1) //. rewrite {y HUy}(cfConjg_id _ HUy) => Ds1. have nH0w: w \in 'N(H0) by rewrite ?(subsetP nH0M) ?(subsetP sW1M). rewrite (subsetP (normal_sub nsH0_HU)) // coset_idr //. have /setDP[]:= subsetP sXthetaXH0U' s1 Xs1; rewrite !inE join_subG /=. case/andP=> kerH0s1 _; apply: contraNeq; rewrite -eq_invg1 => ntw. rewrite -(quotientSGK nH0H) // -(dprodW defHb1) mul_subG ?kerH1c //=. rewrite Ds1 cfker_conjg ?(subsetP nHUW1) // quotientJ // -sub_conjgV. rewrite (subset_trans _ (kerH1c s2 Xs2)) // -(bigdprodWY defH1c) sub_gen //. by rewrite (bigcup_max (inMb w)^-1%g) // !inE ntw groupV mem_quotient. rewrite -size_filter uniq_leq_size //. apply/dinjectiveP=> s1 s2 Xs1 Xs2. case/(cfclass_Ind_irrP _ _ (der_normal 1 M))/cfclassP=> y My Ds2. by apply: irr_inj; rewrite Ds2 cfConjg_id ?(injXtheta y s1 s2). move=> _ /imageP[s Xs ->]; rewrite mem_filter /= cfInd1 // -(index_sdprod defM). rewrite Xtheta_1 // -natrM eqxx mem_seqInd ?gFnormal //. rewrite (subsetP sXthetaXH0U') // !andbT inertia_Ind_irr ?gFnormal //. by apply/subsetP=> y /setIP[My /inertiaJ/esym/injXtheta->]. 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)