proposition: Theorem abelian_tau2 M E E1 E2 E3 p A S (Ms := M`_\sigma) : M \in 'M -> sigma_complement M E E1 E2 E3 -> p \in \tau2(M) -> A \in 'E_p^2(E) -> p.-Sylow(G) S -> A \subset S -> abelian S -> [/\ E2 <| E /\ abelian E2, \tau2(M).-Hall(G) E2, [/\ 'N(A) = 'N(S), 'N(S) = 'N(E2), 'N(E2) = 'N(E3 <*> E2) & 'N(E3 <*> E2) = 'N('F(E))] & forall X, X \in 'E^1(E1) -> 'C_Ms(X) = 1 -> X \subset 'Z(E)].
proof: Proof. move=> maxM complEi t2Mp Ep2A sylS sAS cSS. have [hallE hallE1 hallE2 hallE3 _] := complEi. have [sEM sM'E _] := and3P hallE. have [sE1E t1E1 _] := and3P hallE1. have [sE2E t2E2 _] := and3P hallE2. have [sE3E t3E3 _] := and3P hallE3. have nilF: nilpotent 'F(E) := Fitting_nil E. have sylE2_sylG_ZFE q Q: q.-Sylow(E2) Q -> Q :!=: 1 -> q.-Sylow(G) Q /\ Q \subset 'Z('F(E)). - move=> sylQ ntQ; have [sQE2 qQ _] := and3P sylQ. have piQq: q \in \pi(Q) by rewrite -p_rank_gt0 -rank_pgroup // rank_gt0. have t2Mq: q \in \tau2(M) by rewrite (pnatPpi t2E2) // (piSg sQE2). have sylQ_E: q.-Sylow(E) Q := subHall_Sylow hallE2 t2Mq sylQ. have rqQ: 'r_q(Q) = 2. rewrite (tau2E hallE) !inE -(p_rank_Sylow sylQ_E) in t2Mq. by case/andP: t2Mq => _ /eqP. have [B Eq2B sBQ]: exists2 B, B \in 'E_q^2(E) & B \subset Q. have [B Eq2B] := p_rank_witness q Q; have [sBQ abelB rBQ] := pnElemP Eq2B. exists B; rewrite // !inE rBQ rqQ abelB !andbT. exact: subset_trans sBQ (pHall_sub sylQ_E). have [T /= sylT sQT] := Sylow_superset (subsetT Q) qQ. have qT: q.-group T := pHall_pgroup sylT. have cTT: abelian T. apply: wlog_neg => not_cTT. have [def_t2 _ _ _] := nonabelian_tau2 maxM hallE t2Mq Eq2B qT not_cTT. rewrite def_t2 !inE in t2Mp; rewrite (eqP t2Mp) in sylS. by have [x _ ->] := Sylow_trans sylS sylT; rewrite abelianJ. have sTF: T \subset 'F(E). have subF := abelian_tau2_sub_Fitting maxM hallE t2Mq Eq2B sylT. have [sTN' sN'F _ _ _] := subF (subset_trans sBQ sQT) cTT. exact: subset_trans sTN' sN'F. have sTE: T \subset E := subset_trans sTF (Fitting_sub E). have <-: T :=: Q by apply: (sub_pHall sylQ_E). have sylT_F: q.-Sylow('F(E)) T := pHall_subl sTF (subsetT _) sylT. have [_ <- _ _] := dprodP (center_dprod (nilpotent_pcoreC q nilF)). by rewrite -(nilpotent_Hall_pcore nilF sylT_F) (center_idP cTT) mulG_subl. have hallE2_G: \tau2(M).-Hall(G) E2. rewrite pHallE subsetT /= -(part_pnat_id t2E2); apply/eqnP. rewrite !(widen_partn _ (subset_leq_card (subsetT _))). apply: eq_bigr => q t2q; rewrite -!p_part. have [Q sylQ] := Sylow_exists q E2; have qQ := pHall_pgroup sylQ. have sylQ_E: q.-Sylow(E) Q := subHall_Sylow hallE2 t2q sylQ. have ntQ: Q :!=: 1. rewrite -rank_gt0 (rank_pgroup qQ) (p_rank_Sylow sylQ_E) p_rank_gt0. by rewrite (tau2E hallE) in t2q; case/andP: t2q. have [sylQ_G _] := sylE2_sylG_ZFE q Q sylQ ntQ. by rewrite -(card_Hall sylQ) -(card_Hall sylQ_G). have sE2_ZFE: E2 \subset 'Z('F(E)). rewrite -Sylow_gen gen_subG; apply/bigcupsP=> Q; case/SylowP=> q q_pr sylQ. have [-> | ntQ] := eqsVneq Q 1; first exact: sub1G. by have [_ ->] := sylE2_sylG_ZFE q Q sylQ ntQ. have cE2E2: abelian E2 := abelianS sE2_ZFE (center_abelian _). have sE2FE: E2 \subset 'F(E) := subset_trans sE2_ZFE (center_sub _). have nsE2E: E2 <| E. have hallE2_F := pHall_subl sE2FE (Fitting_sub E) hallE2. by rewrite (nilpotent_Hall_pcore nilF hallE2_F) !gFnormal_trans. have [_ _ [cycE1 cycE3] [_ defEl] _] := sigma_compl_context maxM complEi. have [[K _ defK _] _ _ _] := sdprodP defEl; rewrite defK in defEl. have [nsKE _ mulKE1 nKE1 _] := sdprod_context defEl; have [sKE _] := andP nsKE. have [nsE3K sE2K _ nE32 tiE32] := sdprod_context defK. rewrite -sdprodEY // defK. have{} defK: E3 \x E2 = K. rewrite dprodEsd // (sameP commG1P trivgP) -tiE32 subsetI commg_subr nE32. by rewrite commg_subl (subset_trans sE3E) ?normal_norm. have cKK: abelian K. by have [_ <- cE23 _] := dprodP defK; rewrite abelianM cE2E2 cyclic_abelian. have [_ sNS'F _ sCS_E defFN] := abelian_tau2_sub_Fitting maxM hallE t2Mp Ep2A sylS sAS cSS. have{sCS_E} sSE2: S \subset E2. rewrite (sub_normal_Hall hallE2 nsE2E (subset_trans cSS sCS_E)). by rewrite (pi_pgroup (pHall_pgroup sylS)). have charS: S \char E2. have sylS_E2: p.-Sylow(E2) S := pHall_subl sSE2 (subsetT E2) sylS. by rewrite (nilpotent_Hall_pcore (abelian_nil cE2E2) sylS_E2) pcore_char. have nsSE: S <| E := char_normal_trans charS nsE2E; have [sSE nSE] := andP nsSE. have charA: A \char S. have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A. have sylS_M := pHall_subl (subset_trans sSE sEM) (subsetT M) sylS. have [] := tau2_context maxM t2Mp Ep2A_M; case/(_ S sylS_M)=> _ [//|<- _]. by rewrite Ohm_char. have charE2: E2 \char K. have hallE2_K := pHall_subl sE2K sKE hallE2. by rewrite (nilpotent_Hall_pcore (abelian_nil cKK) hallE2_K) pcore_char. have coKE1: coprime #|K| #|E1|. rewrite -(dprod_card defK) coprimeMl (sub_pnat_coprime tau3'1 t3E3 t1E1). by rewrite (sub_pnat_coprime tau2'1 t2E2 t1E1). have hallK: Hall 'F(E) K. have hallK: Hall E K. by rewrite /Hall -divgS sKE //= -(sdprod_card defEl) mulKn. have sKFE: K \subset 'F(E) by rewrite Fitting_max ?abelian_nil. exact: pHall_Hall (pHall_subl sKFE (Fitting_sub E) (Hall_pi hallK)). have charK: K \char 'F(E). by rewrite (nilpotent_Hall_pcore nilF (Hall_pi hallK)) pcore_char. have{defFN} [eqNAS eqNSE2 eqNE2K eqNKF]: [/\ 'N(A) = 'N(S), 'N(S) = 'N(E2), 'N(E2) = 'N(K) & 'N(K) = 'N('F(E))]. have: #|'N(A)| <= #|'N('F(E))|. by rewrite subset_leq_card // -defFN gFnorm. have leCN := subset_leqif_cards (@char_norms gT _ _ _). have trCN := leqif_trans (leCN _ _ _). have leq_KtoA := trCN _ _ _ _ charE2 (trCN _ _ _ _ charS (leCN _ _ charA)). rewrite (geq_leqif (trCN _ _ _ _ charK leq_KtoA)). by case/and4P; do 4!move/eqP->. split=> // X E1_1_X regX. have cK_NK': 'N(K)^`(1) \subset 'C(K). suffices sKZ: K \subset 'Z('F(E)). by rewrite -eqNE2K -eqNSE2 (centSS sNS'F sKZ) // centsC subsetIr. have{hallK} [pi hallK] := HallP hallK. have [_ <- _ _] := dprodP (center_dprod (nilpotent_pcoreC pi nilF)). by rewrite -(nilpotent_Hall_pcore nilF hallK) (center_idP cKK) mulG_subl. have [q EqX] := nElemP E1_1_X; have [sXE1 abelX dimX] := pnElemP EqX. have sXE := subset_trans sXE1 sE1E. have nKX := subset_trans sXE (normal_norm nsKE). have nCSX_NS: 'N(K) \subset 'N('C(K) * X). rewrite -(quotientGK (cent_normal _)) -quotientK ?norms_cent //. by rewrite morphpre_norms // sub_abelian_norm ?quotientS ?sub_der1_abelian. have nKX_NS: 'N(S) \subset 'N([~: K, X]). have CK_K_1: [~: 'C(K), K] = 1 by apply/commG1P. rewrite eqNSE2 eqNE2K commGC -[[~: X, K]]mul1g -CK_K_1. by rewrite -commMG ?CK_K_1 ?norms1 ?normsR. have not_sNKX_M: ~~ ('N([~: K, X]) \subset M). have [[sM'p _] sSM] := (andP t2Mp, subset_trans sSE sEM). apply: contra sM'p => sNKX_M; apply/existsP; exists S. by rewrite (pHall_subl sSM (subsetT _) sylS) // (subset_trans _ sNKX_M). have cKX: K \subset 'C(X). apply: contraR not_sNKX_M; rewrite (sameP commG1P eqP) => ntKX. rewrite (mmax_normal maxM) //. have [sKM sM'K] := (subset_trans sKE sEM, pgroupS sKE sM'E). have piE1q: q \in \pi(E1). by rewrite -p_rank_gt0 -dimX logn_le_p_rank // inE sXE1. have sM'q: q \in \sigma(M)^' by rewrite (pnatPpi sM'E) // (piSg sE1E). have EpX_NK: X \in 'E_q^1('N_M(K)). by apply: subsetP EqX; rewrite pnElemS // subsetI (subset_trans sE1E). have q'K: q^'.-group K. by rewrite p'groupEpi ?coprime_pi' // in coKE1 *; apply: (pnatPpi coKE1). by have []:= commG_sigma'_1Elem_cyclic maxM sKM sM'K sM'q EpX_NK regX. rewrite subsetI sXE /= -mulKE1 centM subsetI centsC cKX. exact: subset_trans sXE1 (cyclic_abelian cycE1). 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)