proposition: Lemma Ohm1_cent_max_normal_abelem Z : odd p -> p.-group G -> [max Z | Z <| G & p.-abelem Z] -> 'Ohm_1('C_G(Z)) = Z.
proof: Proof. move=> p_odd pG; set X := 'Ohm_1('C_G(Z)). case/maxgroupP=> /andP[nsZG abelZ] maxZ. have [sZG nZG] := andP nsZG; have [_ cZZ expZp] := and3P abelZ. have{nZG} nsXG: X <| G by rewrite gFnormal_trans ?norm_normalI ?norms_cent. have cZX : X \subset 'C(Z) by apply/gFsub_trans/subsetIr. have{sZG expZp} sZX: Z \subset X. rewrite [X](OhmE 1 (pgroupS _ pG)) ?subsetIl ?sub_gen //. apply/subsetP=> x Zx; rewrite !inE ?(subsetP sZG) ?(subsetP cZZ) //=. by rewrite (exponentP expZp). suffices{sZX} expXp: (exponent X %| p). apply/eqP; rewrite eqEsubset sZX andbT -quotient_sub1 ?cents_norm //= -/X. have pGq: p.-group (G / Z) by rewrite quotient_pgroup. rewrite (TI_center_nil (pgroup_nil pGq)) ?quotient_normal //= -/X setIC. apply/eqP/trivgPn=> [[Zd]]; rewrite inE -!cycle_subG -cycle_eq1 -subG1 /= -/X. case/andP=> /sub_center_normal nsZdG. have{nsZdG} [D defD sZD nsDG] := inv_quotientN nsZG nsZdG; rewrite defD. have sDG := normal_sub nsDG; have nsZD := normalS sZD sDG nsZG. rewrite quotientSGK ?quotient_sub1 ?normal_norm //= -/X => sDX /negP[]. rewrite (maxZ D) // nsDG andbA (pgroupS sDG) ?(dvdn_trans (exponentS sDX)) //. have sZZD: Z \subset 'Z(D) by rewrite subsetI sZD centsC (subset_trans sDX). by rewrite (cyclic_factor_abelian sZZD) //= -defD cycle_cyclic. pose normal_abelian := [pred A : {group gT} | A <| G & abelian A]. have{nsZG cZZ} normal_abelian_Z : normal_abelian Z by apply/andP. have{normal_abelian_Z} [A maxA sZA] := maxgroup_exists normal_abelian_Z. have SCN_A : A \in 'SCN(G) by apply: max_SCN pG maxA. move/maxgroupp: maxA => /andP[nsAG cAA] {normal_abelian}. have pA := pgroupS (normal_sub nsAG) pG. have{abelZ maxZ nsAG cAA sZA} defA1: 'Ohm_1(A) = Z. have: Z \subset 'Ohm_1(A) by rewrite -(Ohm1_id abelZ) OhmS. by apply: maxZ; rewrite Ohm1_abelem ?gFnormal_trans. have{SCN_A} sX'A: X^`(1) \subset A. have sX_CWA1 : X \subset 'C('Ohm_1(A)) :&: 'C_G(A / 'Ohm_1(A) | 'Q). rewrite subsetI /X -defA1 (Ohm1_stab_Ohm1_SCN_series _ p_odd) //=. by rewrite gFsub_trans ?subsetIr. by apply: subset_trans (der1_stab_Ohm1_SCN_series SCN_A); rewrite commgSS. pose genXp := [pred U : {group gT} | 'Ohm_1(U) == U & ~~ (exponent U %| p)]. apply/idPn=> expXp'; have genXp_X: genXp [group of X] by rewrite /= Ohm_id eqxx. have{genXp_X expXp'} [U] := mingroup_exists genXp_X; case/mingroupP; case/andP. move/eqP=> defU1 expUp' minU sUX; case/negP: expUp'. have{nsXG} pU := pgroupS (subset_trans sUX (normal_sub nsXG)) pG. case gsetU1: (group_set 'Ldiv_p(U)). by rewrite -defU1 (OhmE 1 pU) gen_set_id // -sub_LdivT subsetIr. move: gsetU1; rewrite /group_set 2!inE group1 expg1n eqxx; case/subsetPn=> xy. case/imset2P=> x y /[!inE] /andP[Ux xp1] /andP[Uy yp1] ->{xy}. rewrite groupM //= => nt_xyp; pose XY := <[x]> <*> <[y]>. have{yp1 nt_xyp} defXY: XY = U. have sXY_U: XY \subset U by rewrite join_subG !cycle_subG Ux Uy. rewrite [XY]minU //= eqEsubset Ohm_sub (OhmE 1 (pgroupS _ pU)) //. rewrite /= joing_idl joing_idr genS; last first. by rewrite subsetI subset_gen subUset !sub1set !inE xp1 yp1. apply: contra nt_xyp => /exponentP-> //. by rewrite groupMl mem_gen // (set21, set22). have: <[x]> <|<| U by rewrite nilpotent_subnormal ?(pgroup_nil pU) ?cycle_subG. case/subnormalEsupport=> [defU | /=]. by apply: dvdn_trans (exponent_dvdn U) _; rewrite -defU order_dvdn. set V := <<class_support <[x]> U>>; case/andP=> sVU ltVU. have{genXp minU xp1 sVU ltVU} expVp: exponent V %| p. apply: contraR ltVU => expVp'; rewrite [V]minU //= expVp' eqEsubset Ohm_sub. rewrite (OhmE 1 (pgroupS sVU pU)) genS //= subsetI subset_gen class_supportEr. apply/bigcupsP=> z _; apply/subsetP=> v Vv. by rewrite inE -order_dvdn (dvdn_trans (order_dvdG Vv)) // cardJg order_dvdn. have{A pA defA1 sX'A V expVp} Zxy: [~ x, y] \in Z. rewrite -defA1 (OhmE 1 pA) mem_gen // !inE (exponentP expVp). by rewrite (subsetP sX'A) //= mem_commg ?(subsetP sUX). by rewrite groupMl -1?[x^-1]conjg1 mem_gen // imset2_f // ?groupV cycle_id. have{Zxy sUX cZX} cXYxy: [~ x, y] \in 'C(XY). by rewrite centsC in cZX; rewrite defXY (subsetP (centS sUX)) ?(subsetP cZX). rewrite -defU1 exponent_Ohm1_class2 // nil_class2 -defXY der1_joing_cycles //. by rewrite subsetI {1}defXY !cycle_subG groupR. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)