proposition: Theorem nonFtype_signalizer_base M x : M \in 'M -> x \in M`_\sigma^# -> ~~ ('C[x] \subset M) -> 'N[x] \notin 'M_'F -> [/\ M \in 'M_'F, 'N[x] \in 'M_'P2 & exists2 E : {group gT}, \sigma(M)^'.-Hall(M) E & cyclic (gval E) /\ [Frobenius M = M`_\sigma ><| E]].
proof: Proof. move=> maxM Ms1x not_sCxM notFmaxN; have ell1x := Msigma_ell1 maxM Ms1x. have [[ntx Ms_x] [y cxy notMy]] := (setD1P Ms1x, subsetPn not_sCxM). have SMxM: M \in 'M_\sigma[x] by rewrite inE maxM cycle_subG. have SMxMy: (M :^ y)%G \in 'M_\sigma[x]. by rewrite inE mmaxJ maxM gen_subG -(normP cxy) /= MsigmaJ conjSg sub1set. have neq_MyM: M :^ y != M by rewrite (sameP eqP normP) norm_mmax. have SMx_gt1: #|'M_\sigma[x]| > 1. by rewrite (cardD1 M) SMxM (cardD1 (M :^ y)%G) inE /= SMxMy neq_MyM. have [_ [//|uniqN _ t2Nx]] := FT_signalizer_context ell1x. rewrite inE (negPf notFmaxN) /= => P2maxN /(_ M SMxM)[_ st2NsM _ hallMN]. pose r := pdiv #[x]; have pixr: r \in \pi(#[x]) by rewrite pi_pdiv order_gt1. have t2Nr := pnatPpi t2Nx pixr; have sMr := st2NsM r t2Nr. have [[PmaxN _] [_ s'N_MN _]] := (setDP P2maxN, and3P hallMN). have [K hallK] := Hall_exists \kappa('N[x]) (sigma_compl_sol hallMN). have [U hallU] := Hall_exists \kappa('N[x])^' (sigma_compl_sol hallMN). have hallK_N := subHall_Hall hallMN (@kappa_sigma' _ _) hallK. have [[sKMN kK _] [sUMN k'U _]] := (and3P hallK, and3P hallU). have mulUK: U * K = M :&: 'N[x]. apply/eqP; rewrite eqEcard mulG_subG sUMN sKMN. rewrite coprime_cardMg ?(p'nat_coprime k'U) //= mulnC. by rewrite (card_Hall hallU) (card_Hall hallK) partnC ?cardG_gt0. have complU: kappa_complement 'N[x] U K. split=> //; last by rewrite mulUK groupP. apply: (subHall_Hall hallMN) => [p|]; first by case/norP. rewrite pHallE sUMN /= (card_Hall hallU) eq_sym; apply/eqP. apply: eq_in_partn => p piMNp; rewrite inE /= negb_or /=. by rewrite [~~ _](pnatPpi s'N_MN). have prK: prime #|K| by case/Ptype_structure: hallK_N => // _ _ _ _ []. have ntK: K :!=: 1 by rewrite -cardG_gt1 prime_gt1. have [maxN _] := setDP PmaxN. have [defUK cUU regUK]: [/\ U ><| K = M :&: 'N[x], abelian U & 'C_U(K) = 1]. have [_ defM _ regUK -> //] := kappa_compl_context maxN complU. have [[_ UK _ defUK] _ _ _] := sdprodP defM. by rewrite (cent_semiregular regUK) // defUK; case/sdprodP: defUK => _ <-. have [[R sylR] [s'Nr rrN]] := (Sylow_exists r (M :&: 'N[x]), andP t2Nr). have [[sRMN rR _] sylR_N] := (and3P sylR, subHall_Sylow hallMN s'Nr sylR). have [nsUMN _ _ nUK _] := sdprod_context defUK. have [[sRM sRN] [sKM _]] := (subsetIP sRMN, subsetIP sKMN). have sRU: R \subset U. rewrite (sub_normal_Hall hallU nsUMN sRMN) (pi_pgroup rR) //. by apply: contraL rrN; move/rank_kappa->. have sNRM: 'N(R) \subset M. apply: (norm_noncyclic_sigma maxM sMr rR sRM). rewrite (odd_pgroup_rank1_cyclic rR) ?mFT_odd //. by rewrite (p_rank_Sylow sylR_N) (eqnP rrN). have sylR_U := pHall_subl sRU sUMN sylR. have maxNRM: M \in 'M('N(R)) by rewrite inE maxM. have [L maxCK_L] := mmax_exists (mFT_cent_proper ntK). have FmaxM: M \in 'M_'F; last split=> //. by have [] := P2type_signalizer P2maxN complU maxCK_L sylR_U maxNRM. have nilMs: nilpotent M`_\sigma by rewrite notP1type_Msigma_nil ?FmaxM. have sMsF: M`_\sigma \subset 'F(M) by rewrite Fitting_max ?pcore_normal. have defR: R :=: 'O_r(U) := nilpotent_Hall_pcore (abelian_nil cUU) sylR_U. have nRK: K \subset 'N(R) by rewrite defR gFnorm_trans. have ntR: R :!=: 1. rewrite -rank_gt0 (rank_Sylow sylR_N) p_rank_gt0. by rewrite (partition_pi_mmax maxN) t2Nr !orbT. have not_nilRK: ~~ nilpotent (R <*> K). apply: contra ntR => nilRK; rewrite -subG1 -regUK subsetI sRU. rewrite (sub_nilpotent_cent2 nilRK) ?joing_subl ?joing_subr //. by rewrite (coprimegS sRU) ?(pnat_coprime kK). have{not_nilRK} not_sKMs: ~~ (K \subset M`_\sigma). apply: contra not_nilRK => sKMs; apply: nilpotentS nilMs. by rewrite join_subG (sub_Hall_pcore (Msigma_Hall maxM)) // (pi_pgroup rR). have s'MK: \sigma(M)^'.-group K. rewrite /pgroup pnatE //; apply: contra not_sKMs; rewrite /= -pnatE // => sK. by rewrite (sub_Hall_pcore (Msigma_Hall maxM)). have [E hallE sKE] := Hall_superset (mmax_sol maxM) sKM s'MK. have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have [[_ t1E1 _] [sEM _]] := (and3P hallE1, andP hallE). have E2_1: E2 :=: 1. have [sE2E t2E2 _] := and3P hallE2. rewrite -(setIidPl sE2E) coprime_TIg ?(pnat_coprime t2E2 (pgroupS sEM _)) //. apply: contraR ntR => not_t2'M. have:= tau2_P2type_signalizer P2maxN complU maxCK_L sylR_U maxNRM not_t2'M. case=> _ _ t2'N; rewrite -(setIidPl sRN) coprime_TIg //. by rewrite (pnat_coprime (pi_pgroup rR t2Nr)). have E3_1: E3 :=: 1. have ntX: 'F(M) :&: 'F(M) :^ y != 1. apply/trivgPn; exists x; rewrite // inE mem_conjg !(subsetP sMsF) //. by rewrite /conjg invgK mulgA (cent1P cxy) mulgK. have [_ _ _ defE _] := nonTI_Fitting_structure maxM notMy ntX. by case/defE: complEi. have [cycE defE]: cyclic E /\ E :=: E1. have [_ _ [cycE1 _] [<- _] _] := sigma_compl_context maxM complEi. by rewrite E2_1 E3_1 !sdprod1g. have [ntMs ntE] := (Msigma_neq1 maxM, subG1_contra sKE ntK). have defM := sdprod_sigma maxM hallE. exists E => //; split=> //; apply/Frobenius_semiregularP=> // z Ez. have{Ez} [ntz szE1] := setD1P Ez; rewrite defE -cycle_subG in szE1. pose q := pdiv #[z]; have pizq: q \in \pi(#[z]) by rewrite pi_pdiv order_gt1. have szM: <[z]> \subset M by rewrite (subset_trans _ sEM) ?defE. have [_ k'M] := setIdP FmaxM; have k'q := pnatPpi k'M (piSg szM pizq). have t1q := pnatPpi t1E1 (piSg szE1 pizq). move: pizq; rewrite -p_rank_gt0 => /p_rank_geP[Z]. rewrite /= -(setIidPr szM) pnElemI -setIdE => /setIdP[EqZ sZz]. apply: contraNeq k'q => ntCMsx /=. rewrite unlock inE /= inE /= t1q; apply/exists_inP; exists Z => //. by rewrite (subG1_contra _ ntCMsx) ?setIS //= -cent_cycle centS. 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)