proposition: Lemma sigma_compl_embedding M E (Ms := M`_\sigma) : M \in 'M -> \sigma(M)^'.-Hall(M) E -> [/\ 'C_Ms(E) \subset Ms^`(1), [~: Ms, E] = Ms & forall g (MsMg := Ms :&: M :^ g), g \notin M -> [/\ cyclic MsMg, \beta(M)^'.-group MsMg & MsMg :&: Ms^`(1) = 1]].
proof: Proof. move=> maxM hallE; have [sEM s'E _] := and3P hallE. have solMs: solvable Ms := solvableS (pcore_sub _ _) (mmax_sol maxM). have defM := coprime_der1_sdprod (sdprod_sigma maxM hallE). have{s'E} coMsE: coprime #|Ms| #|E| := pnat_coprime (pcore_pgroup _ _) s'E. have{defM coMsE} [-> ->] := defM coMsE solMs (Msigma_der1 maxM). split=> // g MsMg notMg. have sMsMg: \sigma(M).-group MsMg := pgroupS (subsetIl _ _) (pcore_pgroup _ _). have EpMsMg p n X: X \in 'E_p^n(MsMg) -> n > 0 -> n = 1%N /\ ~~ ((p \in \beta(M)) || (X \subset Ms^`(1))). - move=> EpX n_gt0; have [sXMsMg abelX dimX] := pnElemP EpX. have [[sXMs sXMg] [pX _]] := (subsetIP sXMsMg, andP abelX). have sXM := subset_trans sXMs (pcore_sub _ _). have piXp: p \in \pi(X) by rewrite -p_rank_gt0 p_rank_abelem ?dimX. have sMp: p \in \sigma(M) := pnatPpi (pgroupS sXMs (pcore_pgroup _ _)) piXp. have not_sCX_M: ~~ ('C(X) \subset M). apply: contra notMg => sCX_M; rewrite -groupV. have [transCX _ _] := sigma_group_trans maxM sMp pX. have [|c CXc [m Mm ->]] := transCX g^-1 sXM; rewrite ?sub_conjgV //. by rewrite groupM // (subsetP sCX_M). have cycX: cyclic X. apply: contraR not_sCX_M => ncycX; apply: subset_trans (cent_sub _) _. exact: norm_noncyclic_sigma maxM sMp pX sXM ncycX. have n1: n = 1%N by apply/eqP; rewrite eqn_leq -{1}dimX -abelem_cyclic ?cycX. rewrite n1 in dimX *; split=> //; apply: contra not_sCX_M. by case/cent_der_sigma_uniq=> //; [apply/pnElemP | case/mem_uniq_mmax]. have tiMsMg_Ms': MsMg :&: Ms^`(1) = 1. apply/eqP/idPn; rewrite -rank_gt0 => /rank_geP[X /nElemP[p]]. case/pnElemP=> /subsetIP[sXMsMg sXMs'] abelX dimX. by case: (EpMsMg p 1%N X) => //; [apply/pnElemP | rewrite sXMs' orbT]. split=> //; last first. apply: sub_in_pnat sMsMg => p. by rewrite -p_rank_gt0 => /p_rank_geP[X /EpMsMg[] // _ /norP[]]. rewrite abelian_rank1_cyclic. by rewrite leqNgt; apply/rank_geP=> [[X /nElemP[p /EpMsMg[]]]]. by rewrite (sameP derG1P trivgP) -tiMsMg_Ms' subsetI der_sub dergS ?subsetIl. 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)