proposition: Lemma ext_coprime_quotient_cent (H : {group gT}) : H \subset G -> [acts A, on H | to] -> coprime #|H| #|A| -> solvable H -> 'C_(|to)(A) / H = 'C_(|to / H)(A).
proof: Proof. move=> sHG nHA coHA solH; pose N := 'N_G(H). have nsHN: H <| N by rewrite normal_subnorm. have [sHN nHn] := andP nsHN. have sNG: N \subset G by apply: subsetIl. have nNA: {acts A, on group N | to}. split; rewrite // actsEsd // injm_subnorm ?injm_sdpair1 //=. by rewrite normsI ?norms_norm ?im_sdpair_norm -?actsEsd. rewrite -!(gacentIdom _ A) -quotientInorm -gacentIim setIAC. rewrite -(gacent_actby nNA) gacentEsd -morphpreIim /= -/N. have:= (injm_sdpair1 <[nNA]>, injm_sdpair2 <[nNA]>). set inG := sdpair1 _; set inA := sdpair2 _ => [[injG injA]]. set G' := inG @* N; set A' := inA @* A; pose H' := inG @* H. have defN: 'N(H | to) = A by apply/eqP; rewrite eqEsubset subsetIl. have def_Dq: qact_dom to H = A by rewrite qact_domE. have sAq: A \subset qact_dom to H by rewrite def_Dq. rewrite {2}def_Dq -(gacent_ract _ sAq); set to_q := (_ \ _)%gact. have:= And3 (sdprod_sdpair to_q) (injm_sdpair1 to_q) (injm_sdpair2 to_q). rewrite gacentEsd; set inAq := sdpair2 _; set inGq := sdpair1 _ => /=. set Gq := inGq @* _; set Aq := inAq @* _ => [[q_d iGq iAq]]. have nH': 'N(H') = setT. apply/eqP; rewrite -subTset -im_sdpair mulG_subG morphim_norms //=. by rewrite -actsEsd // acts_actby subxx /= (setIidPr sHN). have: 'dom (coset H' \o inA \o invm iAq) = Aq. by rewrite ['dom _]morphpre_invm /= nH' morphpreT. case/domP=> /= qA [def_qA ker_qA _ im_qA]. have{coHA} coHA': coprime #|H'| #|A'| by rewrite !card_injm. have{ker_qA} injAq: 'injm qA. rewrite {}ker_qA !ker_comp ker_coset morphpre_invm -morphpreIim /= setIC. by rewrite coprime_TIg // -kerE (trivgP injA) morphim1. have{im_qA} im_Aq : qA @* Aq = A' / H'. by rewrite {}im_qA !morphim_comp im_invm. have: 'dom (quotm (sdpair1_morphism <[nNA]>) nsHN \o invm iGq) = Gq. by rewrite ['dom _]morphpre_invm /= quotientInorm. case/domP=> /= qG [def_qG ker_qG _ im_qG]. have{ker_qG} injGq: 'injm qG. rewrite {}ker_qG ker_comp ker_quotm morphpre_invm (trivgP injG). by rewrite quotient1 morphim1. have im_Gq: qG @* Gq = G' / H'. rewrite {}im_qG morphim_comp im_invm morphim_quotm //= -/inG -/H'. by rewrite -morphimIdom setIAC setIid. have{def_qA def_qG} q_J : {in Gq & Aq, morph_act 'J 'J qG qA}. move=> x' a'; case/morphimP=> Hx; case/morphimP=> x nHx Gx -> GHx ->{Hx x'}. case/morphimP=> a _ Aa ->{a'} /=; rewrite -/inAq -/inGq. rewrite !{}def_qG {}def_qA /= !invmE // -sdpair_act //= -/inG -/inA. have Nx: x \in N by rewrite inE Gx. have Nxa: to x a \in N by case: (nNA); move/acts_act->. have [Gxa nHxa] := setIP Nxa. rewrite invmE qactE ?quotmE ?mem_morphim ?def_Dq //=. by rewrite -morphJ /= ?nH' ?inE // -sdpair_act //= actbyE. pose q := sdprodm q_d q_J. have{injAq injGq} injq: 'injm q. rewrite injm_sdprodm injAq injGq /= {}im_Aq {}im_Gq -/Aq . by rewrite -quotientGI ?im_sdpair_TI ?morphimS //= quotient1. rewrite -[inGq @*^-1 _]morphpreIim -/Gq. have sC'G: inG @*^-1 'C_G'(A') \subset G by rewrite !subIset ?subxx. rewrite -[_ / _](injmK iGq) ?quotientS //= -/inGq; congr (_ @*^-1 _). apply: (injm_morphim_inj injq); rewrite 1?injm_subcent ?subsetT //= -/q. rewrite 2?morphim_sdprodml ?morphimS //= im_Gq. rewrite morphim_sdprodmr ?morphimS //= im_Aq. rewrite {}im_qG morphim_comp morphim_invm ?morphimS //. rewrite morphim_quotm morphpreK ?subsetIl //= -/H'. rewrite coprime_norm_quotient_cent ?im_sdpair_norm ?nH' ?subsetT //=. exact: morphim_sol. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)