proposition: Corollary Ptype_cyclics M K (Ks := 'C_(M`_\sigma)(K)) : M \in 'M_'P -> \kappa(M).-Hall(M) K -> [/\ Ks != 1, cyclic Ks, Ks \subset M^`(2), Ks \subset M`_\F & ~~ cyclic M`_\F].
proof: Proof. move=> PmaxM hallK; have [ntK maxM] := setIdP PmaxM. rewrite -(trivg_kappa maxM hallK) in ntK. have [_ _ [ntKs _] _ _] := Ptype_structure PmaxM hallK. have [_ _ [_ _ _ [cycZ _ _ _ _] [_ _ _ defM]]] := Ptype_embedding PmaxM hallK. have{cycZ} cycKs: cyclic Ks := cyclicS (joing_subr _ _) cycZ. have solM': solvable M^`(1) := solvableS (der_sub 1 M) (mmax_sol maxM). have sMsM' := Msigma_der1 maxM. have{defM} sKsM'': Ks \subset M^`(2). have coM'K: coprime #|M^`(1)| #|K|. by rewrite (coprime_sdprod_Hall_r defM) (pHall_Hall hallK). have [_] := coprime_der1_sdprod defM coM'K solM' (subxx _). exact: subset_trans (setSI _ sMsM'). have [eqMFs | neqMFs] := eqVneq M`_\F M`_\sigma. split=> //; rewrite eqMFs ?subsetIl //; apply: contra ntKs => cycMs. rewrite -subG1 (subset_trans sKsM'') // (sameP trivgP derG1P) /= -derg1. have cycF: cyclic 'F(M). have [[cycY _] [_ _ defF] _ _] := Fitting_structure maxM. have [[x defMs] [y defY]] := (cyclicP cycMs, cyclicP cycY). rewrite defMs (nilpotent_Fitting (abelian_nil (cycle_abelian _))) in defF. have [_ mulXY cxy _] := dprodP defF. rewrite -mulXY defY -cycleM ?cycle_cyclic //. by apply/cent1P; rewrite -cycle_subG sub_cent1 -cycle_subG -defY. by rewrite /order -defMs -defY coprime_pcoreC. apply: abelianS (cyclic_abelian cycF). apply: subset_trans (cent_sub_Fitting (mmax_sol maxM)). rewrite der1_min ?normsI ?normG ?norms_cent ?gFnorm //=. rewrite -ker_conj_aut (isog_abelian (first_isog_loc _ _)) ?gFnorm //=. exact: abelianS (Aut_conj_aut _ _) (Aut_cyclic_abelian cycF). have [D hallD] := Hall_exists #|Ks|^' (solvableS sMsM' solM'). have [_ /(_ K D)[]//=] := Fcore_structure maxM; rewrite -/Ks. set q := #|Ks|; set Q := 'O_q(M) => _ [_ q_pr piMFq bMq] [sylQ _ _] _ _. have sQMF: Q \subset M`_\F by rewrite -[Q]p_core_Fcore ?pcore_sub. have qKs: q.-group Ks := pnat_id q_pr. have sKsM := subset_trans sKsM'' (der_sub 2 M). split=> //; first by apply: subset_trans sQMF; rewrite (sub_Hall_pcore sylQ). apply: contraL (beta_sub_alpha bMq) => /(cyclicS sQMF)cycQ; rewrite -leqNgt. by rewrite leqW // -(rank_Sylow sylQ) -abelian_rank1_cyclic ?cyclic_abelian. 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)