proposition: Corollary sigma'_nil_abelian M N : M \in 'M -> N \subset M -> \sigma(M)^'.-group N -> nilpotent N -> abelian N.
proof: Proof. move=> maxM sNM sM'N /nilpotent_Fitting defN. apply/center_idP; rewrite -{2}defN -{defN}(center_bigdprod defN). apply: eq_bigr => p _; apply/center_idP; set P := 'O_p(N). have [-> | ntP] := eqVneq P 1; first exact: abelian1. have [pP sPN]: p.-group P /\ P \subset N by rewrite pcore_sub pcore_pgroup. have{sPN sNM sM'N} [sPM sM'P] := (subset_trans sPN sNM, pgroupS sPN sM'N). have{sPM sM'P} [E hallE sPE] := Hall_superset (mmax_sol maxM) sPM sM'P. suffices [S sylS cSS]: exists2 S : {group gT}, p.-Sylow(E) S & abelian S. by have [x _ sPS] := Sylow_subJ sylS sPE pP; rewrite (abelianS sPS) ?abelianJ. have{N P sPE pP ntP} piEp: p \in \pi(E). by rewrite (piSg sPE) // -p_rank_gt0 -rank_pgroup // rank_gt0. rewrite (partition_pi_sigma_compl maxM hallE) orbCA orbC -orbA in piEp. have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have{complEi} [_ _ [cycE1 cycE3] _ _] := sigma_compl_context maxM complEi. have{piEp} [t1p | t3p | t2p] := or3P piEp. - have [S sylS] := Sylow_exists p E1. exists S; first exact: subHall_Sylow hallE1 t1p sylS. exact: abelianS (pHall_sub sylS) (cyclic_abelian cycE1). - have [S sylS] := Sylow_exists p E3. exists S; first exact: subHall_Sylow hallE3 t3p sylS. exact: abelianS (pHall_sub sylS) (cyclic_abelian cycE3). have [s'p rpM] := andP t2p; have [S sylS] := Sylow_exists p E; exists S => //. have sylS_M := subHall_Sylow hallE s'p sylS. have [A _ Ep2A] := ex_tau2Elem hallE t2p. by have [/(_ S sylS_M)[]] := tau2_context maxM t2p Ep2A. 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)