proposition: Theorem tau2_P2type_signalizer M Mstar U K r R H (q := #|K|) : M \in 'M_'P2 -> kappa_complement M U K -> Mstar \in 'M('C(K)) -> r.-Sylow(U) R -> H \in 'M('N(R)) -> ~~ \tau2(H)^'.-group H -> [/\ prime q, \tau2(H) =i (q : nat_pred) & \tau2(M)^'.-group M].
proof: Proof. move: Mstar => L P2maxM complU maxCK_L sylR maxNR_H not_t2'H. have [[PmaxM notP1maxM] [hallU hallK _]] := (setDP P2maxM, complU). have q_pr: prime q by have [_ _ _ _ []] := Ptype_structure PmaxM hallK. have [[maxH _] [maxM _]] := (setIdP maxNR_H, setDP PmaxM). have [maxL sCKL] := setIdP maxCK_L; have hallLs := Msigma_Hall maxL. have [_ sUHs] := P2type_signalizer P2maxM complU maxCK_L sylR maxNR_H. set D := H :&: L => defUK [_ sKFD hallD] {r R sylR maxNR_H}. set uniq_q := _ =i _. have{not_t2'H} [q1 t2Hq neq_q]: exists2 q1, q1 \in \tau2(H) & q1 = q -> uniq_q. move: not_t2'H; rewrite negb_and cardG_gt0 all_predC negbK /= has_filter. set s := filter _ _ => nts. have mem_s: s =i \tau2(H). move=> q1; rewrite mem_filter; apply: andb_idr => /= t2q1. by rewrite (partition_pi_mmax maxH) t2q1 !orbT. have [all_q | ] := altP (@allP _ (pred1 q) s); last first. by case/allPn=> q1; rewrite mem_s=> t2q1; move/eqnP=> ne_q1q; exists q1. have s_q1: head q s \in s by case: (s) nts => // q1 s' _; apply: predU1l. exists (head q s) => [|def_q q1]; rewrite -mem_s //. by apply/idP/idP; [apply: all_q | move/eqnP->; rewrite -def_q]. have [A /= Eq2A Eq2A_H] := ex_tau2Elem hallD t2Hq; rewrite -/D in Eq2A. have [b'q qmaxA]: q1 \notin \beta(G) /\ A \in 'E*_q1(G). by have [-> ->] := tau2_not_beta maxH t2Hq. have [sDH s'HD _] := and3P hallD. have [sAH abelA dimA] := pnElemP Eq2A_H; have [qA _] := andP abelA. have [[nsAD _] _ _ _] := tau2_compl_context maxH hallD t2Hq Eq2A. have cKA: A \subset 'C(K). have sFD: 'F(D) \subset D := Fitting_sub _; have sFH := subset_trans sFD sDH. have cFF: abelian 'F(D). exact: sigma'_nil_abelian maxH sFH (pgroupS sFD s'HD) (Fitting_nil _). exact: sub_abelian_cent2 cFF (Fitting_max nsAD (pgroup_nil qA)) sKFD. have sAL: A \subset L := subset_trans cKA sCKL. pose Ks := 'C_(M`_\sigma)(K). have [PmaxL hallKs defK]: [/\ L \in 'M_'P, \kappa(L).-Hall(L) Ks & 'C_(L`_\sigma)(Ks) = K]. - have [L1 [? _] [defL1 [? _] [? _] _ _]] := Ptype_embedding PmaxM hallK. suffices ->: L = L1 by []; apply/set1P; rewrite defL1 // in maxCK_L. by apply/nElemP; exists q; rewrite p1ElemE // !inE subxx eqxx. have sKLs: K \subset L`_\sigma by rewrite -defK subsetIl. have sLq: q \in \sigma(L). by rewrite -pnatE // -pgroupE (pgroupS sKLs) ?pcore_pgroup. have sLq1: q1 \in \sigma(L). apply: contraLR sLq => s'Lq1; rewrite -negnK negbK /= -pnatE // -pgroupE. have s'LA: \sigma(L)^'.-group A by apply: pi_pgroup qA _. have [E hallE sAE] := Hall_superset (mmax_sol maxL) sAL s'LA. have EqA_E: A \in 'E_q1^2(E) by apply/pnElemP. have [[sEL s'E _] t2Lq1] := (and3P hallE, sigma'2Elem_tau2 maxL hallE EqA_E). have [_ [sCAE _ _] _ _] := tau2_compl_context maxL hallE t2Lq1 EqA_E. by apply: pgroupS (subset_trans _ sCAE) s'E; rewrite centsC. have sALs: A \subset L`_\sigma by rewrite sub_Hall_pcore ?(pi_pgroup qA). have solL: solvable L`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxL). pose Q := 'O_q(L)%G; have{solL} [Ds hallDs] := Hall_exists q^' solL. have sQFL: Q \subset 'F(L) by rewrite -[gval Q]p_core_Fitting pcore_sub. have [sAFL sylQ]: A \subset 'F(L) /\ q.-Sylow(L) Q. have [defLF | neqLF] := eqVneq L`_\F L`_\sigma. split; first by rewrite (subset_trans sALs) // -defLF Fcore_sub_Fitting. by rewrite Fcore_pcore_Sylow // defLF mem_primes q_pr cardG_gt0 cardSg. have [_ /(_ _ Ds hallKs neqLF)] := Fcore_structure maxL. rewrite /= defK -/q -/Q; case=> // _ _ [-> _ nsQ0L] _ [_ _ [_ _ <-] _]. rewrite subsetI sALs sub_astabQ quotient_cents // (subset_trans sAL) //. exact: normal_norm nsQ0L. have{sLq1} neqHL: H :!=: L. by apply: contraTneq t2Hq => ->; rewrite negb_and negbK /= sLq1. have def_q1: q1 = q. have uniqQ: Q \in 'U. have [_ _ _ [_ uniqQ _] _] := Ptype_structure PmaxL hallKs. apply/uniq_mmaxP; exists L; case/uniqQ: sylQ => //=; rewrite defK. by rewrite pi_of_prime ?inE. apply: contraNeq neqHL => q'q1. rewrite (eq_uniq_mmax (def_uniq_mmax _ maxL sAL) maxH sAH) //. rewrite (cent_uniq_Uniqueness uniqQ) ?(rank_abelem abelA) ?dimA //. rewrite (sub_nilpotent_cent2 (Fitting_nil L)) //. exact: pnat_coprime (pcore_pgroup _ _) (pi_pgroup qA _). split=> //; first exact: neq_q. rewrite {q1 neq_q}def_q1 in qA Eq2A Eq2A_H t2Hq abelA dimA qmaxA b'q. have{} b'q: q \notin \beta(L) by rewrite -predI_sigma_beta // inE /= sLq. have P1maxL: L \in 'M_'P1. apply: contraR b'q => notP1maxL. by have [_ _ _ _ [|<- //]] := Ptype_structure PmaxL hallKs; apply/setDP. have nilLs: nilpotent L`_\sigma. rewrite (sameP (Fcore_eq_Msigma maxL) eqP); apply: contraR b'q => neqLF. have [_ /(_ _ Ds hallKs neqLF)] := Fcore_structure maxL. by rewrite /= defK -/q -/Q; case=> // _ [_ _ _ ->] _ _ _. have defL': L^`(1) = L`_\sigma. have [Us complUs] := ex_kappa_compl maxL hallKs. have [_ [|<- _ _ _ _]] := kappa_structure maxL complUs. by rewrite (trivg_kappa maxL hallKs) //; case/setDP: PmaxL. suffices ->: Us :=: 1 by rewrite sdprodg1. by apply/eqP; rewrite (trivg_kappa_compl maxL complUs). have [ntK sKLs']: K :!=: 1 /\ K \subset L`_\sigma^`(1). by rewrite -defL' -defK; case/Ptype_cyclics: hallKs. have [sQL qQ _] := and3P sylQ. have not_cQQ: ~~ abelian Q. have sKL: K \subset L := subset_trans sKLs (pcore_sub _ _). have sKQ: K \subset Q by rewrite (sub_Hall_pcore sylQ) /pgroup ?pnat_id. have sQLs: Q \subset L`_\sigma by rewrite sub_Hall_pcore ?(pi_pgroup qQ). have defLs: 'O_q^'(L`_\sigma) * Q = L`_\sigma. rewrite -(setIidPl sQLs) pcore_setI_normal ?pcore_normal //. by have [_] := dprodP (nilpotent_pcoreC q^' nilLs); rewrite pcoreNK. apply: contra ntK => cQQ; rewrite -subG1 /= -(derG1P cQQ) -subsetIidl. rewrite -(pprod_focal_coprime defLs) ?subsetIidl ?pcore_normal //. by rewrite coprime_sym (coprimeSg sKQ) ?coprime_pcoreC. pose X := 'C_A(H`_\sigma)%G. have [sXA cHsX]: X \subset A /\ X \subset 'C(H`_\sigma) by apply/subsetIP. have{not_cQQ} oX: #|X| = q. by have [_ []] := nonabelian_tau2 maxH hallD t2Hq Eq2A qQ not_cQQ. have neqXK: X :!=: K. apply: contraNneq neqHL => defX; rewrite (eq_mmax maxH maxL) //. have [_ <- _ _] := sdprodP (sdprod_sigma maxH hallD). by rewrite mulG_subG subsetIr (subset_trans _ sCKL) // centsC -defX. have{neqXK sXA} not_sXM: ~~ (X \subset M). apply: contra neqXK => sXM; rewrite eqEcard oX leqnn andbT; apply/joing_idPl. have [[sKM kK _] cKX] := (and3P hallK, subset_trans sXA cKA). apply: sub_pHall hallK _ (joing_subl _ _) _; last by rewrite join_subG sKM. by rewrite /= (cent_joinEr cKX) pgroupM {2}/pgroup oX andbb. have{not_sXM} not_sCUM: ~~ ('C(U) \subset M). exact: contra (subset_trans (centsS sUHs cHsX)) not_sXM. apply/pgroupP=> r r_pr _; apply: contra not_sCUM => /= t2Mr. have [hallUK _ _ _ _] := kappa_compl_context maxM complU. have [[B Er2B _] [sUKM _]] := (ex_tau2Elem hallUK t2Mr, andP hallUK). have [[nsBUK _] [sCBUK _ _] _ _ ] := tau2_compl_context maxM hallUK t2Mr Er2B. apply: subset_trans (centS _) (subset_trans sCBUK sUKM). have [sBUK /andP[rB _] _] := pnElemP Er2B. have maxU_UK := Hall_max (pHall_subl (joing_subl _ _) sUKM hallU). rewrite (normal_sub_max_pgroup maxU_UK) // (pi_pgroup rB) //. apply: contraL t2Mr; rewrite negb_and negbK /= inE /=. by case: (r \in _) => //=; move/rank_kappa->. 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)