proposition: Lemma typeP_Galois_P : typeP_Galois -> {F : finFieldType & {phi : {morphism Hbar >-> F} & {psi : {morphism U >-> {unit F}} & {eta : {morphism W1 >-> {perm F}} & forall alpha : {perm F}, reflect (additive alpha * multiplicative alpha) (alpha \in eta @* W1) & [/\ 'injm eta, {in Hbar & W1, morph_act 'Q 'P phi eta} & {in U & W1, forall x w, val (psi (x ^ w)) = eta w (val (psi x))}]} & 'ker psi = C /\ {in Hbar & U, morph_act 'Q 'U phi psi}} & [/\ #|F| = (p ^ q)%N, isom Hbar [set: F] phi & phi @* W2bar = <[1%R : F]>]} & [/\ cyclic Ubar, coprime u p.-1 & u %| (p ^ q).-1 %/ p.-1]}.
proof: Proof. move=> irrU; have [_ sUW1M _ /joing_subP[nHU nHW1] _] := sdprod_context defHUW1. have [nHbU nHbW1] := (quotient_norms H0 nHU, quotient_norms H0 nHW1). have{sUW1M} /joing_subP[nH0U nH0W1] := subset_trans sUW1M nH0M. have [ltCU oW2b oHb] := Ptype_Fcore_factor_facts. pose rU := abelem_repr abelHbar ntHbar nHbU. pose inHb := rVabelem abelHbar ntHbar; pose outHb := abelem_rV abelHbar ntHbar. have{} irrU: mx_irreducible rU by apply/abelem_mx_irrP; rewrite -acts_irrQ. pose E_U := [pred A | (A \in enveloping_algebra_mx rU)%MS]. have cEE A: A \in E_U -> centgmx rU A. case/envelop_mxP=> z_ ->{A}; rewrite -memmx_cent_envelop linear_sum. rewrite summx_sub // => x Ux; rewrite linearZ scalemx_sub {z_}//=. rewrite memmx_cent_envelop; apply/centgmxP=> y Uy. rewrite -repr_mxM // commgC 2?repr_mxM ?(groupR, groupM) -/rU; [| by []..]. apply/row_matrixP=> i; rewrite row_mul; move: (row i _) => h. have cHbH': (U / H0)^`(1) \subset 'C(Hbar). by rewrite -quotient_der ?quotient_cents. apply: rVabelem_inj; rewrite rVabelemJ ?groupR //; apply: (canLR (mulKg _)). by rewrite -[LHS](centsP cHbH')// ?mem_commg ?mem_rVabelem. have{cEE} [F [outF [inF outFK inFK] E_F]]: {F : finFieldType & {outF : {rmorphism F -> 'M(Hbar)%Mg} & {inF : {additive _ -> _} | cancel outF inF & {in E_U, cancel inF outF}} & forall a, outF a \in E_U}}%R. - pose HACK := enveloping_algebra_mx rU. pose B := row_base HACK. have freeB: row_free B by apply: row_base_free. pose outF : {additive _ -> _} := vec_mx \o mulmxr B. pose inF : {additive _ -> _} := mulmxr (pinvmx B) \o mxvec. have E_F a: outF a \in E_U by rewrite !inE vec_mxK mulmx_sub ?eq_row_base. have inK: {in E_U, cancel inF outF}. by move=> A E_A; rewrite /= mulmxKpV ?mxvecK ?eq_row_base. set HACK2 := (quotient_coset_of__canonical__fingroup_FinGroup _) in @outF inF E_F inK *. have outI: injective outF := inj_comp (can_inj vec_mxK) (row_free_inj freeB). have outK: cancel outF inF by move=> a; apply: outI; rewrite inK ?E_F. pose one := inF 1%R; pose mul a b := inF (outF a * outF b)%R. have outM: {morph outF: a b / mul a b >-> a * b}%R. by move=> a b; rewrite inK //; apply: envelop_mxM; apply: E_F. have out0: outF 0%R = 0%R by apply: raddf0. have out1: outF one = 1%R by rewrite inK //; apply: envelop_mx1. have nzFone: one != 0%R by rewrite -(inj_eq outI) out1 out0 oner_eq0. have mulA: associative mul by move=> *; apply: outI; rewrite !{1}outM mulrA. have mulC: commutative mul. move=> a b; apply: outI; rewrite !{1}outM. by apply: cent_mxP (E_F a); rewrite memmx_cent_envelop cEE ?E_F. have mul1F: left_id one mul by move=> a; apply: outI; rewrite outM out1 mul1r. have mulD: left_distributive mul +%R%R. by move=> a1 a2 b; apply: canLR outK _; rewrite !raddfD mulrDl -!{1}outM. pose rV_isComRing := GRing.Zmodule_isComRing.Build 'rV__ mulA mulC mul1F mulD nzFone. Time pose Fring : comRingType := HB.pack 'rV__ rV_isComRing. have outRM: multiplicative (outF : Fring -> _) by []. have mulI (nza : {a | a != 0%R :> Fring}): GRing.rreg (val nza). case: nza => a /=; rewrite -(inj_eq outI) out0 => nzA b1 b2 /(congr1 outF). rewrite !{1}outM => /row_free_inj eqB12; apply/outI/eqB12. by rewrite row_free_unit (mx_Schur irrU) ?cEE ?E_F. pose inv (a : Fring) := oapp (fun nza => invF (mulI nza) one) a (insub a). have inv0: (inv 0 = 0)%R by rewrite /inv insubF ?eqxx. pose field_axiom (R : ringType) inv := (forall x : R, x != 0 :>R -> inv x * x = 1 :> R)%R. have mulV: field_axiom _ inv. by move=> a nz_a; rewrite /inv insubT /= (f_invF (mulI (exist _ _ _))). pose IsField := GRing.ComRing_isField.Build Fring mulV inv0. Time pose F : finFieldType := HB.pack Fring IsField. pose outaM := GRing.isAdditive.Build Fring _ _ (raddfB outF). pose outmM := GRing.isMultiplicative.Build _ _ _ outRM. pose outRMT : GRing.RMorphism.type Fring _ := HB.pack (outF : _ -> _) outaM outmM. by exists F, outRMT; first exists inF. pose in_uF (a : F) : {unit F} := insubd (1 : {unit F}) a. have in_uF_E a: a != 1 -> val (in_uF a) = a. by move=> nt_a; rewrite insubdK /= ?unitfE. have [psi psiK]: {psi : {morphism U >-> {unit F}} | {in U, forall x, outF (val (psi x)) = rU (inMb x)}}. - pose psi x := in_uF (inF (rU (inMb x))). have psiK x: x \in U -> outF (val (psi x)) = rU (inMb x). move/(mem_quotient H0)=> Ux; have EUx := envelop_mx_id rU Ux. rewrite in_uF_E ?inFK //; apply: contraTneq (repr_mx_unitr rU Ux). by move/(canRL_in inFK EUx)->; rewrite rmorph0 unitr0. suffices psiM: {in U &, {morph psi: x y / x * y}} by exists (Morphism psiM). move=> x y Ux Uy /=; apply/val_inj/(can_inj outFK); rewrite rmorphM //=. by rewrite !{1}psiK ?groupM // morphM ?(subsetP nH0U) ?repr_mxM ?mem_quotient. have /trivgPn/sig2W[s W2s nts]: W2bar != 1%G. by rewrite -cardG_gt1 oW2b prime_gt1. pose sb := outHb s; have [Hs cW1s] := setIP W2s. have nz_sb: sb != 0%R by rewrite morph_injm_eq1 ?abelem_rV_injm. pose phi' a : coset_of H0 := inHb (sb *m outF a)%R. have Hphi' a: phi' a \in Hbar by apply: mem_rVabelem. have phi'D: {in setT &, {morph phi' : a b / a * b}}. by move=> a b _ _; rewrite /phi' !raddfD [inHb _]morphM ?mem_im_abelem_rV. have inj_phi': injective phi'. move=> a b /rVabelem_inj eq_sab; apply: contraNeq nz_sb. rewrite -[sb]mulmx1 idmxE -(rmorph1 outF) -subr_eq0 => /divff <-. by rewrite rmorphM /= mulmxA !raddfB /= eq_sab subrr mul0mx. have injm_phi': 'injm (Morphism phi'D) by apply/injmP; apply: in2W. have Dphi: 'dom (invm injm_phi') = Hbar. apply/setP=> h; apply/morphimP/idP=> [[a _ _ ->] // | Hh]. have /cyclic_mxP[A E_A def_h]: (outHb h <= cyclic_mx rU sb)%MS. by rewrite -(mxsimple_cyclic irrU) ?submx1. by exists (inF A); rewrite ?inE //= /phi' inFK // -def_h [inHb _]abelem_rV_K. have [phi [def_phi Kphi _ im_phi]] := domP _ Dphi. have{Kphi} inj_phi: 'injm phi by rewrite Kphi injm_invm. have{} im_phi: phi @* Hbar = setT by rewrite im_phi -Dphi im_invm. have phiK: {in Hbar, cancel phi phi'} by rewrite def_phi -Dphi; apply: invmK. have{def_phi Dphi injm_phi'} phi'K: cancel phi' phi. by move=> a; rewrite def_phi /= invmE ?inE. have phi'1: phi' 1%R = s by rewrite /phi' rmorph1 mulmx1 [inHb _]abelem_rV_K. have phi_s: phi s = 1%R by rewrite -phi'1 phi'K. have phiJ: {in Hbar & U, forall h x, phi (h ^ inMb x) = phi h * val (psi x)}%R. move=> h x Hh Ux; have Uxb := mem_quotient H0 Ux. apply: inj_phi'; rewrite phiK ?memJ_norm ?(subsetP nHbU) // /phi' rmorphM /=. by rewrite psiK // mulmxA [inHb _]rVabelemJ // -/inHb [inHb _]phiK. have Kpsi: 'ker psi = C. apply/setP=> x; rewrite [C]unlock 2!in_setI /= astabQ; apply: andb_id2l => Ux. have Ubx := mem_quotient H0 Ux; rewrite 3!inE (subsetP nH0U) //= inE. apply/eqP/centP=> [psi_x1 h Hh | cHx]; last first. by apply/val_inj; rewrite -[val _]mul1r -phi_s -phiJ // conjgE -cHx ?mulKg. red; rewrite (conjgC h) -[h ^ _]phiK ?memJ_norm ?(subsetP nHbU) ?phiJ //. by rewrite psi_x1 mulr1 phiK. have etaP (w : subg_of W1): injective (fun a => phi (phi' a ^ inMb (val w))). case: w => w /=/(mem_quotient H0)/(subsetP nHbW1) => nHw a b eq_ab. apply/inj_phi'/(conjg_inj (inMb w)). by apply: (injmP inj_phi) eq_ab; rewrite memJ_norm ?mem_rVabelem. pose eta w : {perm F} := perm (etaP (subg W1 w)). have etaK: {in Hbar & W1, forall h w, eta w (phi h) = phi (h ^ inMb w)}. by move=> h w Hh Ww; rewrite /= permE subgK ?phiK. have eta1 w: w \in W1 -> eta w 1%R = 1%R. move=> Ww; rewrite -phi_s etaK //. by rewrite conjgE (centP cW1s) ?mulKg ?mem_quotient. have etaM: {in W1 &, {morph eta: w1 w2 / w1 * w2}}. move=> w1 w2 Ww1 Ww2; apply/permP=> a; rewrite -[a]phi'K permM. rewrite !etaK ?memJ_norm ?groupM ?(subsetP nHbW1) ?mem_quotient //. by rewrite -conjgM -morphM ?(subsetP nH0W1). have etaMpsi a: {in U & W1, forall x w, eta w (a * val (psi x)) = eta w a * val (psi (x ^ w)%g)}%R. - move=> x w Ux Ww; rewrite -[a]phi'K (etaK _ w (Hphi' a) Ww). rewrite -!phiJ // ?memJ_norm ?(subsetP nHbW1, subsetP nUW1) ?mem_quotient //. rewrite etaK ?memJ_norm ?(subsetP nHbU) ?mem_quotient // -!conjgM. by rewrite conjgC -morphJ ?(subsetP nH0U x Ux, subsetP nH0W1 w Ww). have psiJ: {in U & W1, forall x w, val (psi (x ^ w)) = eta w (val (psi x))}. by move=> x w Ux Ww /=; rewrite -[val _]mul1r -(eta1 w Ww) -etaMpsi ?mul1r. have etaRM w: w \in W1 -> (additive (eta w) * multiplicative (eta w)). move=> Ww; have nUw := subsetP nHbW1 _ (mem_quotient _ Ww). have etaD: additive (eta w). move=> a b; rewrite -[a]phi'K -[b]phi'K -!zmodMgE -!zmodVgE. rewrite -morphV // -morphM ?{1}etaK ?groupM ?groupV // conjMg conjVg. by rewrite morphM 1?morphV ?groupV // memJ_norm. do 2![split=> //] => [a b|]; last exact: eta1. rewrite -[a]outFK; have /envelop_mxP[d ->] := E_F a. pose etaaM := GRing.isAdditive.Build _ _ _ etaD. pose etaA : GRing.Additive.type _ _ := HB.pack (fun_of_perm _) etaaM. rewrite raddf_sum mulr_suml ![eta w _](raddf_sum etaA) mulr_suml. apply: eq_bigr => _ /morphimP[x Nx Ux ->]; move: {d}(d _) => dx. rewrite -[dx]natr_Zp scaler_nat !(mulrnAl, raddfMn); congr (_ *+ dx)%R. by rewrite -psiK //= outFK mulrC etaMpsi // mulrC psiJ. have oF: #|F| = (p ^ q)%N by rewrite -cardsT -im_phi card_injm. pose nF := <[1%R : F]>; have o_nF: #|nF| = p. by rewrite -orderE -phi_s (order_injm inj_phi) // (abelem_order_p abelHbar). have cyc_uF := @field_unit_group_cyclic F. exists F. exists phi; last first. split=> //; first exact/isomP; apply/esym/eqP; rewrite eqEcard o_nF -phi_s. by rewrite cycle_subG mem_morphim //= card_injm ?subsetIl ?oW2b. exists psi => //; last first. by split=> // h x Hh Ux; rewrite qactJ (subsetP nH0U) ?phiJ. have inj_eta: 'injm (Morphism etaM). have /properP[_ [h Hh notW2h]]: W2bar \proper Hbar. by rewrite properEcard subsetIl oW2b oHb (ltn_exp2l 1) prime_gt1. apply/subsetP=> w /morphpreP[Ww /set1P/permP/(_ (phi h))]. rewrite etaK // permE => /(injmP inj_phi) => chw. rewrite -(@prime_TIg _ W1 <[w]>) //; first by rewrite inE Ww cycle_id. rewrite proper_subn // properEneq cycle_subG Ww andbT. apply: contraNneq notW2h => defW1; rewrite inE Hh /= -defW1. rewrite quotient_cycle ?(subsetP nH0W1) // cent_cycle cent1C inE. by rewrite conjg_set1 chw ?memJ_norm // (subsetP nHbW1) ?mem_quotient. exists (Morphism etaM) => [alpha |]; last first. by split=> // h w Hh Ww /=; rewrite qactJ (subsetP nH0W1) -?etaK. pose autF (f : {perm F}) := (additive f * multiplicative f)%type. have [r prim_r]: {r : F | forall f g, autF f -> autF g -> f r = g r -> f = g}. have /cyclicP/sig_eqW[r def_uF] := cyc_uF [set: {unit F}]%G. exists (val r) => f g fRM gRM eq_fgr; apply/permP=> a. pose faM := GRing.isAdditive.Build _ _ _ fRM.1. pose fmM := GRing.isMultiplicative.Build _ _ _ fRM.2. pose fRMT : GRing.RMorphism.type _ _ := HB.pack (fun_of_perm f) faM fmM. pose gaM := GRing.isAdditive.Build _ _ _ gRM.1. pose gmM := GRing.isMultiplicative.Build _ _ _ gRM.2. pose gRMT : GRing.RMorphism.type _ _ := HB.pack (fun_of_perm g) gaM gmM. rewrite (_ : f =1 fRMT) // (_ : g =1 gRMT) //. have [-> | /in_uF_E <-] := eqVneq a 0%R; first by rewrite !rmorph0. have /cycleP[m ->]: in_uF a \in <[r]> by rewrite -def_uF inE. by rewrite val_unitX !rmorphXn /= eq_fgr. have /sigW[P /and3P[Pr0 nP lePq]]: exists P: {poly F}, [&& root P r, all (mem nF) P & #|root P| <= q]. - pose Mr := (\matrix_(i < q.+1) (sb *m outF (r ^+ i)))%R. have /rowV0Pn[v /sub_kermxP vMr0 nz_v]: kermx Mr != 0%R. rewrite kermx_eq0 neq_ltn ltnS (leq_trans (rank_leq_col Mr)) //. by rewrite (dim_abelemE abelHbar) // oHb pfactorK. pose P : {poly F} := (\poly_(i < q.+1) (v 0 (inord i))%:R)%R. have szP: size P <= q.+1 by apply: size_poly. exists P; apply/and3P; split. + apply/eqP/inj_phi'; congr (inHb _); rewrite rmorph0 mulmx0 -vMr0. rewrite horner_poly !raddf_sum mulmx_sum_row; apply: eq_bigr => i _. rewrite rowK inord_val //= mulr_natl rmorphMn -scaler_nat scalemxAr. by rewrite natr_Zp. + apply/(all_nthP 0%R)=> i /leq_trans/(_ szP) le_i_q. by rewrite coef_poly /= le_i_q mem_cycle. rewrite cardE -ltnS (leq_trans _ szP) //. rewrite max_poly_roots ?enum_uniq //; last first. by apply/allP=> r'; rewrite mem_enum. apply: contraNneq nz_v => /polyP P0; apply/eqP/rowP=> i; apply/eqP. have /eqP := P0 i; rewrite mxE coef0 coef_poly ltn_ord inord_val. have charF: p \in [char F]%R by rewrite !inE p_pr -order_dvdn -o_nF /=. by rewrite -(dvdn_charf charF) (dvdn_charf (char_Fp p_pr)) natr_Zp. have{Pr0 nP} fPr0 f: autF f -> root P (f r). move=> fRM. pose faM := GRing.isAdditive.Build _ _ _ fRM.1. pose fmM := GRing.isMultiplicative.Build _ _ _ fRM.2. pose fRMT : GRing.RMorphism.type _ _ := HB.pack (fun_of_perm f) faM fmM. suff <-: map_poly fRMT P = P by apply: rmorph_root. apply/polyP=> i; rewrite coef_map. have [/(nth_default _)-> | lt_i_P] := leqP (size P) i; first exact: rmorph0. by have /cycleP[n ->] := all_nthP 0%R nP i lt_i_P; apply: rmorph_nat. apply: (iffP morphimP) => [[w _ Ww ->] | alphaRM]; first exact: etaRM. suffices /setP/(_ (alpha r)): [set (eta w) r | w in W1] = [set t | root P t]. rewrite inE fPr0 // => /imsetP[w Ww def_wr]; exists w => //. by apply: prim_r => //; apply: etaRM. apply/eqP; rewrite eqEcard; apply/andP; split. by apply/subsetP=> _ /imsetP[w Ww ->]; rewrite inE fPr0 //; apply: etaRM. rewrite (@cardsE F) card_in_imset // => w1 w2 Ww1 Ww2 /= /prim_r eq_w12. by apply: (injmP inj_eta) => //; apply: eq_w12; apply: etaRM. have isoUb: isog Ubar (psi @* U) by rewrite /Ubar -Kpsi first_isog. pose unF := [set in_uF a | a in nF^#]. have unF_E: {in nF^#, cancel in_uF val} by move=> a /setD1P[/in_uF_E]. have unFg: group_set unF. apply/group_setP; split=> [|_ _ /imsetP[a nFa ->] /imsetP[b nFb ->]]. have nF1: 1%R \in nF^# by rewrite !inE cycle_id oner_eq0. by apply/imsetP; exists 1%R => //; apply: val_inj; rewrite unF_E. have nFab: (a * b)%R \in nF^#. rewrite !inE mulf_eq0 negb_or. have [[-> /cycleP[m ->]] [-> /cycleP[n ->]]] := (setD1P nFa, setD1P nFb). by rewrite -natrM mem_cycle. by apply/imsetP; exists (a * b)%R => //; apply: val_inj; rewrite /= !unF_E. have <-: #|Group unFg| = p.-1. by rewrite -o_nF (cardsD1 1 nF) group1 (card_in_imset (can_in_inj unF_E)). have <-: #|[set: {unit F}]| = (p ^ q).-1. rewrite -oF -(cardC1 1) cardsT card_sub; apply: eq_card => a /=. by rewrite !inE unitfE. rewrite /u (isog_cyclic isoUb) (card_isog isoUb) cyc_uF. suffices co_u_p1: coprime #|psi @* U| #|Group unFg|. by rewrite -(Gauss_dvdr _ co_u_p1) mulnC divnK ?cardSg ?subsetT. rewrite -(cyclic_dprod (dprodEY _ _)) ?cyc_uF //. by rewrite (sub_abelian_cent2 (cyclic_abelian (cyc_uF [set:_]%G))) ?subsetT. apply/trivgP/subsetP=> _ /setIP[/morphimP[x Nx Ux ->] /imsetP[a nFa /eqP]]. have nCx: x \in 'N(C) by rewrite -Kpsi (subsetP (ker_norm _)). rewrite -val_eqE (unF_E a) //; case/setD1P: nFa => _ /cycleP[n {a}->]. rewrite zmodXgE => /eqP def_psi_x; rewrite mker ?set11 // Kpsi coset_idr //. apply/set1P; rewrite -set1gE -(Frobenius_trivg_cent frobUW1c) /= -/C. rewrite inE mem_quotient //= -sub1set -quotient_set1 ?quotient_cents2r //. rewrite gen_subG /= -/C -Kpsi; apply/subsetP=> _ /imset2P[_ w /set1P-> Ww ->]. have Uxw: x ^ w \in U by rewrite memJ_norm ?(subsetP nUW1). apply/kerP; rewrite (morphM, groupM) ?morphV ?groupV //. apply/(canLR (mulKg _))/val_inj; rewrite psiJ // mulg1 def_psi_x. pose etaaM := GRing.isAdditive.Build _ _ _ (etaRM w Ww).1. pose etamM := GRing.isMultiplicative.Build _ _ _ (etaRM w Ww).2. pose etaRMT : GRing.RMorphism.type _ _ := HB.pack (fun_of_perm _) etaaM etamM. exact: (rmorph_nat etaRMT). 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)