proposition: Lemma coprime_act_abelian_pgroup_structure gT p (A X : {group gT}) : abelian A -> p.-group A -> p^'.-group X -> X \subset 'N(A) -> exists2 s : {set {group gT}}, \big[dprod/1]_(B in s) B = A & {in s, forall B : {group gT}, [/\ homocyclic B, X \subset 'N(B) & acts_irreducibly X (B / 'Phi(B)) 'Q]}.
proof: Proof. move: {2}_.+1 (ltnSn #|A|) => m. elim: m => // m IHm in gT A X *; rewrite ltnS => leAm cAA pA p'X nAX. have [n1 eA]: {n | exponent A = p ^ n}%N by apply p_natP; rewrite pnat_exponent. have [-> | ntA] := eqsVneq A 1. by exists set0 => [|B]; rewrite ?big_set0 ?inE. have [p_pr _ _] := pgroup_pdiv pA ntA; have p_gt1 := prime_gt1 p_pr. case: n1 => [|n] in eA; first by rewrite trivg_exponent eA in ntA. have nA1X: X \subset 'N('Ohm_1(A)) := gFnorm_trans _ nAX. have sAnA1: 'Mho^n(A) \subset 'Ohm_1(A). rewrite (MhoE n pA) (OhmE 1 pA) genS //. apply/subsetP=> _ /imsetP[x Ax ->]; rewrite !inE groupX //. by rewrite -expgM -expnSr -eA -order_dvdn dvdn_exponent. have nAnX: X \subset 'N('Mho^n(A)) := gFnorm_trans _ nAX. have [B minB sBAn]: {B : {group gT} | minnormal B X & B \subset 'Mho^n(A)}. apply: mingroup_exists; rewrite nAnX andbT; apply/trivgPn. have [x Ax ox] := exponent_witness (abelian_nil cAA). exists (x ^+ (p ^ n)); first by rewrite Mho_p_elt ?(mem_p_elt pA). by rewrite -order_dvdn -ox eA dvdn_Pexp2l ?ltnn. have abelA1: p.-abelem 'Ohm_1(A) by rewrite Ohm1_abelem. have sBA1: B \subset 'Ohm_1(A) := subset_trans sBAn sAnA1. have{minB} [/andP[ntB nBX] minB] := mingroupP minB. have{nBX sBA1} [U defA1 nUX] := Maschke_abelem abelA1 p'X sBA1 nA1X nBX. have [_ mulBU _ tiBU] := dprodP defA1; have{mulBU} [_ sUA1] := mulG_sub mulBU. have sUA: U \subset A := subset_trans sUA1 (Ohm_sub 1 _). have [U1 | {defA1 minB}ntU] := eqsVneq U 1. rewrite U1 dprodg1 /= in defA1. have homoA: homocyclic A. apply/(Ohm1_homocyclicP pA cAA); rewrite eA pfactorK //=. by apply/eqP; rewrite eqEsubset sAnA1 -defA1 sBAn. exists [set A]; rewrite ?big_set1 // => G; move/set1P->; split=> //. have OhmMho: forall k, 'Ohm_k(A) = 'Mho^(n.+1 - k)(A). by move=> k; rewrite (homocyclic_Ohm_Mho k pA) // eA pfactorK. have fM: {in A &, {morph (fun x => x ^+ (p ^ n)) : x y / x * y >-> x * y}}. by move=> x y Ax Ay /=; rewrite expgMn // /commute -(centsP cAA). pose f := Morphism fM; have ker_f: 'ker f = 'Phi(A). apply/setP=> z; rewrite (Phi_Mho pA cAA) -(subSnn n) -OhmMho. by rewrite (OhmEabelian pA) ?(abelianS (Ohm_sub n A)) ?inE. have [g injg def_g] := first_isom f; rewrite /= {}ker_f in g injg def_g. have{f} def_g: forall H, gval H \subset A -> g @* (H / _) = 'Mho^n(H). move=> H sHA; rewrite def_g morphimEsub //. by rewrite (MhoEabelian n (pgroupS sHA pA) (abelianS sHA cAA)). have im_g: g @* (A / 'Phi(A)) = B by rewrite def_g // defA1 OhmMho subn1. have defAb: A / 'Phi(A) = g @*^-1 B by rewrite -im_g injmK. have nsPhiA: 'Phi(A) <| A := Phi_normal A. have nPhiX: X \subset 'N('Phi(A)) := gFnorm_trans _ nAX. rewrite defAb; apply/mingroupP; split=> [|Hb]. by rewrite -(morphim_injm_eq1 injg) ?morphpreK /= -?defAb ?im_g ?ntB ?actsQ. case/andP=> ntHb actsXHb /= sgHbB; have [sHbA _] := subsetIP sgHbB. rewrite -sub_morphim_pre // in sgHbB; rewrite -(minB _ _ sgHbB) ?injmK //. rewrite morphim_injm_eq1 // {}ntHb {actsXHb}(subset_trans actsXHb) //=. have{sHbA} [H defHb sPhiH sHA] := inv_quotientS nsPhiA sHbA. rewrite defHb def_g // gFnorm_trans //=. by rewrite astabsQ ?subsetIr ?(normalS sPhiH sHA). have nsUA: U <| A by rewrite -sub_abelian_normal. have nUA: A \subset 'N(U) by case/andP: nsUA. have Au_lt_m: #|A / U| < m := leq_trans (ltn_quotient ntU sUA) leAm. have cAuAu: abelian (A / U) := quotient_abelian _ cAA. have pAu: p.-group (A / U) := quotient_pgroup _ pA. have p'Xu: p^'.-group (X / U) := quotient_pgroup _ p'X. have nXAu: X / U \subset 'N(A / U) := quotient_norms _ nAX. have{Au_lt_m p'Xu nXAu} [S defAu simS] := IHm _ _ _ Au_lt_m cAuAu pAu p'Xu nXAu. have sSAu: forall Ku, Ku \in S -> Ku \subset A / U. by move=> Ku S_Ku; rewrite -(bigdprodWY defAu) sub_gen // (bigcup_max Ku). have{B ntB sBAn tiBU} [Ku S_Ku eKu]: exists2 Ku, Ku \in S & exponent Ku == (p ^ n.+1)%N. apply/exists_inP; apply: contraR ntB; rewrite negb_exists_in -subG1 -tiBU. move/forall_inP=> expSpn; apply/subsetP=> x Ux; rewrite inE Ux coset_idr //. by rewrite (subsetP nUA) // (subsetP (Mho_sub n A)) // (subsetP sBAn). have [y Ay ->]: exists2 y, y \in A & x = y ^+ (p ^ n). by apply/imsetP; rewrite -MhoEabelian ?(subsetP sBAn). rewrite morphX ?(subsetP nUA) // (exponentP _ _ (mem_quotient _ Ay)) //. rewrite -sub_Ldiv -OhmEabelian ?(abelianS (Ohm_sub n _)) //=. rewrite (OhmE n pAu) /= -(bigdprodWY defAu) genS // subsetI sub_gen //=. apply/bigcupsP=> Ku S_Ku; rewrite sub_LdivT. have: exponent Ku %| p ^ n.+1. by rewrite (dvdn_trans (exponentS (sSAu _ S_Ku))) // -eA exponent_quotient. case/dvdn_pfactor=> // k le_k_n1 expKu; rewrite expKu dvdn_exp2l //. by rewrite -ltnS ltn_neqAle le_k_n1 -(eqn_exp2l _ _ p_gt1) -expKu expSpn. have{sSAu} [sKuA [homoKu nKuX minKu]] := (sSAu Ku S_Ku, simS Ku S_Ku). have [K defKu sUK sKA] := inv_quotientS nsUA sKuA. have [cKK cKuKu] := (abelianS sKA cAA, abelianS sKuA cAuAu). have [pK pKu] := (pgroupS sKA pA, pgroupS sKuA pAu). have nsUK: U <| K := normalS sUK sKA nsUA; have [_ nUK] := andP nsUK. have nKX: X \subset 'N(K). by rewrite -(quotientSGK nUX) ?normsG ?quotient_normG // -defKu. pose K1 := 'Mho^1(K); have nsK1K: K1 <| K := Mho_normal 1 K. have nXKb: X / K1 \subset 'N(K / K1) by apply: quotient_norms. pose K'u := \big[dprod/1]_(Bu in S :\ Ku) Bu. have{S_Ku} defAu_K: K / U \x K'u = A / U by rewrite -defKu -big_setD1. have [[_ Pu _ defK'u]] := dprodP defAu_K; rewrite defK'u => mulKPu _ tiKPu. have [_ sPuA] := mulG_sub mulKPu. have [P defPu sUP sPA] := inv_quotientS nsUA sPuA. have{simS defK'u} nPX: X \subset 'N(P). rewrite -(quotientSGK nUX) ?normsG // quotient_normG ?(normalS sUP sPA) //. rewrite -defPu -(bigdprodWY defK'u) norms_gen ?norms_bigcup //. by apply/bigcapsP=> Bu; case/setD1P=> _; case/simS. have abelKb: p.-abelem (K / K1). by rewrite -[K1](Phi_Mho pK) ?Phi_quotient_abelem. have p'Xb: p^'.-group (X / K1) := quotient_pgroup _ p'X. have sUKb: U / K1 \subset K / K1 := quotientS _ sUK. have nUXb: X / K1 \subset 'N(U / K1) := quotient_norms _ nUX. have tiUK1: U :&: K1 = 1. apply/trivgP; apply/subsetP=> xp; case/setIP=> Uxp K1xp. have{K1xp} [x Kx def_xp]: exists2 x, x \in K & xp = x ^+ p. by apply/imsetP; rewrite -(MhoEabelian 1). suffices A1x: x \in 'Ohm_1(A). by rewrite def_xp inE; case/abelemP: abelA1 => // _ ->. have nUx: x \in 'N(U) := subsetP nUK x Kx. rewrite -sub1set -(quotientSGK _ sUA1) ?quotient_set1 ?sub1set //. apply: (subsetP (quotientS U (subset_trans (MhoS n sKA) sAnA1))). rewrite quotientE morphim_Mho //= -quotientE -defKu. have ->: 'Mho^n(Ku) = 'Ohm_1(Ku). by rewrite (homocyclic_Ohm_Mho 1 pKu) // (eqP eKu) pfactorK ?subn1. rewrite (OhmE 1 pKu) ?mem_gen // !inE defKu mem_quotient //=. by rewrite -morphX //= -def_xp coset_id. have [Db defKb nDXb] := Maschke_abelem abelKb p'Xb sUKb nXKb nUXb. have [_ mulUDb _ tiUDb] := dprodP defKb; have [_ sDKb] := mulG_sub mulUDb. have [D defDb sK1D sDK] := inv_quotientS (Mho_normal 1 K) sDKb. have nK1X: X \subset 'N(K1) := gFnorm_trans _ nKX. have [cDU [sK1K nK1K]] := (centSS sUK sDK cKK, andP nsK1K). have nDX: X \subset 'N(D). rewrite -(quotientSGK nK1X) ?normsG // quotient_normG ?(normalS _ sDK) //. by rewrite -defDb. have{mulUDb} mulUD: U * D = K. rewrite (centC cDU) -(mulSGid sK1D) -mulgA -(centC cDU). rewrite -quotientK ?quotientMr ?(subset_trans _ nK1K) ?mul_subG // -defDb. by rewrite mulUDb quotientGK. have cKP: P \subset 'C(K) := centSS sPA sKA cAA. have mulKP: K * P = A. rewrite -(mulSGid sUK) -mulgA -(quotientGK nsUA) -mulKPu defPu. by rewrite -quotientK ?quotientMr ?mul_subG ?(subset_trans _ nUA). have defKP: K :&: P = U. apply/eqP; rewrite eqEsubset subsetI sUK sUP !andbT. by rewrite -quotient_sub1 ?subIset ?nUK // -tiKPu defPu quotientI. have tiUD: U :&: D = 1. apply/trivgP; rewrite -tiUK1 subsetI subsetIl. rewrite -quotient_sub1; last by rewrite subIset ?(subset_trans sUK). by rewrite -tiUDb defDb quotientI. have tiDP: D :&: P = 1 by rewrite -(setIidPl sDK) -setIA defKP setIC. have mulDP: D * P = A by rewrite -(mulSGid sUP) mulgA -(centC cDU) mulUD. have sDA := subset_trans sDK sKA. have defA: D \x P = A by rewrite dprodE // (centSS sPA sDA). have ntD: D :!=: 1. apply: contraNneq ntA => D1; rewrite trivg_exponent eA -(eqP eKu). rewrite -trivg_exponent -subG1 -tiKPu defKu subsetIidl defPu quotientS //. by rewrite -(mul1g P) -D1 mulDP. have ltPm: #|P| < m. by rewrite (leq_trans _ leAm) // -(dprod_card defA) ltn_Pmull ?cardG_gt1. have [cPP pP] := (abelianS sPA cAA, pgroupS sPA pA). have{S defAu K'u defAu_K} [S defP simS] := IHm _ _ _ ltPm cPP pP p'X nPX. exists (D |: S) => [ | {defP}B]. rewrite big_setU1 ?defP //=; apply: contra ntD => S_D. by rewrite -subG1 -tiDP subsetIidl -(bigdprodWY defP) sub_gen ?(bigcup_max D). case/setU1P=> [-> {B S simS} | ]; last exact: simS. have [[pD cDD] nUD] := (pgroupS sDA pA, abelianS sDA cAA, subset_trans sDA nUA). have isoD: D \isog Ku by rewrite defKu -mulUD quotientMidl quotient_isog. rewrite {isoD}(isog_homocyclic isoD); split=> //. have nPhiDX: X \subset 'N('Phi(D)) := gFnorm_trans _ nDX. have [f [injf im_f act_f]]: exists f : {morphism D / 'Phi(D) >-> coset_of 'Phi(Ku)}, [/\ 'injm f, f @* (D / 'Phi(D)) = Ku / 'Phi(Ku) & {in D / 'Phi(D) & X, morph_act 'Q 'Q f (coset U)}]. - have [/= injf im_f] := isomP (quotient_isom nUD tiUD). set f := restrm nUD (coset U) in injf im_f. rewrite -quotientMidl mulUD -defKu in im_f. have fPhiD: f @* 'Phi(D) = 'Phi(Ku) by rewrite -im_f (morphim_Phi _ pD). rewrite -['Phi(Ku)]/(gval 'Phi(Ku)%G) -(group_inj fPhiD). exists (quotm_morphism [morphism of f] (Phi_normal _)). rewrite (injm_quotm _ injf) morphim_quotm /= -/f im_f. split=> // yb x; case/morphimP=> y Ny Dy ->{yb} Xx. have [nPhiDx nUx] := (subsetP nPhiDX x Xx, subsetP nUX x Xx). have Dyx: y ^ x \in D by rewrite memJ_norm // (subsetP nDX). rewrite quotmE // !qactE ?qact_domE ?subsetT ?astabsJ ?quotmE //=. - by congr (coset _ _); rewrite /f /restrm morphJ // (subsetP nUD). - by rewrite (subsetP (morphim_norm _ _)) ?mem_morphim. rewrite morphim_restrm (setIidPr (Phi_sub _)). by rewrite (subsetP (morphim_norm _ _)) ?mem_quotient. apply/mingroupP; split=> [|Y /andP[ntY actsXY] sYD]. rewrite -subG1 quotient_sub1 ?gFnorm //. by rewrite proper_subn ?Phi_proper // actsQ. have{minKu} [_ minKu] := mingroupP minKu. apply: (injm_morphim_inj injf); rewrite // im_f. apply: minKu; last by rewrite /= -im_f morphimS. rewrite morphim_injm_eq1 // ntY. apply/subsetP=> _ /morphimP[x Nx Xx ->]. rewrite 2!inE /= qact_domE ?subsetT // astabsJ. rewrite (subsetP (gFnorm_trans _ nKuX)) ?mem_quotient //=. apply/subsetP=> _ /morphimP[y Dy Yy ->]. by rewrite inE /= -act_f // morphimEsub // imset_f // (acts_act actsXY). Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action gfunctor commutator) mathcomp(gproduct zmodp cyclic center pgroup gseries nilpotent sylow) mathcomp(finalg finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)