proposition: Lemma FTtypeP i M : M \in 'M -> reflect (FTtype_spec i M) (FTtype M == i).
proof: Proof. move=> maxM; pose Ms := M`_\sigma; pose M' := M^`(1); pose H := M`_\F. have [[ntH sHMs sMsM' _] _] := Fcore_structure maxM. apply: (iffP eqP) => [<- | ]; last first. case: i => [// | [[U [[[_ _ defM] _ [U0 [sU0U expU0 frobM]]] _]] | ]]. apply/eqP; rewrite -FTtype_Fmax //; apply: wlog_neg => notFmaxM. have PmaxM: M \in 'M_'P by apply/setDP. apply/FtypeP; split=> // p; apply/idP=> kp. have [X EpX]: exists X, X \in 'E_p^1(U0). apply/p_rank_geP; rewrite p_rank_gt0 -pi_of_exponent expU0 pi_of_exponent. have: p \in \pi(M) by rewrite kappa_pi. rewrite /= -(sdprod_card defM) pi_ofM ?cardG_gt0 //; case/orP=> // Fk. have [[_ sMFMs _ _] _] := Fcore_structure maxM. case/negP: (kappa_sigma' kp). exact: pnatPpi (pcore_pgroup _ _) (piSg sMFMs Fk). have [[sXU0 abelX _] ntX] := (pnElemP EpX, nt_pnElem EpX isT). have kX := pi_pgroup (abelem_pgroup abelX) kp. have [_ sUM _ _ _] := sdprod_context defM. have sXM := subset_trans sXU0 (subset_trans sU0U sUM). have [K hallK sXK] := Hall_superset (mmax_sol maxM) sXM kX. have [ntKs _ _ sKsMF _] := Ptype_cyclics PmaxM hallK; case/negP: ntKs. rewrite -subG1 -(cent_semiregular (Frobenius_reg_ker frobM) sXU0 ntX). by rewrite subsetI sKsMF subIset // centS ?orbT. case=> [[U W K Ks defW [[PtypeM ntU _ _] _ not_sNUM _ _]] | ]. apply/eqP; rewrite -FTtype_P2max // inE andbC. by have [-> _ _ -> _] := typePfacts maxM PtypeM; rewrite negb_or ntU. case=> [[U W K Ks defW [[PtypeM ntU _ _] cUU sNUM]] | ]. have [_ _ _] := typePfacts maxM PtypeM. rewrite (negPf ntU) sNUM FTtype_P1max // cUU /FTtype -/Ms -/M' -/H. by case: ifP => // _; case: (Ms =P M') => // -> _ [//|-> ->]. case=> [[U W K Ks defW [[PtypeM ntU _ _] not_cUU sNUM]] | ]. have [_ _ _] := typePfacts maxM PtypeM. rewrite (negPf ntU) (negPf not_cUU) sNUM FTtype_P1max // /FTtype -/Ms -/M'. by case: ifP => // _; case: (Ms =P M') => // -> _ [//|-> ->]. case=> // [[U K Ks W defW [[PtypeM U_1] _]]]. have [_ _ _] := typePfacts maxM PtypeM. rewrite U_1 eqxx FTtype_P1max //= /FTtype -/Ms -/M' -/H. by case: ifP => // _; case: (Ms =P M') => // -> _ [//|-> _]. have [[U K] /= complU] := kappa_witness maxM; have [hallU hallK _] := complU. have [K1 | ntK] := eqsVneq K 1. have FmaxM: M \in 'M_'F by rewrite -(trivg_kappa maxM hallK) K1. have ->: FTtype M = 1%N by apply/eqP; rewrite -FTtype_Fmax. have ntU: U :!=: 1 by case/(FmaxP maxM complU): FmaxM. have defH: H = Ms. by apply/Fcore_eq_Msigma; rewrite // notP1type_Msigma_nil ?FmaxM. have defM: H ><| U = M. by have [_] := kappa_compl_context maxM complU; rewrite defH K1 sdprodg1. exists U; split. have [_ _ _ cU1U1 exU0] := kappa_structure maxM complU. split=> //; last by rewrite -/Ms -defH in exU0; apply: exU0. exists [group of <<\bigcup_(x in (M`_\sigma)^#) 'C_U[x]>>]. split=> //= [|x Hx]; last by rewrite sub_gen //= -/Ms -defH (bigcup_max x). rewrite -big_distrr /= /normal gen_subG subsetIl. rewrite norms_gen ?normsI ?normG //; apply/subsetP=> u Uu. rewrite inE sub_conjg; apply/bigcupsP=> x Msx. rewrite -sub_conjg -normJ conjg_set1 (bigcup_max (x ^ u)) ?memJ_norm //. by rewrite normD1 (subsetP (gFnorm _ _)) // (subsetP (pHall_sub hallU)). have [|] := boolP [forall (y | y \notin M), 'F(M) :&: 'F(M) :^ y == 1]. move/forall_inP=> TI_F; constructor 1; apply/normedTI_P. rewrite setD_eq0 subG1 mmax_Fcore_neq1 // setTI normD1 gFnorm. split=> // x _; apply: contraR => /TI_F/eqP tiFx. rewrite -setI_eq0 conjD1g -setDIl setD_eq0 -set1gE -tiFx. by rewrite setISS ?conjSg ?Fcore_sub_Fitting. rewrite negb_forall_in => /exists_inP[y notMy ntX]. have [_ _ _ _] := nonTI_Fitting_structure maxM notMy ntX. case=> [[] | [_]]; first by constructor 2. move: #|_| => p; set P := 'O_p(H); rewrite /= -/H => not_cPP cycHp'. case=> [expU | [_]]; [constructor 3 | by rewrite 2!inE FmaxM]. split=> [q /expU | ]. have [_ <- nHU tiHU] := sdprodP defM. by rewrite quotientMidl -(exponent_isog (quotient_isog _ _)). have sylP: p.-Sylow(H) P := nilpotent_pcore_Hall _ (Fcore_nil M). have ntP: P != 1 by apply: contraNneq not_cPP => ->; apply: abelian1. by exists p; rewrite // -p_rank_gt0 -(rank_Sylow sylP) rank_gt0. have PmaxM: M \in 'M_'P by rewrite inE -(trivg_kappa maxM hallK) ntK. have [Mstar _ [_ _ _ [cycW _ _ _ _]]] := Ptype_embedding PmaxM hallK. case=> [[tiV _ _] _ _ defM {Mstar}]. have [_ [_ cycK] [_ nUK _ _ _] _] := BGsummaryA maxM complU; rewrite -/H. case=> [[ntKs defCMK] [_ _ _ _ nilM'H] [sM''F defF /(_ ntK)sFM'] types34]. have hallK_M := pHall_Hall hallK. have [/= [[cUU not_sNUM]]] := BGsummaryC maxM complU ntK; rewrite -/H -/M' -/Ms. case=> cycKs _ sKsH not_cycH [defM' sKsM''] _ [_ _ type2 _]. pose Ks := 'C_H(K); pose W := K <*> Ks; pose V := W :\: (K :|: Ks). have defKs: 'C_Ms(K) = Ks by rewrite -(setIidPr sKsH) setIA (setIidPl sHMs). rewrite {}defKs -/W -/V in ntKs tiV cycW cycKs sKsM'' sKsH defCMK. have{defCMK} prM'K: {in K^#, forall k, 'C_M'[k] = Ks}. have sKsM': Ks \subset M' := subset_trans sKsM'' (der_sub 1 _). move=> k; move/defCMK=> defW; have:= dprod_modr defW sKsM'. have [_ _ _ ->] := sdprodP defM; rewrite dprod1g. by rewrite setIA (setIidPl (der_sub 1 M)). have [sHM' nsM'M] := (subset_trans sHMs sMsM', der_normal 1 M : M' <| M). have hallM': \kappa(M)^'.-Hall(M) M' by apply/(sdprod_normal_pHallP _ hallK). have [sM'M k'M' _] := and3P hallM'. have hallH_M': \pi(H).-Hall(M') H := pHall_subl sHM' sM'M (Fcore_Hall M). have nsHM' := normalS sHM' sM'M (Fcore_normal M). have defW: K \x Ks = W. rewrite dprodEY ?subsetIr //= setIC; apply/trivgP. by have [_ _ _ <-] := sdprodP defM; rewrite setSI ?subIset ?sHM'. have [Ueq1 | ntU] := eqsVneq U 1; last first. have P2maxM: M \in 'M_'P2 by rewrite inE -(trivg_kappa_compl maxM complU) ntU. have ->: FTtype M = 2 by apply/eqP; rewrite -FTtype_P2max. have defH: H = Ms. by apply/Fcore_eq_Msigma; rewrite // notP1type_Msigma_nil ?P2maxM ?orbT. have [//|pr_K tiFM _] := type2; rewrite -defH in defM'. have [_ sUM' _ _ _] := sdprod_context defM'. have MtypeP: of_typeP M U defW by split; rewrite // abelian_nil. have defM'F: M'`_\F = H. apply/eqP; rewrite eqEsubset (Fcore_max hallH_M') ?Fcore_nil // andbT. rewrite (Fcore_max (subHall_Hall hallM' _ (Fcore_Hall _))) ?Fcore_nil //. by move=> p piM'Fp; apply: pnatPpi k'M' (piSg (Fcore_sub _) piM'Fp). exact: gFnormal_trans nsM'M. exists U _ K _ defW; split=> //; split; first by rewrite defM'F. by exists U; split=> // x _; apply: subsetIl. have [_ _ _ _ /(_ ntU)] := kappa_structure maxM complU. by rewrite -/Ms -defH -defM'F. have P1maxM: M \in 'M_'P1 by rewrite -(trivg_kappa_compl maxM complU) Ueq1. have: 2 < FTtype M <= 5 by rewrite -FTtype_P1max. rewrite /FTtype -/H -/Ms; case: ifP => // _; case: eqP => //= defMs _. have [Y hallY nYK]: exists2 Y, \pi(H)^'.-Hall(M') (gval Y) & K \subset 'N(Y). apply: coprime_Hall_exists; first by case/sdprodP: defM. by rewrite (coprime_sdprod_Hall_l defM) (pHall_Hall hallM'). exact: solvableS sM'M (mmax_sol maxM). have{} defM': H ><| Y = M' by apply/(sdprod_normal_p'HallP _ hallY). have MtypeP: of_typeP M Y defW. have [_ sYM' mulHY nHY tiHY] := sdprod_context defM'. do 2!split=> //; rewrite (isog_nil (quotient_isog nHY tiHY)). by rewrite /= -quotientMidl mulHY. have [_ _ _ sNYG [//| defY1 ->]] := typePfacts maxM MtypeP. rewrite defY1; have [Y1 | ntY] := altP (Y :=P: 1); last first. move/esym: sNYG; rewrite (negPf ntY) P1maxM /= => sNYG. have [|_ tiFM prK] := types34; first by rewrite defY1. by case: ifPn; exists Y _ K _ defW. exists Y _ K _ defW; split=> //=. have [|] := boolP [forall (y | y \notin M), 'F(M) :&: 'F(M) :^ y == 1]. move/forall_inP=> TI_F; constructor 1; apply/normedTI_P. rewrite setD_eq0 subG1 mmax_Fcore_neq1 // setTI normD1 gFnorm. split=> // x _; apply: contraR => /TI_F/eqP tiFx. rewrite -setI_eq0 conjD1g -setDIl setD_eq0 -set1gE -tiFx. by rewrite setISS ?conjSg ?Fcore_sub_Fitting. rewrite negb_forall_in => /exists_inP[y notMy ntX]. have [_ _ _ _] := nonTI_Fitting_structure maxM notMy ntX. case=> [[] | [_]]; first by case/idPn; case/setDP: PmaxM. move: #|_| => p; set P := 'O_p(H); rewrite /= -/H => not_cPP cycHp'. have sylP: p.-Sylow(H) P := nilpotent_pcore_Hall _ (Fcore_nil M). have ntP: P != 1 by apply: contraNneq not_cPP => ->; apply: abelian1. have piHp: p \in \pi(H) by rewrite -p_rank_gt0 -(rank_Sylow sylP) rank_gt0. have defH: H = Ms by apply/eqP; rewrite defY1 Y1. rewrite -defMs -defH in defM; have [_ <- nHU tiHU] := sdprodP defM. rewrite quotientMidl -(card_isog (quotient_isog _ _)) //. rewrite -(exponent_isog (quotient_isog _ _)) // exponent_cyclic //=. case=> [K_dv_H1 | []]; [constructor 2 | constructor 3]; exists p => //. by rewrite K_dv_H1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(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 BGsection15)