proposition: Lemma typeP_Galois_Pn : ~~ typeP_Galois -> {H1 : {group coset_of H0} | [/\ #|H1| = p, U / H0 \subset 'N(H1), [acts U, on H1 | 'Q], \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar & let a := #|U : 'C_U(H1 | 'Q)| in [/\ a > 1, a %| p.-1, cyclic (U / 'C_U(H1 | 'Q)) & exists V : {group 'rV['Z_a]_q.-1}, Ubar \isog V]]}.
proof: Proof. have [_ sUW1M defHUW1 nHUW1 _] := sdprod_context defHUW1. have [nHU nHW1] := joing_subP nHUW1. have nH0UW1 := subset_trans sUW1M nH0M; have [nH0U nH0W1] := joing_subP nH0UW1. rewrite /typeP_Galois acts_irrQ //= => not_minHbarU. have [H1 minH1 sH1Hb]: {H1 | minnormal (gval H1) (U / H0) & H1 \subset Hbar}. by apply: mingroup_exists; rewrite ntHbar quotient_norms. exists H1; have [defH1 | ltH1H] := eqVproper sH1Hb. by rewrite -defH1 minH1 in not_minHbarU. have [/andP[ntH1 nH1U] _] := mingroupP minH1. have actsUH1: [acts U, on H1 | 'Q]. by rewrite -(cosetpreK H1) actsQ ?norm_quotient_pre. have [nH0H [neqCU _ oHbar]] := (normal_norm nsH0H, Ptype_Fcore_factor_facts). have nUW1b: W1bar \subset 'N(U / H0) by apply: quotient_norms. have oW1b: #|W1bar| = q. rewrite -(card_isog (quotient_isog _ _)) // coprime_TIg //. by rewrite (coprimeSg sH0H) // (coprimegS (joing_subr U W1)). have [oH1 defHbar]: #|H1| = p /\ \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar. have nHbUW1: U <*> W1 / H0 \subset 'N(Hbar) by apply: quotient_norms. pose rUW1 := abelem_repr abelHbar ntHbar nHbUW1. have irrUW1: mx_irreducible rUW1. apply/abelem_mx_irrP/mingroupP; split=> [|H2]; first by rewrite ntHbar. case/andP=> ntH2 nH2UW1 sH2H; case/mingroupP: minHbar => _; apply=> //. by rewrite ntH2 -defHUW1 quotientMl // mulG_subG sub_abelian_norm. have nsUUW1: U / H0 <| U <*> W1 / H0 by rewrite quotient_normal // normalYl. pose rU := subg_repr rUW1 (normal_sub nsUUW1). pose V1 := rowg_mx (abelem_rV abelHbar ntHbar @* H1). have simV1: mxsimple rU V1 by apply/mxsimple_abelem_subg/mxsimple_abelemGP. have [W0 /subsetP sW01 [sumW0 dxW0]] := Clifford_basis irrUW1 simV1. have def_q: q = (#|W0| * \rank V1)%N. transitivity (\rank (\sum_(w in W0) V1 *m rUW1 w))%R. by rewrite sumW0 mxrank1 /= (dim_abelemE abelHbar) // oHbar pfactorK. rewrite (mxdirectP dxW0) -sum_nat_const; apply: eq_bigr => x /sW01/= Wx. by rewrite mxrankMfree ?row_free_unit ?repr_mx_unit. have oH1: #|H1| = (p ^ \rank V1)%N. by rewrite -{1}(card_Fp p_pr) -card_rowg rowg_mxK card_injm ?abelem_rV_injm. have oW0: #|W0| = q. apply/prime_nt_dvdP=> //; last by rewrite def_q dvdn_mulr. apply: contraTneq (proper_card ltH1H) => trivW0. by rewrite oHbar def_q trivW0 mul1n -oH1 ltnn. have q_gt0 := prime_gt0 pr_q. rewrite oH1 -(mulKn (\rank V1) q_gt0) -{1}oW0 -def_q divnn q_gt0. have defHbar: \big[dprod/1]_(w in W0) H1 :^ w = Hbar. have inj_rV_Hbar := rVabelem_injm abelHbar ntHbar. have/(injm_bigdprod _ inj_rV_Hbar)/= := bigdprod_rowg sumW0 dxW0. rewrite sub_im_abelem_rV rowg1 im_rVabelem => <- //=; apply: eq_bigr => w. by move/sW01=> Ww; rewrite abelem_rowgJ ?rowg_mxK ?abelem_rV_mK. have injW0: {in W0 &, injective (fun w => H1 :^ w)}. move=> x y Wx Wy /= eq_Hxy; apply: contraNeq ntH1 => neq_xy. rewrite -(conjsg_eq1 _ x) -[H1 :^ x]setIid {1}eq_Hxy; apply/eqP. rewrite (bigD1 y) // (bigD1 x) /= ?Wx // dprodA in defHbar. by case/dprodP: defHbar => [[_ _ /dprodP[_ _ _ ->] _]]. have defH1W0: [set H1 :^ w | w in W0] = [set H1 :^ w | w in W1 / H0]. apply/eqP; rewrite eqEcard (card_in_imset injW0) oW0 -oW1b leq_imset_card. rewrite andbT; apply/subsetP=> _ /imsetP[w /sW01/= Ww ->]. move: Ww; rewrite norm_joinEr ?quotientMl // => /mulsgP[x w1 Ux Ww1 ->]. by rewrite conjsgM (normsP nH1U) // imset_f. have injW1: {in W1 / H0 &, injective (fun w => H1 :^ w)}. by apply/imset_injP; rewrite -defH1W0 (card_in_imset injW0) oW0 oW1b. by rewrite -(big_imset id injW1) -defH1W0 big_imset. split=> //; set a := #|_ : _|; pose q1 := #|(W1 / H0)^#|. have a_gt1: a > 1. rewrite indexg_gt1 subsetIidl /= astabQ -sub_quotient_pre //. apply: contra neqCU => cH1U; rewrite [C]unlock (sameP eqP setIidPl) /= astabQ. rewrite -sub_quotient_pre // -(bigdprodWY defHbar) cent_gen centsC. by apply/bigcupsP=> w Ww; rewrite centsC centJ -(normsP nUW1b w) ?conjSg. have Wb1: 1 \in W1bar := group1 _. have ->: q.-1 = q1 by rewrite -oW1b (cardsD1 1) Wb1. have /cyclicP[h defH1]: cyclic H1 by rewrite prime_cyclic ?oH1. have o_h: #[h] = p by rewrite defH1 in oH1. have inj_Zp_h w := injm_Zp_unitm (h ^ w). pose phi w := invm (inj_Zp_h w) \o restr_perm <[h ^ w]> \o actperm 'Q. have dU w: w \in W1bar -> {subset U <= 'dom (phi w)}. move=> Ww x Ux; have Qx := subsetP (acts_dom actsUH1) x Ux. rewrite inE Qx /= im_Zp_unitm inE mem_morphpre //=; last first. by apply: Aut_restr_perm (actperm_Aut 'Q _); rewrite //= quotientT. rewrite cycleJ -defH1 !inE /=; apply/subsetP=> z H1w_z; rewrite inE actpermK. rewrite qactJ (subsetP nH0U) ?memJ_norm // normJ mem_conjg. by rewrite (subsetP nH1U) // -mem_conjg (normsP nUW1b) ?mem_quotient. have sUD := introT subsetP (dU _ _). have Kphi w: 'ker (phi w) = 'C(H1 :^ w | 'Q). rewrite !ker_comp ker_invm -kerE ker_restr_perm defH1 -cycleJ. apply/setP=> x; rewrite !inE; congr (_ && _) => /=. by apply: eq_subset_r => h1; rewrite !inE actpermK. have o_phiU w: w \in W1bar -> #|phi w @* U| = a. move=> Ww; have [w1 Nw1 Ww1 def_w] := morphimP Ww. rewrite card_morphim Kphi (setIidPr _) ?sUD // /a indexgI /= !astabQ. by rewrite centJ def_w morphpreJ // -{1}(normsP nUW1 w1 Ww1) indexJg. have a_dv_p1: a %| p.-1. rewrite -(o_phiU 1) // (dvdn_trans (cardSg (subsetT _))) // card_units_Zp //. by rewrite conjg1 o_h (@totient_pfactor p 1) ?muln1. have cycZhw w: cyclic (units_Zp #[h ^ w]). rewrite -(injm_cyclic (inj_Zp_h w)) // im_Zp_unitm Aut_prime_cyclic //=. by rewrite -orderE orderJ o_h. have cyc_phi1U: cyclic (phi 1 @* U) := cyclicS (subsetT _) (cycZhw 1). split=> //; last have{cyc_phi1U a_dv_p1} [z def_z] := cyclicP cyc_phi1U. by rewrite -(conjsg1 H1) -Kphi (isog_cyclic (first_isog_loc _ _)) ?sUD. have o_hw w: #[h ^ w] = #[h ^ 1] by rewrite !orderJ. pose phi1 w x := eq_rect _ (fun m => {unit 'Z_m}) (phi w x) _ (o_hw w). have val_phi1 w x: val (phi1 w x) = val (phi w x) :> nat. by rewrite /phi1; case: _ / (o_hw _). have mem_phi1 w x: w \in W1bar -> x \in U -> phi1 w x \in <[z]>%G. move=> Ww Ux; have: #|<[z]>%G| = a by rewrite /= -def_z o_phiU. rewrite /phi1; case: _ / (o_hw w) <[z]>%G => A oA /=. suffices <-: phi w @* U = A by rewrite mem_morphim // dU. by apply/eqP; rewrite (eq_subG_cyclic (cycZhw w)) ?subsetT // oA o_phiU. have o_z: #[z] = a by rewrite orderE -def_z o_phiU. pose phi0 w x := ecast m 'Z_m o_z (invm (injm_Zpm z) (phi1 w x)). pose psi x := (\row_(i < q1) (phi0 (enum_val i) x * (phi0 1 x)^-1)%g)%R. have psiM: {in U &, {morph psi: x y / x * y}}. have phi0M w: w \in W1bar -> {in U &, {morph phi0 w: x y / x * y}}. move=> Ww x y Ux Uy; rewrite /phi0; case: (a) / (o_z) => /=. rewrite -morphM; first 1 [congr (invm _ _)] || by rewrite im_Zpm mem_phi1. by rewrite /phi1; case: _ / (o_hw w); rewrite /= -morphM ?dU. move=> x y Ux Uy; apply/rowP=> i; have /setD1P[_ Ww] := enum_valP i. by rewrite !{1}mxE !{1}phi0M // addrCA -addrA -opprD addrCA addrA. suffices Kpsi: 'ker (Morphism psiM) = C. by exists [group of Morphism psiM @* U]; rewrite /Ubar -Kpsi first_isog. apply/esym/eqP; rewrite eqEsubset; apply/andP; split. rewrite [C]unlock -(bigdprodWY defHbar); apply/subsetP=> x /setIP[Ux cHx]. suffices phi0x1 w: w \in W1bar -> phi0 w x = 1. rewrite !inE Ux; apply/eqP/rowP=> i; have /setD1P[_ Ww] := enum_valP i. by rewrite !mxE !phi0x1 ?mulgV. move=> Ww; apply: val_inj; rewrite /phi0; case: (a) / (o_z); congr (val _). suffices /eqP->: phi1 w x == 1 by rewrite morph1. rewrite -2!val_eqE [val _]val_phi1 -(o_hw w) [phi _ _]mker // Kphi. by apply: subsetP (astabS _ _) _ cHx; rewrite sub_gen // (bigcup_sup w). have sKU: 'ker (Morphism psiM) \subset U by apply: subsetIl. rewrite -quotient_sub1 -?(Frobenius_trivg_cent frobUW1c); last first. by apply: subset_trans (normal_norm nsCUW1); rewrite subIset ?joing_subl. rewrite subsetI quotientS //= quotient_cents2r // [C]unlock subsetI. rewrite (subset_trans (commSg W1 sKU)) ?commg_subl //= astabQ gen_subG /=. apply/subsetP=> _ /imset2P[x w1 Kx Ww1 ->]. have:= Kx; rewrite -groupV 2!inE groupV => /andP[Ux /set1P/rowP psi_x'0]. have [nH0x Ux'] := (subsetP nH0U x Ux, groupVr Ux); pose x'b := (inMb x)^-1. rewrite mem_morphpre ?groupR ?morphR //= ?(subsetP nH0W1) //. have conj_x'b w: w \in W1bar -> (h ^ w) ^ x'b = (h ^ w) ^+ val (phi 1 x^-1). move=> Ww; transitivity (Zp_unitm (phi w x^-1) (h ^ w)). have /morphpreP[_ /morphpreP[Px' Rx']] := dU w Ww x^-1 Ux'. rewrite invmK ?restr_permE ?cycle_id //. by rewrite actpermE qactJ groupV nH0x morphV. have:= Ww; rewrite -(setD1K Wb1) autE ?cycle_id // => /setU1P[-> // | W'w]. have /eqP := psi_x'0 (enum_rank_in W'w w); rewrite 2!mxE enum_rankK_in //. rewrite -eq_mulgV1 -val_eqE /phi0; case: (a) / (o_z); rewrite /= val_eqE. rewrite (inj_in_eq (injmP (injm_invm _))) /= ?im_Zpm ?mem_phi1 //. by rewrite -2!val_eqE /= !val_phi1 // => /eqP->. rewrite -sub_cent1 -(bigdprodWY defHbar) gen_subG; apply/bigcupsP=> w2 Ww2. rewrite defH1 -cycleJ cycle_subG cent1C inE conjg_set1 !conjgM // conj_x'b //. rewrite conjXg -!conjgM -conj_x'b ?groupM ?groupV ?mem_quotient //. by rewrite !conjgM !conjgKV. 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)