proposition: Lemma tau1_mmaxI_asymmetry M Mstar p P q Q q_star Qstar : [/\ M \in 'M, Mstar \in 'M & gval Mstar \notin M :^: G] -> [/\ p \in \tau1(M), p \in \tau1(Mstar) & P \in 'E_p^1(M :&: Mstar)] -> [/\ q.-Sylow(M :&: Mstar) Q, q_star.-Sylow(M :&: Mstar) Qstar, P \subset 'N(Q) & P \subset 'N(Qstar)] -> 'C_Q(P) = 1 /\ 'C_Qstar(P) = 1 -> 'N(Q) \subset Mstar /\ 'N(Qstar) \subset M -> False.
proof: Proof. move: Mstar q_star Qstar => L u U. move=> [maxM maxL notMGL] [t1Mp t1Lp EpP] [sylQ sylU nQP nUP]. move=> [regPQ regPU] [sNQL sNUM]; rewrite setIC in sylU. have notLGM: gval M \notin L :^: G by rewrite orbit_sym. have{EpP} [ntP [sPML abelP dimP]] := (nt_pnElem EpP isT, pnElemP EpP). have{sPML} [[sPM sPL] [pP _ _]] := (subsetIP sPML, and3P abelP). have solCP: solvable 'C(P) by rewrite mFT_sol ?mFT_cent_proper. pose Qprops M q Q := [&& q.-Sylow(M) Q, q != p, q \notin \beta(M), 'C_(M`_\beta)(P) != 1 & 'C_(M`_\beta)(P <*> Q) == 1]. have{sylQ sylU} [hypQ hypU]: Qprops M q Q /\ Qprops L u U. apply/andP; apply/nandP=> not_hypQ. without loss{not_hypQ}: L u U M q Q maxM maxL notMGL notLGM t1Mp t1Lp sPM sPL sylQ sylU nQP nUP regPQ regPU sNQL sNUM / ~~ Qprops M q Q. - by move=> IH; case: not_hypQ; [apply: (IH L u U) | apply: (IH M q Q)]. case/and5P; have [_ qQ _] := and3P sylQ. have{} sylQ: q.-Sylow(M) Q. by rewrite -Sylow_subnorm -(setIidPr sNQL) setIA Sylow_subnorm. have ntQ: Q :!=: 1. by apply: contraTneq sNQL => ->; rewrite norm1 proper_subn ?mmax_proper. have p'q: q != p. apply: contraNneq ntQ => def_q; rewrite (trivg_center_pgroup qQ) //. apply/trivgP; rewrite -regPQ setIS // centS //. by rewrite (norm_sub_max_pgroup (Hall_max sylQ)) ?def_q. have EpP: P \in 'E_p^1(M) by apply/pnElemP. have [|_ [// | abM]] := cent_Malpha_reg_tau1 maxM t1Mp p'q EpP ntQ nQP regPQ. apply: contraNneq notMGL => uniqNQ. by rewrite (eq_uniq_mmax uniqNQ) ?orbit_refl. by rewrite joingC /alpha_core abM !(eq_pcore _ abM) => _ -> -> ->. have bML_CMbP: forall M L, [predU \beta(M) & \beta(L)].-group 'C_(M`_\beta)(P). move=> ? ?; apply: pgroupS (subsetIl _ _) (sub_pgroup _ (pcore_pgroup _ _)). by move=> ?; rewrite !inE => ->. have [H hallH sCMbP_H] := Hall_superset solCP (subsetIr _ _) (bML_CMbP M L). have [[s _ rFH] [cPH bH _]] := (rank_witness 'F(H), and3P hallH). have{sCMbP_H rFH cPH} piFHs: s \in \pi('F(H)). rewrite -p_rank_gt0 -rFH rank_gt0 (trivg_Fitting (solvableS cPH solCP)). by rewrite (subG1_contra sCMbP_H) //; case/and5P: hypQ. without loss{bH} bMs: L u U M q Q maxM maxL notMGL notLGM t1Mp t1Lp sPM sPL nQP nUP regPQ regPU sNQL sNUM hypQ hypU hallH / s \in \beta(M). - move=> IH; have:= pnatPpi bH (piSg (Fitting_sub H) piFHs). case/orP; [apply: IH hypQ hypU hallH | apply: IH hypU hypQ _] => //. by apply: etrans (eq_pHall _ _ _) hallH => ?; apply: orbC. without loss{bML_CMbP} sCMbP_H: H hallH piFHs / 'C_(M`_\beta)(P) \subset H. have [x cPx sCMbP_Hx] := Hall_subJ solCP hallH (subsetIr _ _) (bML_CMbP M L). by move=> IH; apply: IH sCMbP_Hx; rewrite ?pHallJ //= FittingJ cardJg. pose X := 'O_s(H); have sylX := nilpotent_pcore_Hall s (Fitting_nil H). have{piFHs sylX} ntX: X != 1. by rewrite -rank_gt0 /= -p_core_Fitting (rank_Sylow sylX) p_rank_gt0. have [[cPH bH _] [sXH nXH]] := (and3P hallH, andP (pcore_normal s H : X <| H)). have [cPX sX] := (subset_trans sXH cPH, pcore_pgroup s H : s.-group X). have{hypQ} [sylQ p'q bM'q ntCMbP] := and5P hypQ; apply: negP. apply: subG1_contra (ntX); rewrite /= centY !subsetI (subset_trans _ cPH) //=. have nsMbM : M`_\beta <| M := pcore_normal _ M; have [sMbM nMbM] := andP nsMbM. have hallMb := Mbeta_Hall maxM; have [_ bMb _] := and3P hallMb. have{ntX} sHM: H \subset M. have [g sXMg]: exists g, X \subset M :^ g. have [S sylS] := Sylow_exists s M`_\beta; have [sSMb _ _] := and3P sylS. have sylS_G := subHall_Sylow (Mbeta_Hall_G maxM) bMs sylS. have [g _ sXSg] := Sylow_subJ sylS_G (subsetT X) sX. by exists g; rewrite (subset_trans sXSg) // conjSg (subset_trans sSMb). have [t _ rFC] := rank_witness 'F('C_(M`_\beta)(P)). pose Y := 'O_t('C_(M`_\beta)(P)). have [sYC tY] := (pcore_sub t _ : Y \subset _, pcore_pgroup t _ : t.-group Y). have sYMb := subset_trans sYC (subsetIl _ _); have bMY := pgroupS sYMb bMb. have{rFC} ntY: Y != 1. rewrite -rank_gt0 /= -p_core_Fitting. rewrite (rank_Sylow (nilpotent_pcore_Hall t (Fitting_nil _))) -rFC. by rewrite rank_gt0 (trivg_Fitting (solvableS (subsetIr _ _) solCP)). have bMt: t \in \beta(M). by rewrite (pnatPpi bMY) // -p_rank_gt0 -rank_pgroup ?rank_gt0. have sHMg: H \subset M :^ g. rewrite (subset_trans nXH) // beta_norm_sub_mmax ?mmaxJ // /psubgroup sXMg. by rewrite (pi_pgroup sX) 1?betaJ. have sYMg: Y \subset M :^ g := subset_trans (subset_trans sYC sCMbP_H) sHMg. have sNY_M: 'N(Y) \subset M. by rewrite beta_norm_sub_mmax // /psubgroup (subset_trans sYMb). have [_ trCY _] := sigma_group_trans maxM (beta_sub_sigma maxM bMt) tY. have [|| h cYh /= defMg] := (atransP2 trCY) M (M :^ g). - by rewrite inE orbit_refl (subset_trans (normG _) sNY_M). - by rewrite inE mem_orbit ?in_setT. by rewrite defMg conjGid // (subsetP sNY_M) ?(subsetP (cent_sub _)) in sHMg. have sXMb: X \subset M`_\beta. by rewrite (sub_Hall_pcore hallMb) ?(subset_trans sXH sHM) ?(pi_pgroup sX). rewrite sXMb (sameP commG1P eqP) /= -/X -subG1. have [sQL [sQM qQ _]] := (subset_trans (normG Q) sNQL, and3P sylQ). have nsLbL : L`_\beta <| L := pcore_normal _ L; have [sLbL nLbL] := andP nsLbL. have nLbQ := subset_trans sQL nLbL. have [<- ti_aLsM _] := sigma_disjoint maxL maxM notLGM. rewrite subsetI (subset_trans _ (Mbeta_sub_Msigma maxM)) ?andbT; last first. by rewrite (subset_trans (commgSS sXMb sQM)) // commg_subl nMbM. have defQ: [~: Q, P] = Q. rewrite -{2}(coprime_cent_prod nQP) ?(pgroup_sol qQ) ?regPQ ?mulg1 //. by rewrite (p'nat_coprime (pi_pnat qQ _) pP). suffices sXL: X \subset L. apply: subset_trans (Mbeta_sub_Malpha L). rewrite -quotient_sub1 ?comm_subG ?quotientR ?(subset_trans _ nLbL) //. have <-: (M`_\beta :&: L) / L`_\beta :&: 'O_q(L^`(1) / L`_\beta) = 1. rewrite coprime_TIg // coprime_morphl // (coprimeSg (subsetIl _ _)) //. exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat (pcore_pgroup _ _) _). rewrite commg_subI // subsetI. rewrite quotientS /=; last by rewrite subsetI sXMb. by rewrite quotient_der ?gFnorm_trans ?normsG ?quotientS. rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ (Mbeta_quo_nil _))) //. rewrite quotient_pgroup ?quotient_norms //. by rewrite normsI ?(subset_trans sQM nMbM) ?normsG. by rewrite quotientS // -defQ commgSS // (subset_trans nQP). have{hypU} [r bLr piHr]: exists2 r, r \in \beta(L) & r \in \pi(H). have [_ _ _] := and5P hypU; rewrite -rank_gt0. have [r _ ->] := rank_witness 'C_(L`_\beta)(P); rewrite p_rank_gt0 => piCr _. have [piLb_r piCPr] := (piSg (subsetIl _ _) piCr, piSg (subsetIr _ _) piCr). have bLr: r \in \beta(L) := pnatPpi (pcore_pgroup _ L) piLb_r. exists r; rewrite //= (card_Hall hallH) pi_of_part // inE /= piCPr. by rewrite inE /= bLr orbT. have sM'r: r \notin \sigma(M). by apply: contraFN (ti_aLsM r) => sMr; rewrite inE /= beta_sub_alpha. have defM: M`_\beta * 'N_M(Q) = M. have nMbQ := subset_trans sQM nMbM. have nsMbQ_M: M`_\beta <*> Q <| M. rewrite -{2}(quotientGK nsMbM) -quotientYK ?cosetpre_normal //. suffices ->: Q / M`_\beta = 'O_q(M^`(1) / M`_\beta). by rewrite quotient_der ?nMbM ?gFnormal_trans. apply: nilpotent_Hall_pcore; first exact: Mbeta_quo_nil. rewrite quotient_pHall // (pHall_subl _ _ sylQ) ?gFsub //. by rewrite -defQ commgSS // (subset_trans nUP). have sylQ_MbQ := pHall_subl (joing_subr _ Q) (normal_sub nsMbQ_M) sylQ. rewrite -{3}(Frattini_arg nsMbQ_M sylQ_MbQ) /= norm_joinEr // -mulgA. by congr (_ * _); rewrite mulSGid // subsetI sQM normG. have [[sM'p _ not_pM'] [sL'p _]] := (and3P t1Mp, andP t1Lp). have{not_pM'} [R ErR nQR]: exists2 R, R \in 'E_r^1('C_M(P)) & R \subset 'N(Q). have p'r: r \in p^' by apply: contraNneq sL'p => <-; apply: beta_sub_sigma. have p'M': p^'.-group M^`(1). by rewrite p'groupEpi mem_primes (negPf not_pM') !andbF. pose K := 'O_p^'(M); have [sKM nKM] := andP (pcore_normal _ M : K <| M). have hallK: p^'.-Hall(M) K. rewrite -(pquotient_pHall _ (der_normal 1 M)) ?quotient_pgroup //. rewrite -pquotient_pcore ?der_normal // nilpotent_pcore_Hall //. by rewrite abelian_nil ?der_abelian. by rewrite (normalS _ sKM) ?pcore_max ?der_normal. have sMbK: M`_\beta \subset K. by rewrite (subset_trans (Mbeta_der1 maxM)) // pcore_max ?der_normal. have coKP: coprime #|K| #|P| := p'nat_coprime (pcore_pgroup _ M) pP. have [solK sNK] := (solvableS sKM (mmax_sol maxM), subsetIl K 'N(Q)). have [nKP coNP] := (subset_trans sPM nKM, coprimeSg sNK coKP). have nNP: P \subset 'N('N_K(Q)) by rewrite normsI // norms_norm. have [S sylS nSP] := coprime_Hall_exists r nNP coNP (solvableS sNK solK). have /subsetIP[sSK nQS]: S \subset 'N_K(Q) := pHall_sub sylS. have sylS_K: r.-Sylow(K) S. rewrite pHallE sSK /= -/K -(setIidPr sKM) -defM -group_modl // setIAC. rewrite (setIidPr sKM) -LagrangeMr partnM // -(card_Hall sylS). rewrite part_p'nat ?mul1n 1?(pnat_dvd (dvdn_indexg _ _)) //. by apply: (pi_p'nat bMb); apply: contra sM'r; apply: beta_sub_sigma. have rC: 'r_r('C_M(P)) > 0 by rewrite p_rank_gt0 (piSg _ piHr) // subsetI sHM. have{rC} [R ErR] := p_rank_geP rC; have [sRcMP abelR _] := pnElemP ErR. have{sRcMP abelR} [[sRM cPR] [rR _]] := (subsetIP sRcMP, andP abelR). have nRP: P \subset 'N(R) by rewrite cents_norm 1?centsC. have sRK: R \subset K by rewrite sub_Hall_pcore ?(pi_pgroup rR). have [T [sylT nTP sRT]] := coprime_Hall_subset nKP coKP solK sRK rR nRP. have [x cKPx defS] := coprime_Hall_trans nKP coKP solK sylS_K nSP sylT nTP. rewrite -(conjGid (subsetP (setSI _ sKM) x cKPx)). by exists (R :^ x)%G; rewrite ?pnElemJ ?(subset_trans _ nQS) // defS conjSg. have [sRcMP abelR _] := pnElemP ErR; have ntR := nt_pnElem ErR isT. have{sRcMP abelR} [[sRM cPR] [rR _]] := (subsetIP sRcMP, andP abelR). have sNR_L: 'N(R) \subset L. by rewrite beta_norm_sub_mmax /psubgroup ?(subset_trans nQR) ?(pi_pgroup rR). have sPR_M: P <*> R \subset M by rewrite join_subG (subset_trans nUP). have sM'_PR: \sigma(M)^'.-group (P <*> R). by rewrite cent_joinEr // pgroupM (pi_pgroup rR) // (pi_pgroup pP). have [E hallE sPRE] := Hall_superset (mmax_sol maxM) sPR_M sM'_PR. have{sPRE} [sPE sRE] := joing_subP sPRE. have EpP: P \in 'E_p^1(E) by apply/pnElemP. have{} ErR: R \in 'E_r^1('C_E(P)). by rewrite -(setIidPr (pHall_sub hallE)) setIAC pnElemI inE ErR inE. apply: subset_trans (cents_norm (subset_trans _ (subsetIr M`_\sigma _))) sNR_L. apply: subset_trans (cent_tau1Elem_Msigma maxM hallE t1Mp EpP ErR). by rewrite subsetI cPX (subset_trans sXMb) ?Mbeta_sub_Msigma. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12)