proposition: Proposition sigma_subgroup_embedding M q X Mstar : M \in 'M -> q \in \sigma(M) -> X \subset M -> q.-group X -> X :!=: 1 -> Mstar \in 'M('N(X)) :\ M -> [/\ gval Mstar \notin M :^: G, forall S, q.-Sylow(M :&: Mstar) S -> X \subset S -> 'N(S) \subset M /\ q.-Sylow(Mstar) S & if q \in \sigma(Mstar) then [/\ Mstar`_\beta * (M :&: Mstar) = Mstar, {subset \tau1(Mstar) <= [predU \tau1(M) & \alpha(M)]} & M`_\beta = M`_\alpha /\ M`_\alpha != 1] else [/\ q \in \tau2(Mstar), {subset [predI \pi(M) & \sigma(Mstar)] <= \beta(Mstar)} & \sigma(Mstar)^'.-Hall(Mstar) (M :&: Mstar)]].
proof: Proof. move: Mstar => H maxM sMq sXM qX ntX /setD1P[neqHM maxNX_H]. have [q_pr _ _] := pgroup_pdiv qX ntX; have [maxH sNX_H] := setIdP maxNX_H. have sXH := subset_trans (normG X) sNX_H. have sX_MH: X \subset M :&: H by apply/subsetIP. have parts_bc S: q.-Sylow(M :&: H) S -> X \subset S -> 'N(S) \subset M /\ q.-Sylow(H) S. - move=> sylS sXS; have [sS_MH qS _] := and3P sylS. have [sSM sSH] := subsetIP sS_MH. have sNS_M: 'N(S) \subset M. have [cycS|] := boolP (cyclic S); last exact: norm_noncyclic_sigma qS _. have [T sylT sST] := Sylow_superset sSM qS; have [sTM qT _] := and3P sylT. rewrite -(nilpotent_sub_norm (pgroup_nil qT) sST). exact: norm_sigma_Sylow sylT. rewrite (sub_pHall sylS (pgroupS (subsetIl T _) qT)) //. by rewrite subsetI sST normG. by rewrite setISS // (subset_trans (char_norms _) sNX_H) // sub_cyclic_char. split=> //; have [T sylT sST] := Sylow_superset sSH qS. have [sTH qT _] := and3P sylT. rewrite -(nilpotent_sub_norm (pgroup_nil qT) sST) //. rewrite (sub_pHall sylS (pgroupS (subsetIl T _) qT)) //=. by rewrite subsetI sST normG. by rewrite /= setIC setISS. have [S sylS sXS] := Sylow_superset sX_MH qX; have [sS_MH qS _] := and3P sylS. have [sSM sSH] := subsetIP sS_MH; have [sNS_M sylS_H] := parts_bc S sylS sXS. have notMGH: gval H \notin M :^: G. by apply: mmax_norm_notJ maxM maxH qX sXM sNX_H _; rewrite sMq eq_sym neqHM. have /orP[sHq | t2Hq] := prime_class_mmax_norm maxH qX sNX_H; last first. have [/= sH'q rqH] := andP t2Hq; rewrite [q \in _](negPf sH'q); split=> //. have [A Eq2A] := p_rank_witness q S; have [sAS abelA dimA] := pnElemP Eq2A. rewrite (p_rank_Sylow sylS_H) (eqP rqH) in dimA; have [qA _] := andP abelA. have [sAH sAM] := (subset_trans sAS sSH, subset_trans sAS sSM). have [F hallF sAF] := Hall_superset (mmax_sol maxH) sAH (pi_pnat qA sH'q). have tiHsM: H`_\sigma :&: M = 1. have{} Eq2A: A \in 'E_q^2(H) by apply/pnElemP. have [_ _ _ -> //] := tau2_context maxH t2Hq Eq2A. by rewrite 3!inE eq_sym neqHM maxM. have{Eq2A} Eq2A_F: A \in 'E_q^2(F) by apply/pnElemP. have [[nsAF _] [sCA_F _ _] _ TIsH] := tau2_compl_context maxH hallF t2Hq Eq2A_F. have sNA_M: 'N(A) \subset M. apply: norm_noncyclic_sigma maxM sMq qA sAM _. by rewrite (abelem_cyclic abelA) dimA. have ->: M :&: H = F. have [[_ <- _ _] [_ nAF]] := (sdprodP (sdprod_sigma maxH hallF), andP nsAF). by rewrite -(group_modr _ (subset_trans nAF sNA_M)) setIC tiHsM mul1g. split=> // p /andP[/= piMp sHp]; apply: wlog_neg => bH'p. have bM'q: q \notin \beta(M). by rewrite -predI_sigma_beta // inE /= sMq; case/tau2_not_beta: t2Hq. have sM'p: p \notin \sigma(M). rewrite orbit_sym in notMGH; have [_ TIsHM] := TIsH M maxM notMGH. by have:= TIsHM p; rewrite inE /= sHp /= => ->. have p'CA: p^'.-group 'C(A). by rewrite (pgroupS sCA_F) // (pi'_p'group (pHall_pgroup hallF)). have p_pr: prime p by rewrite mem_primes in piMp; case/andP: piMp. have [lt_pq | lt_qp | eq_pq] := ltngtP p q; last 1 first. - by rewrite eq_pq sMq in sM'p. - have bH'q: q \notin \beta(H) by apply: contra sH'q; apply: beta_sub_sigma. have [|[P sylP cPA] _ _] := beta'_cent_Sylow maxH bH'p bH'q qA. by rewrite lt_pq sAH orbT. have sylP_H := subHall_Sylow (Msigma_Hall maxH) sHp sylP. have piPp: p \in \pi(P). by rewrite -p_rank_gt0 (p_rank_Sylow sylP_H) p_rank_gt0 sigma_sub_pi. by rewrite centsC in cPA; case/eqnP: (pnatPpi (pgroupS cPA p'CA) piPp). have bM'p: p \notin \beta(M) by apply: contra sM'p; apply: beta_sub_sigma. have [P sylP] := Sylow_exists p M; have [sMP pP _] := and3P sylP. have [|[Q1 sylQ1 cQ1P] _ _] := beta'_cent_Sylow maxM bM'q bM'p pP. by rewrite lt_qp sMP orbT. have sylQ1_M := subHall_Sylow (Msigma_Hall maxM) sMq sylQ1. have [x Mx sAQ1x] := Sylow_subJ sylQ1_M sAM qA. have sPxCA: P :^ x \subset 'C(A) by rewrite (centsS sAQ1x) // centJ conjSg. have piPx_p: p \in \pi(P :^ x). by rewrite /= cardJg -p_rank_gt0 (p_rank_Sylow sylP) p_rank_gt0. by case/eqnP: (pnatPpi (pgroupS sPxCA p'CA) piPx_p). rewrite sHq; split=> //. have sNS_HM: 'N(S) \subset H :&: M by rewrite subsetI (norm_sigma_Sylow sHq). have sylS_G: q.-Sylow(G) S := sigma_Sylow_G maxH sHq sylS_H. have [defM eq_abM] := nonuniq_norm_Sylow_pprod maxM maxH neqHM sylS_G sNS_HM. rewrite setIC eq_sym in sNS_HM neqHM defM. have [defH eq_abH] := nonuniq_norm_Sylow_pprod maxH maxM neqHM sylS_G sNS_HM. rewrite [M`_\alpha](eq_pcore M eq_abM) -/M`_\beta. split=> // [r t1Hr|]; last first. split=> //; apply: contraNneq neqHM => Mb1. by rewrite -val_eqE /= (eq_mmax maxM maxH) // -defM Mb1 mul1g subsetIr. have [R sylR] := Sylow_exists r (M :&: H); have [sR_MH rR _] := and3P sylR. have [sRM sRH] := subsetIP sR_MH; have [sH'r rrH not_rH'] := and3P t1Hr. have bH'r: r \notin \beta(H). by apply: contra sH'r; rewrite -eq_abH; apply: alpha_sub_sigma. have sylR_H: r.-Sylow(H) R. rewrite pHallE sRH -defH -LagrangeMr partnM ?cardG_gt0 //. rewrite -(card_Hall sylR) part_p'nat ?mul1n ?(pnat_dvd (dvdn_indexg _ _)) //=. by rewrite (pi_p'nat (pcore_pgroup _ _)). rewrite inE /= orbC -implyNb eq_abM; apply/implyP=> bM'r. have sylR_M: r.-Sylow(M) R. rewrite pHallE sRM -defM -LagrangeMr partnM ?cardG_gt0 //. rewrite -(card_Hall sylR) part_p'nat ?mul1n ?(pnat_dvd (dvdn_indexg _ _)) //=. by rewrite (pi_p'nat (pcore_pgroup _ _)). have rrR: 'r_r(R) = 1%N by rewrite (p_rank_Sylow sylR_H) (eqP rrH). have piRr: r \in \pi(R) by rewrite -p_rank_gt0 rrR. suffices not_piM'r: r \notin \pi(M^`(1)). rewrite inE /= -(p_rank_Sylow sylR_M) rrR /= -negb_or /=. apply: contra not_piM'r; case/orP=> [sMr | rM']. have sRMs: R \subset M`_\sigma. by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup rR). by rewrite (piSg (Msigma_der1 maxM)) // (piSg sRMs). by move: piRr; rewrite !mem_primes !cardG_gt0; case/andP=> ->. have coMbR: coprime #|M`_\beta| #|R|. exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat rR _). have sylRM': r.-Sylow(M^`(1)) _ := Hall_setI_normal (der_normal 1 M) sylR_M. rewrite -p'groupEpi -partG_eq1 -(card_Hall sylRM') -trivg_card1 /=. rewrite (pprod_focal_coprime defM (pcore_normal _ _)) //. rewrite coprime_TIg ?(pnat_coprime rR (pgroupS (dergS 1 (subsetIr _ _)) _)) //. by rewrite p'groupEpi mem_primes (negPf not_rH') !andbF. 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)