proposition: Proposition exponent_odd_nil23 gT (R : {group gT}) p : p.-group R -> odd #|R| -> nil_class R <= 2 + (p > 3) -> [/\ exponent 'Ohm_1(R) %| p & R^`(1) \subset 'Ohm_1(R) -> {in R &, {morph expgn^~ p : x y / x * y}}].
proof: Proof. move=> pR oddR classR. pose f n := 'C(n, 3); pose g n := 'C(n, 3).*2 + 'C(n, 2). have fS n: f n.+1 = 'C(n, 2) + f n by rewrite /f binS addnC. have gS n: g n.+1 = 'C(n, 2).*2 + 'C(n, 1) + g n. by rewrite /g !binS doubleD -!addnA; do 3!nat_congr. have [-> | ntR] := eqsVneq R 1. rewrite Ohm1 exponent1 der_sub dvd1n; split=> // _ _ _ /set1P-> /set1P->. by rewrite !(mulg1, expg1n). have{ntR} [p_pr p_dv_R _] := pgroup_pdiv pR ntR. have pdivbin2: p %| 'C(p, 2). by rewrite prime_dvd_bin //= odd_prime_gt2 // (dvdn_odd p_dv_R). have p_dv_fp: p > 3 -> p %| f p by move=> pgt3; apply: prime_dvd_bin. have p_dv_gp: p > 3 -> p %| g p. by move=> pgt3; rewrite dvdn_add // -muln2 dvdn_mulr // p_dv_fp. have exp_dv_p x m (S : {group gT}): exponent S %| p -> p %| m -> x \in S -> x ^+ m = 1. - move=> expSp p_dv_m Sx; apply/eqP; rewrite -order_dvdn. by apply: dvdn_trans (dvdn_trans expSp p_dv_m); apply: dvdn_exponent. have p3_L21: p <= 3 -> {in R & &, forall u v w, [~ u, v, w] = 1}. move=> lep3 u v w Ru Rv Rw; rewrite (ltnNge 3) lep3 nil_class2 in classR. by apply/eqP/commgP; red; rewrite (centerC Rw) // (subsetP classR) ?mem_commg. have{fS gS} expMR_fg: {in R &, forall u v n (r := [~ v, u]), (u * v) ^+ n = u ^+ n * v ^+ n * r ^+ 'C(n, 2) * [~ r, u] ^+ f n * [~ r, v] ^+ g n}. - move=> u v Ru Rv n r; have Rr: r \in R by apply: groupR. have cRr: {in R &, forall x y, commute x [~ r, y]}. move=> x y Rx Ry /=; red; rewrite (centerC Rx) //. have: [~ r, y] \in 'L_3(R) by rewrite !mem_commg. by apply: subsetP; rewrite -nil_class3 (leq_trans classR) // !ltnS leq_b1. elim: n => [|n IHn]; first by rewrite !mulg1. rewrite 3!expgSr {}IHn -!mulgA (mulgA (_ ^+ f n)); congr (_ * _). rewrite -commuteM; try by apply: commuteX; red; rewrite cRr ?groupM. rewrite -mulgA; do 2!rewrite (mulgA _ u) (commgC _ u) -2!mulgA. congr (_ * (_ * _)); rewrite (mulgA _ v). have ->: [~ v ^+ n, u] = r ^+ n * [~ r, v] ^+ 'C(n, 2). elim: n => [|n IHn]; first by rewrite comm1g mulg1. rewrite !expgS commMgR -/r {}IHn commgX; last exact: cRr. rewrite binS bin1 addnC expgD -2!mulgA; congr (_ * _); rewrite 2!mulgA. by rewrite commuteX2 // /commute cRr. rewrite commXg 1?commuteX2 -?[_ * v]commuteX; try exact: cRr. rewrite mulgA {1}[mulg]lock mulgA -mulgA -(mulgA v) -!expgD -fS -lock. rewrite -{2}(bin1 n) addnC -binS -2!mulgA (mulgA _ v) (commgC _ v). rewrite -commuteX; last by red; rewrite cRr ?(Rr, groupR, groupX, groupM). rewrite -3!mulgA; congr (_ * (_ * _)); rewrite 2!mulgA. rewrite commXg 1?commuteX2; try by red; rewrite cRr 1?groupR. by rewrite -!mulgA -!expgD addnCA binS addnAC addnn addnC -gS. have expR1p: exponent 'Ohm_1(R) %| p. elim: _.+1 {-2 4}R (ltnSn #|R|) (subxx R) => // n IHn Q leQn sQR. rewrite (OhmE 1 (pgroupS sQR pR)) expn1 -sub_LdivT. rewrite gen_set_id ?subsetIr //. apply/group_setP; rewrite !inE group1 expg1n /=. split=> // x y /LdivP[Qx xp1] /LdivP[Qy yp1]; rewrite !inE groupM //=. have sxQ: <[x]> \subset Q by rewrite cycle_subG. have [{sxQ}defQ|[S maxS /= sxS]] := maximal_exists sxQ. rewrite expgMn; first by rewrite xp1 yp1 mulg1. by apply: (centsP (cycle_abelian x)); rewrite ?defQ. have:= maxgroupp maxS; rewrite properEcard => /andP[sSQ ltSQ]. have pQ := pgroupS sQR pR; have pS := pgroupS sSQ pQ. have{ltSQ leQn} ltSn: #|S| < n by apply: leq_trans ltSQ _. have expS1p := IHn _ ltSn (subset_trans sSQ sQR). have defS1 := Ohm1Eexponent p_pr expS1p; move/exp_dv_p: expS1p => expS1p. have nS1Q: [~: Q, 'Ohm_1(S)] \subset 'Ohm_1(S). by rewrite commg_subr gFnorm_trans ?normal_norm // (p_maximal_normal pQ). have S1x : x \in 'Ohm_1(S) by rewrite defS1 !inE -cycle_subG sxS xp1 /=. have S1yx : [~ y, x] \in 'Ohm_1(S) by rewrite (subsetP nS1Q) ?mem_commg. have S1yxx : [~ y, x, x] \in 'Ohm_1(S) by rewrite groupR. have S1yxy : [~ y, x, y] \in 'Ohm_1(S). by rewrite -invg_comm groupV (subsetP nS1Q) 1?mem_commg. rewrite expMR_fg ?(subsetP sQR) //= xp1 yp1 expS1p ?mul1g //. case: (leqP p 3) => [p_le3 | p_gt3]; last by rewrite ?expS1p ?mul1g; auto. by rewrite !p3_L21 // ?(subsetP sQR) // !expg1n mulg1. split=> // sR'R1 x y Rx Ry; rewrite -[x ^+ p * _]mulg1 expMR_fg // -2!mulgA //. have expR'p := exp_dv_p _ _ _ (dvdn_trans (exponentS sR'R1) expR1p). congr (_ * _); rewrite expR'p ?mem_commg // mul1g. case: (leqP p 3) => [p_le3 | p_gt3]. by rewrite !p3_L21 // ?(subsetP sQR) // !expg1n mulg1. by rewrite !expR'p 1?mem_commg ?groupR ?mulg1; auto. 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)