proposition: Proposition p2Elem_mmax M p A : M \in 'M -> A \in 'E_p^2(M) -> 'C(A) \subset M /\ ([forall A0 in 'E_p^1(A), 'M('N(A0)) != [set M]] -> [/\ p \in \sigma(M), M`_\alpha = 1 & nilpotent M`_\sigma]).
proof: Proof. move=> maxM Ep2A; have p_pr := pnElem_prime Ep2A. have [sAM abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have [EpAnonuniq |] := altP forall_inP; last first. rewrite negb_forall_in; case/exists_inP=> A0 EpA0; rewrite negbK. case/eqP/mem_uniq_mmax=> _ sNA0_M; rewrite (subset_trans _ sNA0_M) //. by have [sA0A _ _] := pnElemP EpA0; rewrite cents_norm // centS. have{EpAnonuniq} sCMkApCA y: y \in A^# -> [/\ 'r('C_M(<[y]>)) <= 2, p \in \sigma(M)^' -> 'C_(M`_\sigma)[y] \subset 'C_M(A) & p \in \alpha(M)^' -> 'C_(M`_\alpha)[y] \subset 'C_M(A)]. - case/setD1P=> nty Ay; pose Y := <[y]>%G. rewrite -cent_cycle -[<[y]>]/(gval Y). have EpY: Y \in 'E_p^1(A). by rewrite p1ElemE // 2!inE cycle_subG Ay -orderE (abelem_order_p abelA) /=. have [sYA abelY dimY] := pnElemP EpY; have [pY _] := andP abelY. have [H maxNYH neqHM]: exists2 H, H \in 'M('N(Y)) & H \notin [set M]. apply/subsetPn; rewrite subset1 negb_or EpAnonuniq //=. apply/set0Pn; have [|H] := (@mmax_exists _ 'N(Y)); last by exists H. rewrite mFT_norm_proper ?(mFT_pgroup_proper pY) //. by rewrite -rank_gt0 (rank_abelem abelY) dimY. have{maxNYH} [maxH sNYH] := setIdP maxNYH; rewrite inE -val_eqE /= in neqHM. have ->: 'r('C_M(Y)) <= 2. apply: contraR neqHM; rewrite -ltnNge => rCMYgt2. have uniqCMY: 'C_M(Y)%G \in 'U. by rewrite rank3_Uniqueness ?(sub_mmax_proper maxM) ?subsetIl. have defU: 'M('C_M(Y)) = [set M] by apply: def_uniq_mmax; rewrite ?subsetIl. rewrite (eq_uniq_mmax defU maxH) ?subIset //. by rewrite orbC (subset_trans (cent_sub Y)). have [cAMs cAMa] := nonuniq_p2Elem_cent_sigma maxM maxH neqHM Ep2A EpY sNYH. do 2!rewrite {1}subsetI {1}(subset_trans (subsetIl _ _) (pcore_sub _ _)). have sCYH: 'C(Y) \subset H := subset_trans (cent_sub Y) sNYH. by split=> // [/cAMs | /cAMa]; rewrite centsC; apply/subset_trans/setIS. have ntA: A :!=: 1 by rewrite -rank_gt0 (rank_abelem abelA) dimA. have ncycA: ~~ cyclic A by rewrite (abelem_cyclic abelA) dimA. have rCMAle2: 'r('C_M(A)) <= 2. have [y Ay]: exists y, y \in A^# by apply/set0Pn; rewrite setD_eq0 subG1. have [rCMy _ _] := sCMkApCA y Ay; apply: leq_trans rCMy. by rewrite rankS // setIS // centS // cycle_subG; case/setIdP: Ay. have sMp: p \in \sigma(M). apply: contraFT (ltnn 1) => sM'p; rewrite -dimA -(rank_abelem abelA). suffices cMsA: A \subset 'C(M`_\sigma). by rewrite -(setIidPl cMsA) sub'cent_sigma_rank1 // (pi_pgroup pA). have nMsA: A \subset 'N(M`_\sigma) by rewrite (subset_trans sAM) ?gFnorm. rewrite centsC /= -(coprime_abelian_gen_cent1 _ _ nMsA) //; last first. exact: pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _). rewrite gen_subG; apply/bigcupsP=> y; case/sCMkApCA=> _ sCMsyCA _. by rewrite (subset_trans (sCMsyCA sM'p)) ?subsetIr. have [P sylP sAP] := Sylow_superset sAM pA; have [sPM pP _] := and3P sylP. pose Z := 'Ohm_1('Z(P)). have sZA: Z \subset A. have maxA: A \in 'E*_p('C_M(A)). have sACMA: A \subset 'C_M(A) by rewrite subsetI sAM. rewrite (subsetP (p_rankElem_max _ _)) // !inE abelA sACMA. rewrite eqn_leq logn_le_p_rank /=; last by rewrite !inE sACMA abelA. by rewrite dimA (leq_trans (p_rank_le_rank _ _)). rewrite [Z](OhmE 1 (pgroupS (center_sub P) pP)) gen_subG. rewrite -(pmaxElem_LdivP p_pr maxA) -(setIA M) setIid setSI //=. by rewrite setISS // centS. have{ntA} ntZ: Z != 1. by rewrite Ohm1_eq1 (center_nil_eq1 (pgroup_nil pP)) (subG1_contra sAP). have rPle2: 'r(P) <= 2. have [z Zz ntz]: exists2 z, z \in Z & z \notin [1]. by apply/subsetPn; rewrite subG1. have [|rCMz _ _] := sCMkApCA z; first by rewrite inE ntz (subsetP sZA). rewrite (leq_trans _ rCMz) ?rankS // subsetI sPM centsC cycle_subG. by rewrite (subsetP _ z Zz) // gFsub_trans ?subsetIr. have aM'p: p \in \alpha(M)^'. by rewrite !inE -leqNgt -(p_rank_Sylow sylP) -rank_pgroup. have sMaCMA: M`_\alpha \subset 'C_M(A). have nMaA: A \subset 'N(M`_\alpha) by rewrite (subset_trans sAM) ?gFnorm. rewrite -(coprime_abelian_gen_cent1 _ _ nMaA) //; last first. exact: (pnat_coprime (pcore_pgroup _ _) (pi_pnat pA _)). rewrite gen_subG; apply/bigcupsP=> y; case/sCMkApCA=> _ _ sCMayCA. by rewrite (subset_trans (sCMayCA aM'p)) ?subsetIr. have Ma1: M`_\alpha = 1. have [q q_pr rMa]:= rank_witness M`_\alpha. apply: contraTeq rCMAle2; rewrite -ltnNge -rank_gt0 rMa p_rank_gt0 => piMa_q. have aMq: q \in \alpha(M) := pnatPpi (pcore_pgroup _ _) piMa_q. apply: leq_trans (rankS sMaCMA); rewrite rMa. have [Q sylQ] := Sylow_exists q M`_\alpha; rewrite -(p_rank_Sylow sylQ). by rewrite (p_rank_Sylow (subHall_Sylow (Malpha_Hall maxM) aMq sylQ)). have nilMs: nilpotent M`_\sigma. rewrite (nilpotentS (Msigma_der1 maxM)) // (isog_nil (quotient1_isog _)). by rewrite -Ma1 Malpha_quo_nil. rewrite (subset_trans (cents_norm (centS sZA))) ?(mmax_normal maxM) //=. have{} sylP: p.-Sylow(M`_\sigma) P. apply: pHall_subl _ (pcore_sub _ _) sylP. by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) // (pi_pgroup pP). by rewrite (nilpotent_Hall_pcore _ sylP) ?gFnormal_trans. 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)