proposition: Proposition p2_Ohm1_metacyclic gT p (R : {group gT}) : p.-group R -> p > 3 -> logn p #|'Ohm_1(R)| <= 2 -> metacyclic R.
proof: Proof. move=> pR p_gt3 dimR1; move: {2}_.+1 (ltnSn #|R|) => n. elim: n => // n IHn in gT R pR dimR1 *; rewrite ltnS => leRn. have pR1: p.-group 'Ohm_1(R) := pgroupS (Ohm_sub 1 R) pR. have [cRR | not_cRR] := boolP (abelian R). have [b defR typeR] := abelian_structure cRR; move: dimR1 defR. rewrite -(rank_abelian_pgroup pR cRR) -(size_abelian_type cRR) -{}typeR. case: b => [|a [|b []]] //= _; first by move <-; rewrite big_nil metacyclic1. by rewrite big_seq1 => <-; rewrite cyclic_metacyclic ?cycle_cyclic. rewrite big_cons big_seq1; case/dprodP=> _ <- cAB _. apply/existsP; exists <[a]>%G; rewrite cycle_cyclic /=. rewrite /normal mulG_subl mulG_subG normG cents_norm //= quotientMidl. by rewrite quotient_cycle ?cycle_cyclic // -cycle_subG cents_norm. pose R' := R^`(1); pose e := 'Mho^1(R') != 1. have nsR'R: R' <| R := der_normal 1 R; have [sR'R nR'R] := andP nsR'R. have [T EpT]: exists T, T \in 'E_p^1('Mho^e(R') :&: 'Z(R)). apply/p_rank_geP; rewrite -rank_pgroup; last first. by rewrite (pgroupS _ pR) //= setIC subIset ?center_sub. rewrite rank_gt0 (meet_center_nil (pgroup_nil pR)) ?gFnormal_trans //. by case ntR'1: e; rewrite //= Mho0 (sameP eqP derG1P). have [p_gt1 p_pr] := (ltnW (ltnW p_gt3), pnElem_prime EpT). have p_odd: odd p by case/even_prime: p_pr p_gt3 => ->. have{p_odd} oddR: odd #|R| := odd_pgroup_odd p_odd pR. have [sTR'eZ abelT oT] := pnElemPcard EpT; rewrite expn1 in oT. have{sTR'eZ abelT} [[sTR'e sTZ] [pT cTT eT]] := (subsetIP sTR'eZ, and3P abelT). have sTR': T \subset R' := subset_trans sTR'e (Mho_sub e _). have nsTR := sub_center_normal sTZ; have [sTR cRT] := subsetIP sTZ. have cTR: R \subset 'C(T) by rewrite centsC. have{n IHn leRn EpT} metaRb: metacyclic (R / T). have pRb: p.-group (R / T) := quotient_pgroup T pR. have dimRb: logn p #|'Ohm_1(R / T)| <= 2 by apply: quotient_p2_Ohm1. by rewrite IHn ?(leq_trans (ltn_quotient _ _)) ?(nt_pnElem EpT). have{metaRb} [Xb [cycXb nsXbR cycRs]] := metacyclicP metaRb. have{cycRs} [yb defRb]: exists yb, R / T = Xb <*> <[yb]>. have [ys defRs] := cyclicP cycRs; have [yb nXyb def_ys] := cosetP ys. exists yb; rewrite -quotientYK ?cycle_subG ?quotient_cycle // -def_ys -defRs. by rewrite quotientGK. have{sTZ} ntXb: Xb :!=: 1. apply: contraNneq not_cRR => Xb1. by rewrite (cyclic_factor_abelian sTZ) // defRb Xb1 joing1G cycle_cyclic. have [TX defTXb sTTX nsTXR] := inv_quotientN nsTR nsXbR. have{cycXb} [[sTXR nTXR] [xb defXb]] := (andP nsTXR, cyclicP cycXb). have [[x nTx def_xb] [y nTy def_yb]] := (cosetP xb, cosetP yb). have{defTXb} defTX: T <*> <[x]> = TX. rewrite -quotientYK ?cycle_subG ?quotient_cycle // -def_xb -defXb defTXb. by rewrite quotientGK // (normalS _ sTXR). have{yb defRb def_yb} defR: TX <*> <[y]> = R. rewrite -defTX -joingA -quotientYK ?join_subG ?quotientY ?cycle_subG ?nTx //. by rewrite !quotient_cycle // -def_xb -def_yb -defXb -defRb quotientGK. have sXYR: <[x]> <*> <[y]> \subset R by rewrite -defR -defTX -joingA joing_subr. have [Rx Ry]: x \in R /\ y \in R by rewrite -!cycle_subG; apply/joing_subP. have cTXY := subset_trans sXYR cTR; have [cTX cTY] := joing_subP cTXY. have [R'1_1 {e sTR'e} | ntR'1] := eqVneq 'Mho^1(R') 1; last first. have sR'TX: R' \subset TX. rewrite der1_min // -defR quotientYidl ?cycle_subG ?(subsetP nTXR) //. by rewrite quotient_abelian // cycle_abelian. have sTX : T \subset <[x]>. rewrite (subset_trans (subset_trans sTR'e (MhoS e sR'TX))) // /e ntR'1. have{} defTX: T \* <[x]> = TX by rewrite cprodEY // centsC. rewrite -(Mho_cprod 1 defTX) ['Mho^1(_)](trivgP _) ?cprod1g ?Mho_sub //=. rewrite (MhoE 1 pT) gen_subG; apply/subsetP=> tp; case/imsetP=> t Tt ->{tp}. by rewrite inE (exponentP eT). apply/metacyclicP; exists TX; split=> //. by rewrite -defTX (joing_idPr sTX) cycle_cyclic. rewrite -defR quotientYidl ?cycle_subG ?(subsetP nTXR) //. by rewrite quotient_cyclic ?cycle_cyclic. have{R'1_1} eR': exponent R' %| p. have <-: 'Ohm_1(R') = R' by apply/eqP; rewrite trivg_Mho ?R'1_1. rewrite -sub_LdivT (OhmEabelian (pgroupS sR'R pR)) ?subsetIr //. by rewrite (abelianS (OhmS 1 sR'R)) // (p2group_abelian pR1). pose r := [~ x, y]; have Rr: r \in R by apply: groupR. have{defXb ntXb nsXbR} [i def_rb]: exists i, coset T r = (xb ^+ p) ^+ i. have p_xb: p.-elt xb by rewrite def_xb morph_p_elt ?(mem_p_elt pR). have pRbb: p.-group (R / T / 'Mho^1(Xb)) by rewrite !quotient_pgroup. have /andP[_ nXb1R]: 'Mho^1(Xb) <| R / T by apply: gFnormal_trans. apply/cycleP; rewrite -(Mho_p_cycle 1 p_xb) -defXb. apply: coset_idr; first by rewrite (subsetP nXb1R) ?mem_quotient. apply/eqP; rewrite !morphR ?(subsetP nXb1R) ?mem_quotient //=; apply/commgP. red; rewrite -(@centerC _ (R / T / _)) ?mem_quotient // -cycle_subG. rewrite -quotient_cycle ?(subsetP nXb1R) ?mem_quotient // -def_xb -defXb. suffices oXbb: #|Xb / 'Mho^1(Xb)| = p. apply: prime_meetG; first by rewrite oXbb. rewrite (meet_center_nil (pgroup_nil pRbb)) ?quotient_normal //. by rewrite -cardG_gt1 oXbb. rewrite -divg_normal ?Mho_normal //= defXb. rewrite -(mul_card_Ohm_Mho_abelian 1) ?cycle_abelian ?mulnK ?cardG_gt0 //. by rewrite (Ohm1_cyclic_pgroup_prime _ p_xb) ?cycle_cyclic //= -defXb. have{xb def_xb def_rb} [t Tt def_r]: exists2 t, t \in T & r = t * x ^+ (p * i). apply/rcosetP; rewrite -val_coset ?groupX ?morphX //= -def_xb. by rewrite expgM -def_rb val_coset ?groupR // rcoset_refl. have{eR' def_r cTT} defR': R' = <[r]>. have R'r : r \in R' by apply: mem_commg. have cxt: t \in 'C[x] by apply/cent1P; apply: (centsP cRT). have crx: x \in 'C[r] by rewrite cent1C def_r groupM ?groupX ?cent1id. have def_xy: x ^ y = t * x ^+ (p * i).+1. by rewrite conjg_mulR -/r def_r expgS !mulgA (cent1P cxt). have crR : R \subset 'C[r]. rewrite -defR -defTX !join_subG sub_cent1 (subsetP cTR) //= !cycle_subG. rewrite crx cent1C (sameP cent1P commgP); apply/conjg_fixP. rewrite def_r conjMg conjXg conjgE (centsP cRT t) // mulKg conjg_mulR -/r. by rewrite (expgMn _ (cent1P crx)) (expgM r) (exponentP eR') ?expg1n ?mulg1. apply/eqP; rewrite eqEsubset cycle_subG R'r andbT. have nrR : R \subset 'N(<[r]>) by rewrite cents_norm ?cent_cycle. rewrite der1_min // -defR -defTX -joingA. rewrite norm_joinEr ?(subset_trans sXYR) ?normal_norm //. rewrite quotientMl ?(subset_trans sTR) // abelianM quotient_abelian //=. rewrite quotient_cents //= -der1_joing_cycles ?der_abelian //. by rewrite -sub_cent1 (subset_trans sXYR). have [S maxS sR'S] : {S | [max S | S \subset R & cyclic S] & R' \subset S}. by apply: maxgroup_exists; rewrite sR'R /= -/R' defR' cycle_cyclic. case/maxgroupP: maxS; case/andP=> sSR cycS maxS. have nsSR: S <| R := sub_der1_normal sR'S sSR; have [_ nSR] := andP nsSR. apply/existsP; exists S; rewrite cycS nsSR //=. suffices uniqRs1 Us: Us \in 'E_p^1(R / S) -> 'Ohm_1(R) / S = Us. have pRs: p.-group (R / S) := quotient_pgroup S pR. rewrite abelian_rank1_cyclic ?sub_der1_abelian ?(rank_pgroup pRs) // leqNgt. apply: contraFN (ltnn 1) => rRs; have [Us EpUs] := p_rank_geP (ltnW rRs). have [Vs EpVs] := p_rank_geP rRs; have [sVsR abelVs <-] := pnElemP EpVs. have [_ _ <-] := pnElemP EpUs; apply: lognSg; apply/subsetP=> vs Vvs. apply: wlog_neg => notUvs; rewrite -cycle_subG -(uniqRs1 _ EpUs). rewrite (uniqRs1 <[vs]>%G) ?p1ElemE // !inE cycle_subG (subsetP sVsR) //=. by rewrite -orderE (abelem_order_p abelVs Vvs (group1_contra notUvs)). case/pnElemPcard; rewrite expn1 => sUsR _ oUs. have [U defUs sSU sUR] := inv_quotientS nsSR sUsR. have [cycU | {maxS} ncycU] := boolP (cyclic U). by rewrite -[p]oUs defUs (maxS U) ?sUR // trivg_quotient cards1 in p_gt1. have EpU1: 'Ohm_1(U)%G \in 'E_p^2(U). have [u defS] := cyclicP cycS; rewrite defS cycle_subG in sSU. rewrite (Ohm1_extremal_odd (pgroupS sUR pR) (oddSg sUR oddR) _ sSU) //. by rewrite -defS -card_quotient -?defUs // (subset_trans sUR). have defU1: 'Ohm_1(U) = 'Ohm_1(R). apply/eqP; rewrite eqEcard OhmS // (card_pnElem EpU1). by rewrite (card_pgroup pR1) leq_exp2l. apply/eqP; rewrite eqEcard oUs defUs -{1}defU1 quotientS ?Ohm_sub //. rewrite dvdn_leq ?cardG_gt0 //; case/pgroup_pdiv: (quotient_pgroup S pR1) => //. rewrite -subG1 quotient_sub1 ?(gFsub_trans _ nSR) //. apply: contraL (cycS) => sR1S; rewrite abelian_rank1_cyclic ?cyclic_abelian //. rewrite -ltnNge (rank_pgroup (pgroupS sSR pR)); apply/p_rank_geP. by exists 'Ohm_1(U)%G; rewrite -(setIidPr sSU) pnElemI inE EpU1 inE /= defU1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)