proposition: Corollary Fitting_structure M (H := M`_\F) (Y := 'O_\sigma(M)^'('F(M))) : M \in 'M -> [/\ cyclic Y /\ \tau2(M).-group Y, [/\ M^`(2) \subset 'F(M), H \* 'C_M(H) = 'F(M) & 'F(M`_\sigma) \x Y = 'F(M)], H \subset M^`(1) /\ nilpotent (M^`(1) / H) & M \in 'M_'P -> 'F(M) \subset M^`(1)].
proof: Proof. move=> maxM; have nilF := Fitting_nil M. have sHF: H \subset 'F(M) := Fcore_sub_Fitting M. have nsMsM: M`_\sigma <| M := pcore_normal _ _; have [sMsM nMsM] := andP nsMsM. have sMs: \sigma(M).-group M`_\sigma := pcore_pgroup _ _. have nsFM: 'F(M) <| M := Fitting_normal M; have [sFM nFM] := andP nsFM. have sYF: Y \subset 'F(M) := pcore_sub _ _; have sYM := subset_trans sYF sFM. have defF: 'F(M`_\sigma) \x Y = 'F(M). rewrite -(nilpotent_pcoreC \sigma(M) nilF); congr (_ \x _). apply/eqP; rewrite eqEsubset pcore_max ?(pgroupS (Fitting_sub _)) //=. rewrite Fitting_max ?(nilpotentS (pcore_sub _ _)) //=. by rewrite -(pcore_setI_normal _ nsFM) norm_normalI ?(subset_trans sMsM). rewrite /normal (char_norm_trans (Fitting_char _)) ?(subset_trans sFM) //. by rewrite Fitting_max ?Fitting_nil ?gFnormal_trans. have [[ntH sHMs sMsM' _] nnil_struct] := Fcore_structure maxM. have hallH: \pi(H).-Hall(M`_\sigma) H := pHall_subl sHMs sMsM (Fcore_Hall M). have [X [_ cycX t2X defCH]] := cent_Hall_sigma_sdprod maxM hallH ntH. have hallX: \sigma(M)^'.-Hall('C_M(H)) X. have [_ mulCsH_X _ _] := sdprodP defCH. have [|//] := coprime_mulpG_Hall mulCsH_X (pgroupS (subsetIl _ _) sMs). by apply: sub_pgroup t2X => p /andP[]. have sYX: Y \subset X. rewrite (normal_sub_max_pgroup (Hall_max hallX)) ?pcore_pgroup //. rewrite /normal gFnorm_trans ?subIset ?nFM //= -/Y andbT. have [_ _ cFsY _] := dprodP defF. rewrite subsetI sYM (sub_nilpotent_cent2 nilF) //= -/Y -/H. exact: pnat_coprime (pgroupS sHMs sMs) (pcore_pgroup _ _). have [cycY t2Y]: cyclic Y /\ \tau2(M).-group Y. by rewrite (cyclicS sYX cycX) (pgroupS sYX t2X). have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). have [U complU] := ex_kappa_compl maxM hallK. have [[defM _ cM'M'b] defM' _ _ _] := kappa_structure maxM complU. have d_holds: M \in 'M_'P -> 'F(M) \subset M^`(1). rewrite inE maxM andbT -(trivg_kappa maxM hallK) => ntK. rewrite -(dprodW defF) mulG_subG gFsub_trans //= -/Y. have{defM'} [[defM' _] nsM'M] := (defM' ntK, der_normal 1 M). have hallM': \kappa(M)^'.-Hall(M) M^`(1). by apply/(sdprod_normal_pHallP nsM'M hallK); rewrite /= -defM'. rewrite (sub_normal_Hall hallM') ?(sub_pgroup _ t2Y) // => p /andP[_]. by apply: contraL => /rank_kappa->. have defF_H: 'C_M(H) \subset 'F(M) -> H \* 'C_M(H) = 'F(M). move=> sCHF; apply/eqP; rewrite cprodE ?subsetIr // eqEsubset ?mul_subG //=. have hallH_F := pHall_subl sHF sFM (Fcore_Hall M). have nsHF := normalS sHF sFM (Fcore_normal M). have /dprodP[_] := nilpotent_pcoreC \pi(H) nilF. rewrite (normal_Hall_pcore hallH_F nsHF) /= -/H => defF_H cHFH' _. by rewrite -defF_H mulgS // subsetI gFsub_trans. have [eqHMs | neqHMs] := eqVneq H M`_\sigma. split=> //; [split=> // | by rewrite eqHMs abelian_nil]. by rewrite (subset_trans _ sHF) //= eqHMs der1_min ?comm_subG. rewrite defF_H // -(sdprodW defCH) -eqHMs mulG_subG subIset ?sHF //=. rewrite Fitting_max ?abelian_nil ?cyclic_abelian //. rewrite -(normal_Hall_pcore hallX) ?gFnormal_trans //. by rewrite norm_normalI // eqHMs norms_cent. move: defCH; rewrite -dprodEsd; first by case/dprod_normal2. by rewrite -eqHMs (centsS (subsetIl _ _)); case/subsetIP: (pHall_sub hallX). pose q := #|'C_(M`_\sigma)(K)|; pose Q := 'O_q(M). have [D hallD] := Hall_exists q^' (solvableS sMsM (mmax_sol maxM)). case/(_ K D): nnil_struct => //=; rewrite -/H -/q -/Q. move=> [_ _ defMs] [_ _ piHq _] [sylQ nilD _] _ [_ -> [defF_Q _ _] _]. have sQH: Q \subset H by rewrite -[Q](p_core_Fcore piHq) pcore_sub. split=> //; rewrite -?{}defMs; split=> //. by rewrite defF_H // -defF_Q joingC sub_gen // subsetU ?setIS ?centS. have sQMs := subset_trans sQH sHMs; have sylQ_Ms := pHall_subl sQMs sMsM sylQ. have nsQ_Ms: Q <| M`_\sigma := normalS sQMs sMsM (pcore_normal _ _). have defMs: Q ><| D = M`_\sigma := sdprod_normal_p'HallP nsQ_Ms hallD sylQ_Ms. have [_ <- _ _] := sdprodP defMs; rewrite -quotientMidl mulgA (mulGSid sQH). by rewrite quotientMidl quotient_nil. 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 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14)