proposition: Theorem nonabelian_tau2 M E p A P0 (Ms := M`_\sigma) (A0 := 'C_A(Ms)%G) : M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) -> p.-group P0 -> ~~ abelian P0 -> [/\ \tau2(M) =i (p : nat_pred), #|A0| = p /\ Ms \x A0 = 'F(M), forall X, X \in 'E_p^1(E) :\ A0 -> 'C_Ms(X) = 1 /\ ~~ ('C(X) \subset M) & exists2 E0 : {group gT}, A0 ><| E0 = E & forall x, x \in Ms^# -> {subset \pi('C_E0[x]) <= \tau1(M)}].
proof: Proof. rewrite {}/A0 => maxM hallE t2Mp Ep2A pP0 not_cP0P0 /=. have p_pr := pnElem_prime Ep2A. have [sEM sM'E _] := and3P hallE; have [sM'p _] := andP t2Mp. have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have Ep2A_M: A \in 'E_p^2(M) by rewrite (subsetP (pnElemS _ _ sEM)). have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have [regE3 _ sAE2] := tau2_regular maxM complEi t2Mp Ep2A. have [P sylP sAP] := Sylow_superset sAE2 pA; have [sPE2 pP _] := and3P sylP. have [S /= sylS sPS] := Sylow_superset (subsetT P) pP. have pS := pHall_pgroup sylS; have sAS := subset_trans sAP sPS. have sylP_E: p.-Sylow(E) P := subHall_Sylow hallE2 t2Mp sylP. have sylP_M: p.-Sylow(M) P := subHall_Sylow hallE sM'p sylP_E. have [syl_p_M _ regA _ _] := tau2_context maxM t2Mp Ep2A_M. have{syl_p_M} cPP: abelian P by case: (syl_p_M P). have{P0 pP0 not_cP0P0} not_cSS: ~~ abelian S. have [x _ sP0Sx] := Sylow_subJ sylS (subsetT P0) pP0. by apply: contra not_cP0P0 => cSS; rewrite (abelianS sP0Sx) ?abelianJ. have [defP | ltPS] := eqVproper sPS; first by rewrite -defP cPP in not_cSS. have [[nsAE defEp] [sCAE _ _] nregA _] := tau2_compl_context maxM hallE t2Mp Ep2A. have defCSA: 'C_S(A) = P. apply: (sub_pHall sylP_E (pgroupS (subsetIl _ _) pS)). by rewrite subsetI sPS (sub_abelian_cent2 cPP). by rewrite subIset // sCAE orbT. have max2A: A \in 'E_p^2(G) :&: 'E*_p(G). by rewrite 3!inE subsetT abelA dimA; case: (tau2_not_beta maxM t2Mp) => _ ->. have def_t2: \tau2(M) =i (p : nat_pred). move=> q; apply/idP/idP=> [t2Mq |]; last by move/eqnP->. apply: contraLR (proper_card ltPS); rewrite !inE /= eq_sym -leqNgt => q'p. apply: wlog_neg => p'q; have [B EqB] := p_rank_witness q E. have{EqB} Eq2B: B \in 'E_q^2(E). by move: t2Mq; rewrite (tau2E hallE) => /andP[_ /eqP <-]. have [sBE abelB dimB]:= pnElemP Eq2B; have [qB _] := andP abelB. have coBA: coprime #|B| #|A| by apply: pnat_coprime qB (pi_pnat pA _). have [[nsBE _] [sCBE _ _] _ _] := tau2_compl_context maxM hallE t2Mq Eq2B. have nBA: A \subset 'N(B) by rewrite (subset_trans sAE) ?normal_norm. have cAB: B \subset 'C(A). rewrite (sameP commG1P trivgP) -(coprime_TIg coBA) subsetI commg_subl nBA. by rewrite commg_subr (subset_trans sBE) ?normal_norm. have{cAB} qCA: q %| #|'C(A)|. by apply: dvdn_trans (cardSg cAB); rewrite (card_pnElem Eq2B) dvdn_mull. have [Q maxQ sBQ] := max_normed_exists qB nBA. have nnQ: q.-narrow Q. apply/implyP=> _; apply/set0Pn; exists B. rewrite 3!inE sBQ abelB dimB (subsetP (pmaxElemS q (subsetT Q))) //=. rewrite setIC 2!inE sBQ; case: (tau2_not_beta maxM t2Mq) => _ -> //. by rewrite (subsetP (pnElemS _ _ sEM)). have [P1 [sylP1 _] [_ _]] := max_normed_2Elem_signaliser q'p max2A maxQ qCA. move/(_ nnQ)=> cQP1; have sylP1_E: p.-Sylow(E) P1. apply: pHall_subl (subset_trans _ sCBE) (subsetT E) sylP1. exact: subset_trans (centS sBQ). rewrite (card_Hall sylS) -(card_Hall sylP1). by rewrite (card_Hall sylP_E) -(card_Hall sylP1_E). have coMsA: coprime #|Ms| #|A|. by apply: pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _). have defMs: <<\bigcup_(X in 'E_p^1(A)) 'C_Ms(X)>> = Ms. have ncycA: ~~ cyclic A by rewrite (abelem_cyclic abelA) dimA. have [sAM _ _] := pnElemP Ep2A_M. have{sAM} nMsA: A \subset 'N(Ms) by rewrite (subset_trans sAM) ?gFnorm. apply/eqP; rewrite eqEsubset andbC gen_subG. rewrite -{1}[Ms](coprime_abelian_gen_cent1 cAA ncycA nMsA coMsA). rewrite genS; apply/bigcupsP=> x; rewrite ?subsetIl //; case/setD1P=> ntx Ax. rewrite /= -cent_cycle (bigcup_max <[x]>%G) // p1ElemE // . by rewrite 2!inE cycle_subG Ax /= -orderE (abelem_order_p abelA). have [A0 EpA0 nregA0]: exists2 A0, A0 \in 'E_p^1(A) & 'C_Ms(A0) != 1. apply/exists_inP; rewrite -negb_forall_in. apply: contra (Msigma_neq1 maxM); move/forall_inP => regAp. rewrite -/Ms -defMs -subG1 gen_subG; apply/bigcupsP=> X EpX. by rewrite subG1 regAp. have uniqCA0: 'M('C(A0)) = [set M]. by rewrite nregA // (subsetP (pnElemS _ _ sAE)). have defSM: S :&: M = P. apply: sub_pHall (pgroupS (subsetIl S M) pS) _ (subsetIr S M) => //. by rewrite subsetI sPS (pHall_sub sylP_M). have{ltPS} not_sSM: ~~ (S \subset M). by rewrite (sameP setIidPl eqP) defSM proper_neq. have not_sA0Z: ~~ (A0 \subset 'Z(S)). apply: contra not_sSM; rewrite subsetI centsC; case/andP=> _ sS_CA0. by case/mem_uniq_mmax: uniqCA0 => _; apply: subset_trans sS_CA0. have [EpZ0 dxCSA transNSA] := basic_p2maxElem_structure max2A pS sAS not_cSS. do [set Z0 := 'Ohm_1('Z(S))%G; set EpA' := _ :\ Z0] in EpZ0 dxCSA transNSA. have sZ0Z: Z0 \subset 'Z(S) := Ohm_sub 1 _. have [sA0A _ _] := pnElemP EpA0; have sA0P := subset_trans sA0A sAP. have EpA'_A0: A0 \in EpA'. by rewrite 2!inE EpA0 andbT; apply: contraNneq not_sA0Z => ->. have{transNSA sAP not_sSM defSM} regA0' X: X \in 'E_p^1(E) :\ A0 -> 'C_Ms(X) = 1 /\ ~~ ('C(X) \subset M). - case/setD1P=> neqXA0 EpX. suffices not_sCXM: ~~ ('C(X) \subset M). split=> //; apply: contraNeq not_sCXM => nregX. by case/mem_uniq_mmax: (nregA X EpX nregX). have [sXZ | not_sXZ] := boolP (X \subset 'Z(S)). apply: contra (subset_trans _) not_sSM. by rewrite centsC (subset_trans sXZ) ?subsetIr. have EpA'_X: X \in EpA'. by rewrite 2!inE -defEp EpX andbT; apply: contraNneq not_sXZ => ->. have [g NSAg /= defX] := atransP2 transNSA EpA'_A0 EpA'_X. have{NSAg} [Sg nAg] := setIP NSAg. have neqMgM: M :^ g != M. rewrite (sameP eqP normP) (norm_mmax maxM); apply: contra neqXA0 => Mg. rewrite defX [_ == _](sameP eqP normP) (subsetP (cent_sub A0)) //. by rewrite (subsetP (centSS (subxx _) sA0P cPP)) // -defSM inE Sg. apply: contra neqMgM; rewrite defX centJ sub_conjg. by move/(eq_uniq_mmax uniqCA0) => defM; rewrite -{1}defM ?mmaxJ ?actKV. have{defMs} defA0: 'C_A(Ms) = A0. apply/eqP; rewrite eq_sym eqEcard subsetI sA0A (card_pnElem EpA0). have pCA: p.-group 'C_A(Ms) := pgroupS (subsetIl A _) pA. rewrite andbC (card_pgroup pCA) leq_exp2l ?prime_gt1 // -ltnS -dimA. rewrite properG_ltn_log //=; last first. rewrite properE subsetIl /= subsetI subxx centsC -(subxx Ms) -subsetI. by rewrite regA subG1 Msigma_neq1. rewrite centsC -defMs gen_subG (big_setD1 A0) //= subUset subsetIr /=. by apply/bigcupsP=> X; rewrite -defEp; case/regA0'=> -> _; rewrite sub1G. rewrite defA0 (group_inj defA0) (card_pnElem EpA0). have{dxCSA} [Y [cycY sZ0Y]] := dxCSA; move/(_ _ EpA'_A0)=> dxCSA. have defCP_Ms: 'C_P(Ms) = A0. move: dxCSA; rewrite defCSA => /dprodP[_ mulA0Y cA0Y tiA0Y]. rewrite -mulA0Y -group_modl /=; last by rewrite -defA0 subsetIr. rewrite setIC TI_Ohm1 ?mulg1 // setIC. have pY: p.-group Y by rewrite (pgroupS _ pP) // -mulA0Y mulG_subr. have cYY: abelian Y := cyclic_abelian cycY. have ->: 'Ohm_1(Y) = Z0. apply/eqP; rewrite eq_sym eqEcard (card_pnElem EpZ0) /= -['Ohm_1(_)]Ohm_id. rewrite OhmS // (card_pgroup (pgroupS (Ohm_sub 1 Y) pY)). rewrite leq_exp2l ?prime_gt1 -?p_rank_abelian // -rank_pgroup //. by rewrite -abelian_rank1_cyclic. rewrite prime_TIg ?(card_pnElem EpZ0) // centsC (sameP setIidPl eqP) eq_sym. case: (regA0' Z0) => [|-> _]; last exact: Msigma_neq1. by rewrite 2!inE defEp EpZ0 andbT; apply: contraNneq not_sA0Z => <-. have [sPM pA0] := (pHall_sub sylP_M, pgroupS sA0A pA). have cMsA0: A0 \subset 'C(Ms) by rewrite -defA0 subsetIr. have nsA0M: A0 <| M. have [_ defM nMsE _] := sdprodP (sdprod_sigma maxM hallE). rewrite /normal (subset_trans sA0P) // -defM mulG_subG cents_norm 1?centsC //. by rewrite -defA0 normsI ?norms_cent // normal_norm. have defFM: Ms \x A0 = 'F(M). have nilF := Fitting_nil M. rewrite dprodE ?(coprime_TIg (coprimegS sA0A coMsA)) //. have [_ /= defFM cFpp' _] := dprodP (nilpotent_pcoreC p nilF). have defFp': 'O_p^'('F(M)) = Ms. apply/eqP; rewrite eqEsubset. rewrite (sub_Hall_pcore (Msigma_Hall maxM)); last by rewrite !gFsub_trans. rewrite /pgroup (sub_in_pnat _ (pcore_pgroup _ _)) => [|q piFq]; last first. have [Q sylQ] := Sylow_exists q 'F(M); have [sQF qQ _] := and3P sylQ. have ntQ: Q :!=: 1. rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ) p_rank_gt0. by rewrite (piSg _ piFq) ?pcore_sub. have sNQM: 'N(Q) \subset M. rewrite (mmax_normal maxM) // (nilpotent_Hall_pcore nilF sylQ). by rewrite p_core_Fitting pcore_normal. apply/implyP; rewrite implyNb /= -def_t2 orbC. by rewrite (prime_class_mmax_norm maxM qQ). rewrite pcore_max ?(pi_p'group (pcore_pgroup _ _)) //. rewrite [_ <| _]andbC gFsub_trans ?gFnorm //. rewrite Fitting_max ?gFnormal ?(tau2_Msigma_nil _ t2Mp) //. rewrite p_core_Fitting defFp' centsC in defFM cFpp'. rewrite -defFM (centC cFpp'); congr (Ms * _). apply/eqP; rewrite eqEsubset pcore_max //. by rewrite -defCP_Ms subsetI cFpp' pcore_sub_Hall. split=> {defFM}//. have [[sE1E t1E1 _] t2E2] := (and3P hallE1, pHall_pgroup hallE2). have defE2: E2 :=: P by rewrite (sub_pHall sylP) // -(eq_pgroup _ def_t2) t2E2. have [[_ nsE3E] _ _ [defEr _] _] := sigma_compl_context maxM complEi. have [sE3E nE3E] := andP nsE3E; have{} nE3E := subset_trans _ nE3E. have [[_ E21 _ defE21]] := sdprodP defEr; rewrite defE21 => defE nE321 tiE321. rewrite defE2 in defE21; have{defE21} [_ defPE1 nPE1 tiPE1] := sdprodP defE21. have [P0 defP nP0E1]: exists2 P0 : {group gT}, A0 \x P0 = P & E1 \subset 'N(P0). have p'E1b: p^'.-group (E1 / 'Phi(P)). rewrite quotient_pgroup //; apply: sub_pgroup t1E1 => q /tau2'1. by rewrite inE /= def_t2. have defPhiP: 'Phi(P) = 'Phi(Y). have [_ _ cA0Y tiA0Y] := dprodP dxCSA. rewrite defCSA dprodEcp // in dxCSA. have [_ abelA0 _] := pnElemP EpA0; rewrite -trivg_Phi // in abelA0. by rewrite -(Phi_cprod pP dxCSA) (eqP abelA0) cprod1g. have abelPb := Phi_quotient_abelem pP; have sA0Pb := quotientS 'Phi(P) sA0P. have [||P0b] := Maschke_abelem abelPb p'E1b sA0Pb; rewrite ?quotient_norms //. by rewrite (subset_trans (subset_trans sE1E sEM)) ?normal_norm. case/dprodP=> _ defPb _ tiAP0b nP0E1b. have sP0Pb: P0b \subset P / 'Phi(P) by rewrite -defPb mulG_subr. have [P0 defP0b sPhiP0 sP0P] := inv_quotientS (Phi_normal P) sP0Pb. exists P0; last first. rewrite -(quotientSGK (char_norm_trans (Phi_char P) nPE1)); last first. by rewrite cents_norm ?(sub_abelian_cent2 cPP (Phi_sub P) sP0P). by rewrite quotient_normG -?defP0b ?(normalS _ _ (Phi_normal P)). rewrite dprodEY ?(sub_abelian_cent2 cPP) //. apply/eqP; rewrite eqEsubset join_subG sA0P sP0P /=. rewrite -(quotientSGK (normal_norm (Phi_normal P))) //=; last first. by rewrite sub_gen // subsetU // sPhiP0 orbT. rewrite cent_joinEr ?(sub_abelian_cent2 cPP) //. rewrite quotientMr //; last by rewrite (subset_trans sP0P) ?gFnorm. by rewrite -defP0b defPb. apply/trivgP; case/dprodP: dxCSA => _ _ _ <-. rewrite subsetI subsetIl (subset_trans _ (Phi_sub Y)) // -defPhiP. rewrite -quotient_sub1 ?subIset ?(subset_trans sA0P) ?gFnorm //. by rewrite quotientIG // -defP0b tiAP0b. have nA0E := subset_trans _ (subset_trans sEM (normal_norm nsA0M)). have{defP} [_ defAP0 _ tiAP0] := dprodP defP. have sP0P: P0 \subset P by rewrite -defAP0 mulG_subr. have sP0E := subset_trans sP0P (pHall_sub sylP_E). pose E0 := (E3 <*> (P0 <*> E1))%G. have sP0E1_E: P0 <*> E1 \subset E by rewrite join_subG sP0E. have sE0E: E0 \subset E by rewrite join_subG sE3E. have mulA0E0: A0 * E0 = E. rewrite /= (norm_joinEr (nE3E _ sP0E1_E)) mulgA -(normC (nA0E _ sE3E)). by rewrite /= -mulgA (norm_joinEr nP0E1) (mulgA A0) defAP0 defPE1. have tiA0E0: A0 :&: E0 = 1. rewrite cardMg_TI // mulA0E0 -defE /= (norm_joinEr (nE3E _ sP0E1_E)). rewrite !TI_cardMg //; last first. by apply/trivgP; rewrite -tiE321 setIS //= ?norm_joinEr // -defPE1 mulSg. rewrite mulnCA /= leq_mul // norm_joinEr //= -defPE1. rewrite !TI_cardMg //; last by apply/trivgP; rewrite -tiPE1 setSI. by rewrite mulnA -(TI_cardMg tiAP0) defAP0. have defAE0: A0 ><| E0 = E by rewrite sdprodE ?nA0E. exists E0 => // x /setD1P[ntx Ms_x] q piCE0x_q. have: q \in \pi(E) by apply: piSg piCE0x_q; rewrite subIset ?sE0E. rewrite mem_primes in piCE0x_q; case/and3P: piCE0x_q => q_pr _. case/Cauchy=> // z /setIP[E0z cxz] oz. have ntz: z != 1 by rewrite -order_gt1 oz prime_gt1. have ntCMs_z: 'C_Ms[z] != 1. apply: contraNneq ntx => reg_z; rewrite (sameP eqP set1gP) -reg_z inE Ms_x. by rewrite cent1C. rewrite (partition_pi_sigma_compl maxM hallE) def_t2. case/or3P => [-> // | pq | t3Mq]. have EpA0'_z: <[z]>%G \in 'E_p^1(E) :\ A0. rewrite p1ElemE // !inE -orderE oz (eqnP pq) eqxx cycle_subG. rewrite (subsetP sE0E) // !andbT; apply: contraNneq ntz => eqA0z. by rewrite (sameP eqP set1gP) -tiA0E0 inE -eqA0z cycle_id E0z. have [reg_z _] := regA0' _ EpA0'_z. by rewrite -cent_cycle reg_z eqxx in ntCMs_z. rewrite regE3 ?eqxx // !inE ntz /= in ntCMs_z. by rewrite (mem_normal_Hall hallE3 nsE3E) ?(subsetP sE0E) // /p_elt oz pnatE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)