proposition: Corollary rank2_der1_cent_chief gT p (G Gs U V : {group gT}) : odd #|G| -> solvable G -> Gs <| G -> 'r_p(Gs) <= 2 -> chief_factor G V U -> p.-group (U / V) -> U \subset Gs -> G^`(1) \subset 'C(U / V | 'Q).
proof: Proof. move=> oddG solG nsGsG rGs chiefUf pUf sUGs. wlog Gs_p'_1: gT G Gs U V oddG solG nsGsG rGs chiefUf pUf sUGs / 'O_p^'(Gs) = 1. pose K := 'O_p^'(Gs)%G; move/(_ _ (G / K) (Gs / K) (U / K) (V / K))%G. rewrite trivg_pcore_quotient quotient_odd ?quotient_sol ?quotientS //. have p'K: p^'.-group K := pcore_pgroup p^' Gs. have tiUfK := coprime_TIg (pnat_coprime pUf (quotient_pgroup V p'K)). have nsKG: K <| G by apply: gFnormal_trans. have [[sG'G sGsG] nKG] := (der_sub 1 G, normal_sub nsGsG, normal_norm nsKG). have{sGsG} [nKG' nKGs] := (subset_trans sG'G nKG, subset_trans sGsG nKG). case/andP: chiefUf; case/maxgroupP; case/andP=> ltVU nVG maxV nsUG. have [sUG nUG] := andP nsUG; have [sVU not_sUV] := andP ltVU. have [nUG' nVG'] := (subset_trans sG'G nUG, subset_trans sG'G nVG). have [sVG nVU] := (subset_trans sVU sUG, subset_trans sUG nVG). have [nKU nKV] := (subset_trans sUG nKG, subset_trans sVG nKG). have nsVU: V <| U by apply/andP. rewrite p_rank_p'quotient // /chief_factor -quotient_der ?quotient_normal //. rewrite andbT !sub_astabQR ?quotient_norms // -quotientR // => IH. rewrite -quotient_sub1 ?comm_subG // -tiUfK subsetI quotientS ?commg_subr //. rewrite quotientSK ?(comm_subG nVG') // (normC nKV) -quotientSK ?comm_subG //. apply: IH => //=; last first. rewrite -(setIid U) -(setIidPr sVU) -![_ / K](morphim_restrm nKU). by rewrite -(morphim_quotm _ nsVU) morphim_pgroup. apply/maxgroupP; rewrite /proper quotientS ?quotient_norms //= andbT. rewrite quotientSK // -(normC nKV) -quotientSK // -subsetIidl tiUfK. split=> [|Wb]; first by rewrite quotient_sub1. do 2![case/andP]=> sWbU not_sUWb nWbG sVWb; apply/eqP; rewrite eqEsubset sVWb. have nsWbG: Wb <| G / K by rewrite /normal (subset_trans sWbU) ?quotientS. have [W defWb sKW] := inv_quotientN nsKG nsWbG; case/andP=> sWG nWG. rewrite -(setIidPl sWbU) defWb -quotientGI // quotientS //. rewrite (maxV (W :&: U))%G ?normsI //; last first. by rewrite subsetI sVU andbT -(quotientSGK nKV sKW) -defWb. by rewrite andbT /proper subsetIr subsetIidr -(quotientSGK nKU sKW) -defWb. pose R := 'O_p(Gs); have pR: p.-group R := pcore_pgroup p Gs. have nsRG: R <| G by apply: gFnormal_trans. have [[sGsG nGsG] [sRG nRG]] := (andP nsGsG, andP nsRG). have nsRGs: R <| Gs := pcore_normal p Gs; have [sRGs nRGs] := andP nsRGs. have sylR: p.-Sylow(Gs) R. have [solGs oddGs] := (solvableS sGsG solG, oddSg sGsG oddG). have [_ _ p'Gsb] := rank2_der1_complement solGs oddGs rGs. by rewrite /pHall pcore_sub pR -card_quotient //= -(pseries_pop2 p Gs_p'_1). case/andP: (chiefUf); case/maxgroupP; case/andP=> ltVU nVG maxV nsUG. have [sUG nUG] := andP nsUG; have [sVU not_sUV] := andP ltVU. have [sVG nVU] := (subset_trans sVU sUG, subset_trans sUG nVG). have nsVU: V <| U by apply/andP. have nVGs := subset_trans sGsG nVG; have nVR := subset_trans sRGs nVGs. have{sylR} sUfR: U / V \subset R / V. have sylRb: p.-Sylow(Gs / V) (R / V) by rewrite quotient_pHall. by rewrite (sub_normal_Hall sylRb) ?quotientS ?quotient_normal. have pGb: p.-group((G / 'C_G(R))^`(1)). pose A := conj_aut 'O_p(Gs) @* G. have AA: A \subset Aut R := Aut_conj_aut _ G. have isoGbA: G / 'C_G(R) \isog A by rewrite -ker_conj_aut first_isog_loc. have{isoGbA} [f injf defA] := isogP isoGbA; rewrite /= -/A in defA. rewrite /pgroup -(card_injm injf) ?der_sub ?morphim_der //. have [? ?]: odd #|A| /\ solvable A by rewrite -defA !morphim_odd ?morphim_sol. have rR: 'r(R) <= 2 by rewrite (rank_pgroup pR) (leq_trans (p_rankS p sRGs)). by rewrite defA -pgroupE (der1_Aut_rank2_pgroup pR) ?(oddSg sRG). set C := 'C_G(U / V | 'Q). have nUfG: [acts G, on U / V | 'Q] by rewrite actsQ. have nCG: G \subset 'N(C) by rewrite -(setIidPl nUfG) normsGI ?astab_norm. have{pGb sUfR} pGa': p.-group (G / C)^`(1). have nCRG : G \subset 'N('C_G(R)) by rewrite normsI ?normG ?norms_cent. have sCR_C: 'C_G(R) \subset C. rewrite subsetI subsetIl sub_astabQ ?subIset ?nVG ?(centsS sUfR) //=. by rewrite quotient_cents ?subsetIr. have [f /= <-]:= homgP (homg_quotientS nCRG nCG sCR_C). by rewrite -morphim_der //= morphim_pgroup. have irrG: acts_irreducibly (G / C) (U / V) ('Q %% _). by rewrite acts_irr_mod_astab // acts_irrQ // chief_factor_minnormal. have Ga_p_1: 'O_p(G / C) = 1. rewrite (pcore_faithful_irr_act pUf _ irrG) ?modact_faithful //. by rewrite gacentC ?quotientS ?subsetT ?subsetIr //= setICA subsetIl. have sG'G := der_sub 1 G; have nCG' := subset_trans sG'G nCG. rewrite -subsetIidl -{2}(setIidPl sG'G) -setIA subsetIidl -/C. by rewrite -quotient_sub1 /= ?quotient_der //= -Ga_p_1 pcore_max ?der_normal. 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)