proposition: Proposition Ptype_structure M K (Ms := M`_\sigma) (Kstar := 'C_Ms(K)) : M \in 'M_'P -> \kappa(M).-Hall(M) K -> [/\ exists2 U : {group gT}, kappa_complement M U K /\ Ms ><| (U ><| K) = M & [/\ abelian U, semiprime Ms K & semiregular U K], K \x Kstar = 'N_M(K) /\ {in 'E^1(K), forall X, 'N_M(X) = 'N_M(K) /\ {in 'M('N(X)), forall Mstar, X \subset Mstar`_\sigma}}, Kstar != 1 /\ {in 'E^1(Kstar), forall X, 'M('C(X)) = [set M]}, [/\ {in ~: M, forall g, Kstar :&: M :^ g = 1} /\ {in M :\: 'N_M(K), forall g, K :&: K :^ g = 1}, {in \pi(Kstar), forall p S, p.-Sylow(M) S -> 'M(S) = [set M] /\ ~~ (S \subset Kstar)} & forall Y, \sigma(M).-group Y -> Y :&: Kstar != 1 -> Y \subset Ms] & M \in 'M_'P2 -> [/\ \sigma(M) =i \beta(M), prime #|K|, nilpotent Ms & normedTI Ms^# G M]].
proof: Proof. move: @Kstar => Ks PmaxM hallK; have [maxM notFmaxM] := setDP PmaxM. have sMs: \sigma(M).-group M`_\sigma := pcore_pgroup _ M. have{notFmaxM} ntK: K :!=: 1 by rewrite (trivg_kappa maxM). have [sKM kK _] := and3P hallK; have s'K := sub_pgroup (@kappa_sigma' M) kK. have solM := mmax_sol maxM; have [E hallE sKE] := Hall_superset solM sKM s'K. have [[sEM s'E _] [_ [E3 hallE3]]] := (and3P hallE, ex_tau13_compl hallE). have [F1 hallF1] := Hall_exists \tau1(M) (solvableS sKM solM). have [[sF1K t1F1 _] solE] := (and3P hallF1, sigma_compl_sol hallE). have [E1 hallE1 sFE1] := Hall_superset solE (subset_trans sF1K sKE) t1F1. have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have [[_ nsE3E] _ [cycE1 _] [defEl defE] _] := sigma_compl_context maxM complEi. have [sE1E t1E1 _] := and3P hallE1; have sE1M := subset_trans sE1E sEM. have [sE3E t3E3 _] := and3P hallE3; have sE3M := subset_trans sE3E sEM. set part_a := exists2 U, _ & _; pose b1_hyp := {in 'E^1(K), forall X, X <| K}. have [have_a nK1K ntE1 sE1K]: [/\ part_a, b1_hyp, E1 :!=: 1 & E1 \subset K]. have [t1K | not_t1K] := boolP (\tau1(M).-group K). have sKE1: K \subset E1 by rewrite (sub_pHall hallF1 t1K). have prE1 := tau1_primact_Msigma maxM hallE hallE1. have st1k: {subset \tau1(M) <= \kappa(M)}. move=> p t1p; rewrite unlock !(t1p, inE). have [X]: exists X, X \in 'E_p^1(E1). apply/p_rank_geP; rewrite p_rank_gt0 /= (card_Hall hallE1). by rewrite pi_of_part // inE /= (partition_pi_sigma_compl maxM) ?t1p. rewrite -(setIidPr sE1M) pnElemI -setIdE => /setIdP[EpX sXE1]. pose q := pdiv #|K|; have piKq: q \in \pi(K) by rewrite pi_pdiv cardG_gt1. have /p_rank_geP[Y]: 0 < 'r_q(K) by rewrite p_rank_gt0. rewrite -(setIidPr sKM) pnElemI -setIdE => /setIdP[EqY sYK]. have ntCMsY := kappa_nonregular (pnatPpi kK piKq) EqY. have [ntY sYE1] := (nt_pnElem EqY isT, subset_trans sYK sKE1). apply/exists_inP; exists X; rewrite ?(subG1_contra _ ntCMsY) //=. by rewrite (cent_semiprime prE1 sYE1 ntY) ?setIS ?centS. have defK := sub_pHall hallK (sub_pgroup st1k t1E1) sKE1 sE1M. split=> [|X||]; rewrite ?defK //; last first. rewrite -defK; case/nElemP=> p /pnElemP[sXE1 _ _]. by rewrite char_normal // sub_cyclic_char. have [[U _ defU _] _ _ _] := sdprodP defE; rewrite defU in defE. have [nsUE _ mulUE1 nUE1 _] := sdprod_context defE. have [[_ V _ defV] _] := sdprodP defEl; rewrite defV. have [_ <- nE21 _] := sdprodP defV => /mulGsubP[nE32 nE31] _. have regUK: semiregular U K. move=> y /setD1P[]; rewrite -cycle_subG -cent_cycle -order_gt1. rewrite -pi_pdiv; move: (pdiv _) => p pi_y_p Ky. have piKp := piSg Ky pi_y_p; have t1p := pnatPpi t1K piKp. move: pi_y_p; rewrite -p_rank_gt0 => /p_rank_geP[Y] /=. rewrite -{1}(setIidPr (subset_trans Ky sKE)) pnElemI -setIdE. case/setIdP=> EpY sYy; have EpMY := subsetP (pnElemS _ _ sEM) Y EpY. apply: contraNeq (kappa_nonregular (pnatPpi kK piKp) EpMY). move/(subG1_contra (setIS U (centS sYy))). have{y sYy Ky} sYE1 := subset_trans sYy (subset_trans Ky sKE1). have ntY: Y :!=: 1 by apply: (nt_pnElem EpY). rewrite -subG1 /=; have [_ <- _ tiE32] := sdprodP defU. rewrite -subcent_TImulg ?subsetI ?(subset_trans sYE1) // mulG_subG. rewrite !subG1 /= => /nandP[nregE3Y | nregE2Y]. have pr13 := cent_semiprime (tau13_primact_Msigma maxM complEi _). rewrite pr13 ?(subset_trans sYE1) ?joing_subr //; last first. by move/cent_semiregular=> regE31; rewrite regE31 ?eqxx in nregE3Y. pose q := pdiv #|'C_E3(Y)|. have piE3q: q \in \pi(E3). by rewrite (piSg (subsetIl E3 'C(Y))) // pi_pdiv cardG_gt1. have /p_rank_geP[X]: 0 < 'r_q(M :&: E3). by rewrite (setIidPr sE3M) p_rank_gt0. rewrite pnElemI -setIdE => /setIdP[EqX sXE3]. rewrite -subG1 -(_ : 'C_Ms(X) = 1) ?setIS ?centS //. by rewrite (subset_trans sXE3) ?joing_subl. apply: contraTeq (pnatPpi t3E3 piE3q) => nregMsX; apply: tau3'1. suffices kq: q \in \kappa(M). rewrite (pnatPpi t1K) //= (card_Hall hallK) pi_of_part //. by rewrite inE /= kappa_pi. rewrite unlock 2!inE /= (pnatPpi t3E3 piE3q) orbT /=. by apply/exists_inP; exists X. pose q := pdiv #|'C_E2(Y)|; have [sE2E t2E2 _] := and3P hallE2. have piCE2Yq: q \in \pi('C_E2(Y)) by rewrite pi_pdiv cardG_gt1. have [X]: exists X, X \in 'E_q^1(E :&: 'C_E2(Y)). by apply/p_rank_geP; rewrite /= setIA (setIidPr sE2E) p_rank_gt0. rewrite pnElemI -setIdE => /setIdP[EqX sXcE2Y]. have t2q:= pnatPpi t2E2 (piSg (subsetIl _ _) piCE2Yq). have [A Eq2A _] := ex_tau2Elem hallE t2q. have [[_ defEq1] _ _ _] := tau2_compl_context maxM hallE t2q Eq2A. rewrite (tau12_regular maxM hallE t1p EpY t2q Eq2A) //. rewrite (subG1_contra _ (nt_pnElem EqX _)) // subsetI. rewrite defEq1 in EqX; case/pnElemP: EqX => -> _ _. by rewrite (subset_trans sXcE2Y) ?subsetIr. have [defM [sUE _]] := (sdprod_sigma maxM hallE, andP nsUE). have hallU: \sigma_kappa(M)^'.-Hall(M) U. suffices: [predI \sigma(M)^' & \kappa(M)^'].-Hall(M) U. by apply: etrans; apply: eq_pHall=> p; rewrite inE /= negb_or. apply: subHall_Hall hallE _ _ => [p|]; first by case/andP. rewrite pHallE partnI (part_pnat_id s'E) -pHallE. have hallK_E: \kappa(M).-Hall(E) K := pHall_subl sKE sEM hallK. by apply/(sdprod_normal_pHallP nsUE hallK_E); rewrite -defK. exists U; [rewrite -{2}defK defE | rewrite -{1}defK]; split=> //. by split; rewrite // -defK mulUE1 groupP. apply: abelianS (der_mmax_compl_abelian maxM hallE). rewrite -(coprime_cent_prod nUE1) ?(solvableS sUE) //. by rewrite {2}defK (cent_semiregular regUK) // mulg1 commgSS. by rewrite (coprime_sdprod_Hall_r defE); apply: pHall_Hall hallE1. move: not_t1K; rewrite negb_and cardG_gt0 => /allPn[p piKp t1'p]. have kp := pnatPpi kK piKp; have t3p := kappa_tau13 kp. rewrite [p \in _](negPf t1'p) /= in t3p. have [X]: exists X, X \in 'E_p^1(K) by apply/p_rank_geP; rewrite p_rank_gt0. rewrite -{1}(setIidPr sKM) pnElemI -setIdE => /setIdP[EpX sXK]. have sXE3: X \subset E3. rewrite (sub_normal_Hall hallE3) ?(subset_trans sXK) ?(pi_pgroup _ t3p) //. by case/pnElemP: EpX => _ /andP[]. have [nregX ntX] := (kappa_nonregular kp EpX, nt_pnElem EpX isT). have [regE3|ntE1 {}defE prE nE1_E] := tau13_nonregular maxM complEi. by case/eqP: nregX; rewrite (cent_semiregular regE3). have defK: E :=: K. apply: (sub_pHall hallK _ sKE sEM); apply/pgroupP=> q q_pr q_dv_E. have{q_dv_E} piEq: q \in \pi(E) by rewrite mem_primes q_pr cardG_gt0. rewrite unlock; apply/andP; split=> /=. apply: pnatPpi piEq; rewrite -pgroupE -(sdprodW defE). rewrite pgroupM (sub_pgroup _ t3E3) => [|r t3r]; last by apply/orP; right. by rewrite (sub_pgroup _ t1E1) // => r t1r; apply/orP; left. have:= piEq; rewrite -p_rank_gt0 => /p_rank_geP[Y]. rewrite -{1}(setIidPr sEM) pnElemI -setIdE => /setIdP[EqY sYE]. rewrite (cent_semiprime prE) ?(subset_trans sXK) // in nregX. apply/exists_inP; exists Y => //; apply: subG1_contra nregX. by rewrite setIS ?centS. have defM := sdprod_sigma maxM hallE. rewrite /b1_hyp -defK; split=> //; exists 1%G; last first. by split; [apply: abelian1 | rewrite -defK | apply: semiregular1l]. rewrite sdprod1g; do 2?split=> //; rewrite ?mul1g ?groupP -?defK //. rewrite pHallE sub1G cards1 eq_sym partG_eq1 pgroupNK /=. have{defM} [_ defM _ _] := sdprodP defM; rewrite -{2}defM defK pgroupM. rewrite (sub_pgroup _ sMs) => [|r sr]; last by apply/orP; left. by rewrite (sub_pgroup _ kK) // => r kr; apply/orP; right. set part_b := _ /\ _; set part_c := _ /\ _; set part_d := _ /\ _. have [U [complUK defM] [cUU prMsK regUK]] := have_a. have [hallU _ _] := complUK; have [sUM sk'U _] := and3P hallU. have have_b: part_b. have coMsU: coprime #|Ms| #|U|. by rewrite (pnat_coprime sMs (sub_pgroup _ sk'U)) // => p; case/norP. have{defM} [[_ F _ defF]] := sdprodP defM; rewrite defF. have [_ <- nUK _] := sdprodP defF; rewrite mulgA mulG_subG => defM. case/andP=> nMsU nMsK _. have coMsU_K: coprime #|Ms <*> U| #|K|. rewrite norm_joinEr // (p'nat_coprime _ kK) // -pgroupE. rewrite pgroupM // (sub_pgroup _ sMs) => [|r]; last first. by apply: contraL; apply: kappa_sigma'. by apply: sub_pgroup _ sk'U => r /norP[]. have defNK X: X <| K -> X :!=: 1 -> 'N_M(X) = Ks * K. case/andP=> sXK nXK ntX; rewrite -defM -(norm_joinEr nMsU). rewrite setIC -group_modr // setIC. rewrite coprime_norm_cent ?(subset_trans sXK) ?normsY //; last first. by rewrite (coprimegS sXK). rewrite /= norm_joinEr -?subcent_TImulg ?(coprime_TIg coMsU) //; last first. by rewrite subsetI !(subset_trans sXK). by rewrite (cent_semiregular regUK) // mulg1 (cent_semiprime prMsK). rewrite /part_b dprodE ?subsetIr //; last first. rewrite setICA setIA (coprime_TIg (coprimeSg _ coMsU_K)) ?setI1g //. by rewrite joing_subl. rewrite -centC ?subsetIr // defNK //; split=> // X Eq1X. have [q EqX] := nElemP Eq1X; have ntX := nt_pnElem EqX isT. have:= EqX; rewrite -{1}(setIidPr sKE) pnElemI -setIdE. case/setIdP=> EqEX sXK; split; first by rewrite defNK ?nK1K. have [_ abelX dimX] := pnElemP EqX; have [qX _] := andP abelX. have kq: q \in \kappa(M). by rewrite (pnatPpi kK (piSg sXK _)) // -p_rank_gt0 p_rank_abelem ?dimX. have nregX := kappa_nonregular kq (subsetP (pnElemS _ _ sEM) _ EqEX). have sq := tau13_nonregular_sigma maxM hallE EqEX (kappa_tau13 kq) nregX. move=> H maxNH; have [maxH sNXH] := setIdP maxNH. rewrite (sub_Hall_pcore (Msigma_Hall maxH)) ?(subset_trans (normG X)) //. exact: pi_pgroup qX (sq H maxNH). have have_c: part_c. pose p := pdiv #|E1|; have piE1p: p \in \pi(E1) by rewrite pi_pdiv cardG_gt1. have:= piE1p; rewrite -p_rank_gt0 => /p_rank_geP[Y]. rewrite -(setIidPr sE1M) pnElemI -setIdE => /setIdP[EpY sYE1]. have [sYK ntY] := (subset_trans sYE1 sE1K, nt_pnElem EpY isT). split=> [|X /nElemP[q]]. rewrite /Ks -(cent_semiprime prMsK sYK) //. exact: kappa_nonregular (pnatPpi kK (piSg sE1K piE1p)) EpY. rewrite /= -(cent_semiprime prMsK sYK) // => EqX. by have [] := cent_cent_Msigma_tau1_uniq maxM hallE hallE1 sYE1 ntY EqX. have [[defNK defK1] [_ uniqKs]] := (have_b, have_c). have have_d: part_d. split=> g. rewrite inE; apply: contraNeq; rewrite -rank_gt0. case/rank_geP=> X; rewrite nElemI -setIdE -groupV => /setIdP[EpX sXMg]. have [_ sCXMs] := mem_uniq_mmax (uniqKs _ EpX). case/nElemP: EpX => p /pnElemP[/subsetIP[sXMs _] abelX dimX]. have [[pX _] sXM] := (andP abelX, subset_trans sXMs (pcore_sub _ _)). have piXp: p \in \pi(X) by rewrite -p_rank_gt0 p_rank_abelem ?dimX. have sp := pnatPpi sMs (piSg sXMs piXp). have [def_g _ _] := sigma_group_trans maxM sp pX. have [|c cXc [m Mm ->]] := def_g g^-1 sXM; first by rewrite sub_conjgV. by rewrite groupM // (subsetP sCXMs). case/setDP=> Mg; apply: contraNeq; rewrite -rank_gt0 /=. case/rank_geP=> X; rewrite nElemI -setIdE => /setIdP[EpX sXKg]. have [<- _] := defK1 X EpX; rewrite 2!inE Mg /=. have{EpX} [p EpX] := nElemP EpX; have [_ abelX dimX] := pnElemP EpX. have defKp1: {in 'E_p^1(K), forall Y, 'Ohm_1('O_p(K)) = Y}. move=> Y EpY; have E1K_Y: Y \in 'E^1(K) by apply/nElemP; exists p. have piKp: p \in \pi(K) by rewrite -p_rank_gt0; apply/p_rank_geP; exists Y. have [pKp sKpK] := (pcore_pgroup p K, pcore_sub p K). have cycKp: cyclic 'O_p(K). rewrite (odd_pgroup_rank1_cyclic pKp) ?mFT_odd //. by rewrite -(rank_kappa (pnatPpi kK piKp)) p_rankS ?(subset_trans sKpK). have [sYK abelY oY] := pnElemPcard EpY; have [pY _] := andP abelY. have sYKp: Y \subset 'O_p(K) by rewrite pcore_max ?nK1K. apply/eqP; rewrite eq_sym eqEcard -{1}(Ohm1_id abelY) OhmS //= oY. rewrite (Ohm1_cyclic_pgroup_prime cycKp pKp) ?(subG1_contra sYKp) //=. exact: nt_pnElem EpY _. rewrite sub_conjg -[X :^ _]defKp1 ?(defKp1 X) //. by rewrite !inE sub_conjgV sXKg abelemJ abelX cardJg dimX. split=> {part_a part_b part_c have_a have_b have_c}//; first split=> //. - move=> q; rewrite /Ks -(cent_semiprime prMsK sE1K ntE1) => picMsE1q. have sq := pnatPpi (pcore_pgroup _ M) (piSg (subsetIl _ _) picMsE1q). move: picMsE1q; rewrite -p_rank_gt0; case/p_rank_geP=> y EqY S sylS. have [sSM qS _] := and3P sylS. have sSMs: S \subset M`_\sigma. by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup qS). have sylS_Ms: q.-Sylow(M`_\sigma) S := pHall_subl sSMs (pcore_sub _ M) sylS. have [_]:= cent_cent_Msigma_tau1_uniq maxM hallE hallE1 (subxx _) ntE1 EqY. move/(_ S sylS_Ms) => uniqS; split=> //; rewrite subsetI sSMs /=. pose p := pdiv #|E1|; have piE1p: p \in \pi(E1) by rewrite pi_pdiv cardG_gt1. have [s'p _] := andP (pnatPpi t1E1 piE1p). have [P sylP] := Sylow_exists p E1; have [sPE1 pP _] := and3P sylP. apply: contra (s'p) => cE1S; apply/exists_inP; exists P. exact: subHall_Sylow s'p (subHall_Sylow hallE1 (pnatPpi t1E1 piE1p) sylP). apply: (sub_uniq_mmax uniqS); first by rewrite cents_norm // (centsS sPE1). apply: mFT_norm_proper (mFT_pgroup_proper pP). by rewrite -rank_gt0 (rank_Sylow sylP) p_rank_gt0. - move=> Y sY ntYKs; have ntY: Y :!=:1 := subG1_contra (subsetIl _ _) ntYKs. have [[x sYxMs] _] := sigma_Jsub maxM sY ntY; rewrite sub_conjg in sYxMs. suffices Mx': x^-1 \in M by rewrite (normsP _ _ Mx') ?gFnorm in sYxMs. rewrite -(setCK M) inE; apply: contra ntYKs => M'x'. rewrite setIC -(setIidPr sYxMs) -/Ms -[Ms](setIidPr (pcore_sub _ _)). by rewrite conjIg !setIA; have [-> // _] := have_d; rewrite !setI1g. rewrite inE PmaxM andbT -(trivg_kappa_compl maxM complUK) => ntU. have [regMsU nilMs]: 'C_Ms(U) = 1 /\ nilpotent Ms. pose p := pdiv #|U|; have piUp: p \in \pi(U) by rewrite pi_pdiv cardG_gt1. have sk'p := pnatPpi sk'U piUp. have [S sylS] := Sylow_exists p U; have [sSU _] := andP sylS. have sylS_M := subHall_Sylow hallU sk'p sylS. have [|_ _ regMsS1 nilMs] := sigma'_kappa'_facts maxM sylS_M. by rewrite -negb_or (piSg sUM). by split=> //; apply/trivgP; rewrite -regMsS1 setIS ?centS ?gFsub_trans. have [[_ F _ defF] _ _ _] := sdprodP defM; rewrite defF in defM. have hallMs: \sigma(M).-Hall(M) Ms by apply: Msigma_Hall. have hallF: \sigma(M)^'.-Hall(M) F by apply/(sdprod_Hall_pcoreP hallMs). have frF: [Frobenius F = U ><| K] by apply/Frobenius_semiregularP. have ntMs: Ms != 1 by apply: Msigma_neq1. have prK: prime #|K|. have [solF [_ _ nMsF _]] := (sigma_compl_sol hallF, sdprodP defM). have solMs: solvable Ms := solvableS (pcore_sub _ _) (mmax_sol maxM). have coMsF: coprime #|Ms| #|F|. by rewrite (coprime_sdprod_Hall_r defM) (pHall_Hall hallF). by have [] := Frobenius_primact frF solF nMsF solMs ntMs coMsF prMsK. have eq_sb: \sigma(M) =i \beta(M). suffices bMs: \beta(M).-group Ms. move=> p; apply/idP/idP=> [sp|]; last exact: beta_sub_sigma. rewrite (pnatPpi bMs) //= (card_Hall (Msigma_Hall maxM)) pi_of_part //. by rewrite inE /= sigma_sub_pi. have [H hallH cHF'] := der_compl_cent_beta' maxM hallF. rewrite -pgroupNK -partG_eq1 -(card_Hall hallH) -trivg_card1 -subG1. rewrite -regMsU subsetI (pHall_sub hallH) centsC (subset_trans _ cHF') //. have [solU [_ mulUK nUK _]] := (abelian_sol cUU, sdprodP defF). have coUK: coprime #|U| #|K|. rewrite (p'nat_coprime (sub_pgroup _ (pHall_pgroup hallU)) kK) // => p. by case/norP. rewrite -(coprime_cent_prod nUK) // (cent_semiregular regUK) // mulg1. by rewrite -mulUK commgSS ?mulG_subl ?mulG_subr. split=> //; apply/normedTI_P; rewrite setD_eq0 subG1 setTI normD1 gFnorm. split=> // g _; rewrite -setI_eq0 conjD1g -setDIl setD_eq0 subG1 /= -/Ms. have [_ _ b'MsMg] := sigma_compl_embedding maxM hallE. apply: contraR => notMg; have{b'MsMg notMg} [_ b'MsMg _] := b'MsMg g notMg. rewrite -{2}(setIidPr (pHall_sub hallMs)) conjIg setIA coprime_TIg // cardJg. by apply: p'nat_coprime b'MsMg _; rewrite -(eq_pnat _ eq_sb). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)