proposition: Lemma typeP_Galois_characters (is_Galois : typeP_Galois) : [/\ {in X_ H0, forall s, (u %| 'chi_s 1%g)%Cx}, {in X_ H0C', forall s, 'chi_s 1%g = u%:R /\ (exists2 xi : 'CF(HC), xi \is a linear_char & 'chi_s = 'Ind xi)}, size mu_ = p.-1 /\ {in mu_, forall mu_j, isIndHC mu_j} & all redM (S_ H0C') -> [/\ C :=: 1%g, u = (p ^ q).-1 %/ p.-1 & [Frobenius HU / H0 = Hbar ><| (U / H0)]]].
proof: Proof. have [F [phi [psi _ [Kpsi phiJ]]]] := typeP_Galois_P is_Galois. case=> [oF /isomP[inj_phi im_phi] phiW2] [cycUbar co_u_p1 u_dv_pq1]. have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM. have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU. have [nsH0C_M nsHC_M _ nsH0C'_M] := nsH0xx_M; have nH0H := normal_norm nsH0H. have nsH0HU: H0 <| HU := normalS (subset_trans sH0H sHHU) sHUM nsH0M. have nH0U: U \subset 'N(H0) := subset_trans sUHU (normal_norm nsH0HU). have nH0C := subset_trans sCU nH0U. have sH0C_HU: H0C \subset HU by rewrite -(sdprodWY defHU) genS ?setUSS. have nsH0C_HU: H0C <| HU := normalS sH0C_HU sHUM nsH0C_M. have nH0C_HU := normal_norm nsH0C_HU. have [coH0U coHC] := (coprimeSg sH0H coHU, coprimegS sCU coHU). have [nH0C_H nH0C_U] := (subset_trans sHHU nH0C_HU, subset_trans sUHU nH0C_HU). have tiHOC_H: H0C :&: H = H0. by rewrite /= norm_joinEr // -group_modl // setIC coprime_TIg ?mulg1. have{coH0U} tiHOC_U: H0C :&: U = C. by rewrite /= norm_joinEr // setIC -group_modr // setIC coprime_TIg ?mul1g. have isoHbar: Hbar \isog H / H0C. by have:= second_isog nH0C_H; rewrite tiHOC_H. have isoUbar: Ubar \isog U / H0C. by have:= second_isog nH0C_U; rewrite tiHOC_U. have frobHU: [Frobenius HU / H0C = (H / H0C) ><| (U / H0C)]. have defHUbar: (H / H0C) ><| (U / H0C) = (HU / H0C)%g. exact: quotient_coprime_sdprod. apply/Frobenius_semiregularP=> //; first by rewrite -(isog_eq1 isoHbar). by rewrite -(isog_eq1 isoUbar); have [] := Frobenius_context frobUW1c. move=> yb /setD1P[ntyb /morphimP[y nH0Cy Uy] Dyb] /=; rewrite Dyb. apply/trivgP/subsetP=> _ /setIP[/morphimP[/= x nHOCx Hx ->] /cent1P/commgP]. rewrite -morphR //; set xy := [~ x, y] => /eqP/coset_idr/=H0Cxy. have [nH0x nH0y] := (subsetP nH0H x Hx, subsetP nH0U y Uy). rewrite inE coset_id ?mem_gen // inE coset_idr //; apply: contraNeq ntyb. rewrite -(morph_injm_eq1 inj_phi) ?mem_quotient // => nz_x. rewrite {yb}Dyb /= coset_id ?mem_gen // -Kpsi !inE Uy orbC /= -val_eqE. rewrite -(inj_eq (mulfI nz_x)) mulr1 -[_ * _]phiJ ?mem_quotient // qactJ nH0y. rewrite -morphJ // conjg_mulR -/xy mkerr ?eqxx // ker_coset -tiHOC_H inE. by rewrite andbC groupM ?groupV ?memJ_norm ?(subsetP nHU) //= H0Cxy ?groupR. have{coHC} tiHbC: (Hbar :&: C / H0 = 1)%g by rewrite coprime_TIg ?coprime_morph. have{tiHbC} defHCbar: Hbar \x (C / H0) = (HC / H0)%g. by rewrite dprodEY ?quotientY // [C]unlock/= astabQ quotient_setIpre subsetIr. have sHCHU: HC \subset HU by rewrite -(sdprodWY defHU) genS ?setUS. have nsHCHU: HC <| HU := normalS sHCHU sHUM nsHC_M. have sH0HC: H0 \subset HC := subset_trans sH0H (joing_subl H C). have nsH0HC: H0 <| HC := normalS sH0HC sHCHU nsH0HU. have nsHHUb: Hbar <| HU / H0 by rewrite quotient_normal. have I_XH0_C i: i != 0 -> 'I_HU['chi[Hbar]_i %% H0]%CF = HC. move=> /= nz_i; apply/esym/eqP. have nsCHUb: C / H0 <| HU / H0 by rewrite -quotientYidl ?quotient_normal. have sH0C_HC: H0C \subset HC by rewrite genS ?setSU. have nsH0C_HC: H0C <| HC := normalS sH0C_HC sHCHU nsH0C_HU. have [j Dj]: exists j, 'chi_j = (cfDprodl defHCbar 'chi_i %% H0)%CF. by rewrite -dprodl_IirrE -mod_IirrE //; set j := mod_Iirr _; exists j. have kerH0Cj: H0C \subset cfker 'chi_j. by rewrite Dj sub_cfker_mod ?join_subG ?normG // quotientYidl ?cfker_sdprod. rewrite inertia_mod_pre // -(inertia_dprodl defHCbar) ?normal_norm //. rewrite -inertia_mod_pre // -Dj eqEsubset sub_Inertia //=. rewrite -(quotientSGK _ sH0C_HC) ?subIset ?nH0C_HU -?inertia_quo //. rewrite -(quotientYidr nH0C_H) joingA (joing_idPl sH0H) in frobHU. rewrite -?quo_IirrE ?(inertia_Frobenius_ker (FrobeniusWker frobHU)) //. by rewrite quo_Iirr_eq0 // -irr_eq1 Dj cfMod_eq1 // cfDprodl_eq1 irr_eq1. have{I_XH0_C} irr_IndHC r: r \in Iirr_kerD HC H H0 -> 'Ind 'chi_r \in irr HU. rewrite !inE => /andP[ker'H kerH0]; apply: inertia_Ind_irr => //. apply: subset_trans (sub_inertia_Res _ (normal_norm nsHHU)) _. rewrite -{kerH0}(quo_IirrK _ kerH0) // mod_IirrE // in ker'H *. have /codomP[[i j] Dr] := dprod_Iirr_onto defHCbar (quo_Iirr H0 r). rewrite {r}Dr dprod_IirrE cfResMod ?joing_subl ?sub_cfker_mod //= in ker'H *. rewrite cfDprod_Resl linearZ inertia_scale_nz ?irr1_neq0 ?I_XH0_C //. by apply: contraNneq ker'H => ->; rewrite irr0 cfDprod_cfun1l cfker_sdprod. have [nb_mu H0C_mu] := nb_redM_H0; set part_a' := ({in X_ H0C', _}). have Part_a s: s \in X_ H0 -> exists r, 'chi_s = 'Ind[HU, HC] 'chi_r. rewrite !inE => /andP[Ks'H KsH0]; have [r sHCr] := constt_cfRes_irr HC s. have{KsH0} KrH0: H0 \subset cfker 'chi_r. by rewrite (sub_cfker_constt_Res_irr sHCr) // ?normal_norm. have{Ks'H} Kr'H: ~~ (H \subset cfker 'chi_r). by rewrite (sub_cfker_constt_Res_irr sHCr) ?joing_subl // ?normal_norm. have /irr_IndHC/irrP[s1 Ds1]: r \in Iirr_kerD HC H H0 by rewrite !inE Kr'H. rewrite -constt_Ind_Res Ds1 constt_irr inE in sHCr. by rewrite (eqP sHCr) -Ds1; exists r. have [nH0HC nH0C'] := (normal_norm nsH0HC, subset_trans (der_sub 1 _) nH0C). have Part_a': part_a'. move=> s /setDP[KsH0C' Ks'H]; have [|r Ds] := Part_a s. by rewrite inE Ks'H (subsetP (Iirr_kerS _ _) _ KsH0C') ?joing_subl. suffices lin_r: 'chi_r \is a linear_char. by split; [rewrite Du Ds cfInd1 ?lin_char1 ?mulr1 | exists 'chi_r]. have KrH0C': H0C' \subset cfker 'chi_r. rewrite inE Ds sub_cfker_Ind_irr // in KsH0C'. by rewrite (subset_trans sHUM) ?normal_norm. rewrite lin_irr_der1 (subset_trans _ KrH0C') //= (norm_joinEr nH0C'). rewrite -quotientSK ?gFsub_trans ?quotient_der //= -/C. by rewrite -(der_dprod 1 defHCbar) (derG1P abHbar) dprod1g. split=> // [s /Part_a[r ->] | | {Part_a' part_a'}red_H0C']. - by rewrite Du cfInd1 // dvdC_mulr // Cint_Cnat ?Cnat_irr1. - split=> // mu_j /H0C_mu H0C_mu_j; have [s XH0Cs Dmuj] := seqIndP H0C_mu_j. have [|s1u [xi lin_xi Ds]] := Part_a' s. by rewrite (subsetP _ _ XH0Cs) ?Iirr_kerDS // genS ?setUS ?der_sub. split=> //; first by rewrite Dmuj cfInd1 // s1u -natrM -(index_sdprod defM). by rewrite Dmuj Ds cfIndInd //; exists xi. have C1: C :=: 1%g. apply: contraTeq red_H0C' => ntC; apply/allPn. have sCM: C \subset M := subset_trans sCU (subset_trans sUHU sHUM). have{sCM} solCbar: solvable (C / H0). by rewrite quotient_sol ?(solvableS sCM) ?mmax_sol. have [|{ntC solCbar} j lin_j nz_j] := solvable_has_lin_char _ solCbar. rewrite -(isog_eq1 (quotient_isog _ _)) ?(subset_trans sCU) //. by rewrite coprime_TIg ?(coprimegS sCU) ?(coprimeSg sH0H). have [i lin_i nz_i] := solvable_has_lin_char ntHbar solHbar. pose r := mod_Iirr (dprod_Iirr defHCbar (i, j)). have KrH0: H0 \subset cfker 'chi_r by rewrite mod_IirrE ?cfker_mod. have Kr'H: ~~ (H \subset cfker 'chi_r). rewrite -subsetIidl -cfker_Res ?joing_subl ?irr_char // mod_IirrE //. rewrite cfResMod ?joing_subl // sub_cfker_mod // dprod_IirrE. by rewrite cfDprodKl ?lin_char1 // subGcfker -irr_eq1. have /irr_IndHC/irrP[s Ds]: r \in Iirr_kerD HC H H0 by rewrite !inE Kr'H. have Ks'H: s \notin Iirr_ker HU H. by rewrite inE -Ds sub_cfker_Ind_irr ?normal_norm. exists ('Ind 'chi_s). rewrite mem_seqInd ?gFnormal // inE Ks'H inE -Ds. rewrite sub_cfker_Ind_irr // ?(subset_trans sHUM) ?normal_norm //=. rewrite mod_IirrE // join_subG cfker_mod // sub_cfker_mod ?quotient_der //. apply: subset_trans (dergS 1 (quotientS H0 (joing_subr H C))) _. by rewrite -lin_irr_der1 dprod_IirrE cfDprod_lin_char. apply: contra nz_j => red_j; have /implyP := H0C_mu ('Ind 'chi_s). rewrite mem_filter red_j !mem_seqInd ?gFnormal // !in_setD Ks'H !inE -Ds. rewrite irr_eq1 !sub_cfker_Ind_irr ?(normal_norm nsH0HU) //. rewrite mod_IirrE // join_subG cfker_mod //= sub_cfker_mod // dprod_IirrE. by move/(sub_cfker_Res (subxx _)); rewrite cfDprodKr ?lin_char1 ?subGcfker. rewrite /= -/C C1 joingG1 in frobHU; split=> //; move/FrobeniusWker in frobHU. have nsHbHU: Hbar <| (HU / H0) by rewrite quotient_normal. have ->: (p ^ q).-1 = (#|X_ H0| * u)%N. rewrite -oF -cardsT -im_phi card_injm // -(card_Iirr_abelian abHbar). rewrite -(cardsC1 0) (card_imset_Ind_irr nsHbHU) => [|i|i y]; last first. - by rewrite !inE conjg_Iirr_eq0. - by rewrite !inE => nz_i; rewrite inertia_Ind_irr ?inertia_Frobenius_ker. rewrite index_quotient_eq ?(subset_trans sHUM) ?subIset ?sH0H ?orbT //. apply/eqP; rewrite Du /= C1 joingG1 mulnC eqn_pmul2r //. rewrite -(card_imset _ (can_inj (mod_IirrK _))) // -imset_comp. apply/eqP/eq_card=> s; apply/imsetP/idP=> [[i nz_i -> /=] | Xs]. rewrite !inE mod_IirrE 1?{1}cfker_mod // andbT in nz_i *. rewrite cfIirrE ?inertia_Ind_irr ?inertia_Frobenius_ker // sub_cfker_mod //. by rewrite sub_cfker_Ind_irr ?quotientS ?normal_norm // subGcfker. have [[]] := (Part_a s Xs, setDP Xs). rewrite /= C1 joingG1 !inE => r Ds [kerH0s]. have:= kerH0s; rewrite Ds !sub_cfker_Ind_irr ?normal_norm // => kerH0 ker'H. exists (quo_Iirr H0 r). by rewrite !inE -subGcfker quo_IirrE // cfker_quo ?quotientSGK. by rewrite quo_IirrE // cfIndQuo // -Ds -quo_IirrE // irrK quo_IirrK. suffices ->: #|X_ H0| = p.-1 by rewrite -(subnKC (prime_gt1 p_pr)) mulKn. rewrite -nb_mu (size_red_subseq_seqInd_typeP MtypeP _ H0C_mu) //; last first. - exact/allP/filter_all. - by rewrite filter_uniq ?seqInd_uniq. apply/esym/eq_card => i; rewrite inE mem_filter mem_seqInd ?gFnormal //. rewrite andb_idl // => Xi; rewrite (allP red_H0C') //. by rewrite mem_seqInd ?gFnormal //= C1 (trivgP (der_sub 1 _)) joingG1. 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)