proposition: Lemma quotient_p2_Ohm1 gT p (R : {group gT}) : p.-group R -> p > 3 -> logn p #|'Ohm_1(R)| <= 2 -> forall T : {group gT}, T <| R -> logn p #|'Ohm_1(R / T)| <= 2.
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. apply/forall_inP/idPn; rewrite negb_forall_in. case/existsP/ex_mingroup=> T /mingroupP[/andP[nsTR dimRb1] minT]. have [sTR nTR] := andP nsTR; have pT: p.-group T := pgroupS sTR pR. pose card_iso_Ohm := card_isog (gFisog [igFun of @Ohm 1] _). have ntT: T :!=: 1; last have p_pr: prime p by have [] := pgroup_pdiv pT ntT. apply: contraNneq dimRb1 => ->. by rewrite -(card_iso_Ohm _ _ _ _ (quotient1_isog R)). have{minT} dimT: logn p #|T| = 1%N. have [Z EpZ]: exists Z, Z \in 'E_p^1(T :&: 'Z(R)). apply/p_rank_geP; rewrite -rank_pgroup ?(pgroupS (subsetIl T _)) //. by rewrite rank_gt0 (meet_center_nil (pgroup_nil pR)). have [sZ_ZT _ dimZ] := pnElemP EpZ; have [sZT sZZ] := subsetIP sZ_ZT. have{sZZ} nsZR: Z <| R := sub_center_normal sZZ. rewrite -(minT Z) // nsZR; apply: contra dimRb1 => dimRz1. rewrite -(card_iso_Ohm _ _ _ _ (third_isog sZT nsZR nsTR)) /=. rewrite IHn ?quotient_pgroup ?quotient_normal ?(leq_trans _ leRn) //. by rewrite ltn_quotient ?(subset_trans sZT) // (nt_pnElem EpZ). have pRb: p.-group (R / T) by apply: quotient_pgroup. have{IHn} minR (Ub : {group coset_of T}): Ub \subset R / T -> ~~ (logn p #|'Ohm_1(Ub)| <= 2) -> R / T = Ub. - case/inv_quotientS=> // U -> sTU sUR dimUb; congr (_ / T). apply/eqP; rewrite eq_sym eqEcard sUR leqNgt; apply: contra dimUb => ltUR. rewrite IHn ?(pgroupS sUR) ?(normalS _ sUR) ?(leq_trans ltUR) //. by rewrite (leq_trans _ dimR1) ?lognSg ?OhmS. have [dimRb eRb]: logn p #|R / T| = 3 /\ exponent (R / T) %| p. have [Rb_gt2 | Rb_le2] := ltnP 2 'r_p(R / T). have [Ub Ep3Ub] := p_rank_geP Rb_gt2. have [sUbR abelUb dimUb] := pnElemP Ep3Ub; have [_ _ eUb] := and3P abelUb. by rewrite (minR Ub) // (Ohm1_id abelUb) dimUb. rewrite -rank_pgroup // in Rb_le2. have eRb: exponent (R / T) %| p. by rewrite (minR _ (Ohm_sub 1 _)) ?exponent_Ohm1_rank2 ?Ohm_id. split=> //; apply/eqP; rewrite eqn_leq rank2_exponent_p_p3group // ltnNge. by apply: contra (leq_trans _) dimRb1; rewrite lognSg ?Ohm_sub. have ntRb: (R / T) != 1. by rewrite -cardG_gt1 (card_pgroup pRb) dimRb (ltn_exp2l 0) ?prime_gt1. have{dimRb} dimR: logn p #|R| = 4. by rewrite -(Lagrange sTR) lognM ?cardG_gt0 // dimT -card_quotient ?dimRb. have nsR1R: 'Ohm_1(R) <| R := Ohm_normal 1 R; have [sR1R nR1R] := andP nsR1R. have pR1: p.-group 'Ohm_1(R) := pgroupS sR1R pR. 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{} dimR1: logn p #|'Ohm_1(R)| = 2. apply/eqP; rewrite eqn_leq dimR1 -p_rank_abelem; last first. by rewrite abelem_Ohm1 // (p2group_abelian pR1). rewrite ltnNge p_rank_Ohm1 -odd_pgroup_rank1_cyclic //. apply: contra dimRb1 => cycR; have cycRb := quotient_cyclic T cycR. by rewrite (Ohm1_cyclic_pgroup_prime cycRb pRb ntRb) (pfactorK 1). have pRs: p.-group (R / 'Ohm_1(R)) by rewrite quotient_pgroup. have dimRs: logn p #|R / 'Ohm_1(R)| = 2. by rewrite -divg_normal // logn_div ?cardSg // dimR1 dimR. have sR'R1: R^`(1) \subset 'Ohm_1(R). by rewrite der1_min // (p2group_abelian pRs) ?dimRs. have [|_ phiM] := exponent_odd_nil23 pR oddR. by rewrite (leq_trans (nil_class_pgroup pR)) // dimR p_gt3. pose phi := Morphism (phiM sR'R1). suffices: logn p #|R / 'Ohm_1(R)| <= logn p #|T| by rewrite dimT dimRs. have ->: 'Ohm_1(R) = 'ker phi. rewrite -['ker phi]genGid (OhmE 1 pR); congr <<_>>. by apply/setP=> x; rewrite !inE. rewrite (card_isog (first_isog phi)) lognSg //=. apply/subsetP=> _ /morphimP[x _ Rx ->] /=. apply: coset_idr; first by rewrite groupX ?(subsetP nTR). by rewrite morphX ?(subsetP nTR) // (exponentP eRb) // mem_quotient. 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)