proposition: Theorem critical_odd gT p (G : {group gT}) : p.-group G -> odd #|G| -> G :!=: 1 -> {H : {group gT} | [/\ H \char G, [~: H, G] \subset 'Z(H), nil_class H <= 2, exponent H = p & p.-group 'C(H | [Aut G])]}.
proof: Proof. move=> pG oddG ntG; have [H krH]:= Thompson_critical pG. have [chH sPhiZ sGH_Z scH] := krH; have clH := critical_class2 krH. have sHG := char_sub chH; set D := 'Ohm_1(H)%G; exists D. have chD: D \char G := char_trans (Ohm_char 1 H) chH. have sDH: D \subset H := Ohm_sub 1 H. have sDG_Z: [~: D, G] \subset 'Z(D). rewrite subsetI commg_subl char_norm // commGC. apply: subset_trans (subset_trans sGH_Z _); first by rewrite commgS. by rewrite subIset // orbC centS. rewrite nil_class2 !(subset_trans (commgS D _) sDG_Z) ?(char_sub chD) {sDH}//. have [p_pr p_dv_G _] := pgroup_pdiv pG ntG; have odd_p := dvdn_odd p_dv_G oddG. split=> {chD sDG_Z}//. apply/prime_nt_dvdP=> //; last by rewrite exponent_Ohm1_class2 ?(pgroupS sHG). rewrite -dvdn1 -trivg_exponent /= Ohm1_eq1; apply: contraNneq ntG => H1. by rewrite -(setIidPl (cents1 G)) -{1}H1 scH H1 center1. apply/pgroupP=> q q_pr /Cauchy[] //= f. rewrite astab_ract => /setIdP[Af cDf] ofq; apply: wlog_neg => p'q. suffices: f \in 'C(H | [Aut G]). move/(mem_p_elt (critical_p_stab_Aut krH pG))/pnatP=> -> //. by rewrite ofq. rewrite astab_ract inE Af; apply/astabP=> x Hx; rewrite /= /aperm /=. rewrite nil_class2 in clH; have pH := pgroupS sHG pG. have /p_natP[i ox]: p.-elt x by apply: mem_p_elt Hx. have{ox}: x ^+ (p ^ i) = 1 by rewrite -ox expg_order. elim: i x Hx => [|[|i] IHi] x Hx xp1. - by rewrite [x]xp1 -(autmE Af) morph1. - by apply: (astabP cDf); rewrite (OhmE 1 pH) mem_gen // !inE Hx xp1 eqxx. have expH': {in H &, forall y z, [~ y, z] ^+ p = 1}. move=> y z Hy Hz; apply/eqP. have /setIP[_ cHyz]: [~ y, z] \in 'Z(H) by rewrite (subsetP clH) // mem_commg. rewrite -commXg; last exact/commute_sym/(centP cHyz). suffices /setIP[_ cHyp]: y ^+ p \in 'Z(H) by apply/commgP/(centP cHyp). rewrite (subsetP sPhiZ) // (Phi_joing pH) mem_gen // inE orbC. by rewrite (Mho_p_elt 1) ?(mem_p_elt pH). have Hfx: f x \in H. case/charP: chH => _ /(_ _ (injm_autm Af) (im_autm Af)) <-. by rewrite -{1}(autmE Af) mem_morphim // (subsetP sHG). set y := x^-1 * f x; set z := [~ f x, x^-1]. have Hy: y \in H by rewrite groupM ?groupV. have /centerP[_ Zz]: z \in 'Z(H) by rewrite (subsetP clH) // mem_commg ?groupV. have fy: f y = y. apply: (IHi); first by rewrite groupM ?groupV. rewrite expMg_Rmul; try by apply: commute_sym; apply: Zz; rewrite ?groupV. rewrite -/z bin2odd ?oddX // {3}expnS -mulnA expgM expH' ?groupV //. rewrite expg1n mulg1 expgVn -(autmE Af) -morphX ?(subsetP sHG) //= autmE. rewrite IHi ?mulVg ?groupX // {2}expnS expgM -(expgM x _ p) -expnSr. by rewrite xp1 expg1n. have /eqP: (f ^+ q) x = x * y ^+ q. elim: (q) => [|j IHj]; first by rewrite perm1 mulg1. rewrite expgSr permM {}IHj -(autmE Af). rewrite morphM ?morphX ?groupX ?(subsetP sHG) //= autmE. by rewrite fy expgS mulgA mulKVg. rewrite -{1}ofq expg_order perm1 eq_mulVg1 mulKg -order_dvdn. case: (primeP q_pr) => _ dv_q /dv_q; rewrite order_eq1 -eq_mulVg1. case/pred2P=> // oyq; case/negP: p'q. by apply: (pgroupP pH); rewrite // -oyq order_dvdG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)