proposition: Theorem prime_Frobenius_sol_kernel_nil gT (G K R : {group gT}) : K ><| R = G -> solvable G -> prime #|R| -> 'C_K(R) = 1 -> nilpotent K.
proof: Proof. move=> defG solG R_pr regR. elim: {K}_.+1 {-2}K (ltnSn #|K|) => // m IHm K leKm in G defG solG regR *. have [nsKG sRG defKR nKR tiKR] := sdprod_context defG. have [sKG nKG] := andP nsKG. wlog ntK: / K :!=: 1 by case: eqP => [-> _ | _ ->] //; apply: nilpotent1. have [L maxL _]: {L : {group gT} | maxnormal L K G & [1] \subset L}. by apply: maxgroup_exists; rewrite proper1G ntK norms1. have [ltLK nLG]:= andP (maxgroupp maxL); have [sLK not_sKL]:= andP ltLK. have{m leKm IHm}nilL: nilpotent L. pose G1 := L <*> R; have nLR := subset_trans sRG nLG. have sG1G: G1 \subset G by rewrite join_subG (subset_trans sLK). have defG1: L ><| R = G1. by rewrite sdprodEY //; apply/eqP; rewrite -subG1 -tiKR setSI. apply: (IHm _ _ _ defG1); rewrite ?(solvableS sG1G) ?(oddSg sG1G) //. exact: leq_trans (proper_card ltLK) _. by apply/eqP; rewrite -subG1 -regR setSI. have sLG := subset_trans sLK sKG; have nsLG: L <| G by apply/andP. have sLF: L \subset 'F(G) by apply: Fitting_max. have frobG: [Frobenius G = K ><| R] by apply/prime_FrobeniusP. have solK := solvableS sKG solG. have frobGq := Frobenius_quotient frobG solK nsLG not_sKL. suffices sKF: K \subset 'F(K) by apply: nilpotentS sKF (Fitting_nil K). apply: subset_trans (chief_stab_sub_Fitting solG nsKG). rewrite subsetI subxx; apply/bigcapsP=> [[X Y] /= /andP[chiefXY sXF]]. set V := X / Y; have [maxY nsXG] := andP chiefXY. have [ltYX nYG] := andP (maxgroupp maxY); have [sYX _]:= andP ltYX. have [sXG nXG] := andP nsXG; have sXK := subset_trans sXF (Fitting_sub K). have minV := chief_factor_minnormal chiefXY. have cVL: L \subset 'C(V | 'Q). apply: subset_trans (subset_trans sLF (Fitting_stab_chief solG _)) _ => //. exact: (bigcap_inf (X, Y)). have nVG: {acts G, on group V | 'Q}. split; last by rewrite ?quotientS ?subsetT. by rewrite actsQ // normal_norm. pose V1 := sdpair1 <[nVG]> @* V. have [p p_pr abelV]: exists2 p, prime p & p.-abelem V. apply/is_abelemP; apply: charsimple_solvable (quotient_sol _ _). exact: minnormal_charsimple minV. exact: nilpotent_sol (nilpotentS sXF (Fitting_nil _)). have abelV1: p.-abelem V1 by rewrite morphim_abelem. have injV1 := injm_sdpair1 <[nVG]>. have ntV1: V1 :!=: 1. by rewrite -cardG_gt1 card_injm // cardG_gt1; case/andP: (mingroupp minV). have nV1_G1 := im_sdpair_norm <[nVG]>. pose rV := morphim_repr (abelem_repr abelV1 ntV1 nV1_G1) (subxx G). have def_kerV: rker rV = 'C_G(V | 'Q). rewrite rker_morphim rker_abelem morphpreIdom morphpreIim -astabEsd //. by rewrite astab_actby setIid. have kerL: L \subset rker rV by rewrite def_kerV subsetI sLG. pose rVq := quo_repr kerL nLG. suffices: K / L \subset rker rVq. rewrite rker_quo def_kerV quotientSGK //= 1?subsetI 1?(subset_trans sKG) //. by rewrite sLG. have irrVq: mx_irreducible rVq. apply/quo_mx_irr; apply/morphim_mx_irr; apply/abelem_mx_irrP. apply/mingroupP; rewrite ntV1; split=> // U1; case/andP=> ntU1 nU1G sU1V. rewrite -(morphpreK sU1V); congr (_ @* _). case/mingroupP: minV => _; apply; last by rewrite sub_morphpre_injm. rewrite -subG1 sub_morphpre_injm ?sub1G // morphim1 subG1 ntU1 /=. set U := _ @*^-1 U1; rewrite -(cosetpreK U) quotient_norms //. have: [acts G, on U | <[nVG]>] by rewrite actsEsd ?subsetIl // morphpreK. rewrite astabs_actby subsetI subxx (setIidPr _) ?subsetIl //=. by rewrite -{1}(cosetpreK U) astabsQ ?normal_cosetpre //= -/U subsetI nYG. have [q q_pr abelKq]: exists2 q, prime q & q.-abelem (K / L). apply/is_abelemP; apply: charsimple_solvable (quotient_sol _ solK). exact: maxnormal_charsimple maxL. case (eqVneq q p) => [def_q | neq_qp]. have sKGq: K / L \subset G / L by apply: quotientS. rewrite rfix_mx_rstabC //; have [_ _]:= irrVq; apply; rewrite ?submx1 //. by rewrite normal_rfix_mx_module ?quotient_normal. rewrite -(rfix_subg _ sKGq) (@rfix_pgroup_char _ p) ?char_Fp -?def_q //. exact: (abelem_pgroup abelKq). suffices: rfix_mx rVq (R / L) == 0. apply: contraLR; apply: (Frobenius_rfix_compl frobGq). apply: pi_pnat (abelem_pgroup abelKq) _. by rewrite inE /= (charf_eq (char_Fp p_pr)). rewrite -mxrank_eq0 (rfix_quo _ _ sRG) (rfix_morphim _ _ sRG). rewrite (rfix_abelem _ _ _ (morphimS _ sRG)) mxrank_eq0 rowg_mx_eq0 -subG1. rewrite (sub_abelem_rV_im _ _ _ (subsetIl _ _)) -(morphpreSK _ (subsetIl _ _)). rewrite morphpreIim -gacentEsd gacent_actby gacentQ (setIidPr sRG) /=. rewrite -coprime_quotient_cent ?(solvableS sXG) ?(subset_trans sRG) //. by rewrite {1}['C_X(R)](trivgP _) ?quotient1 ?sub1G // -regR setSI. by apply: coprimeSg sXK _; apply: Frobenius_coprime frobG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)