proposition: Lemma morphim_pcore_mod pi gT rT (D G : {group gT}) (f : {morphism D >-> rT}) : f @* pcore_mod G pi (F _ G) \subset pcore_mod (f @* G) pi (F _ (f @* G)).
proof: Proof. have sDF: D :&: G \subset 'dom (coset (F _ G)). by rewrite setIC subIset ?gFnorm. have sDFf: D :&: G \subset 'dom (coset (F _ (f @* G)) \o f). by rewrite -sub_morphim_pre ?subsetIl // morphimIdom gFnorm. pose K := 'ker (restrm sDFf (coset (F _ (f @* G)) \o f)). have sFK: 'ker (restrm sDF (coset (F _ G))) \subset K. rewrite /K !ker_restrm ker_comp /= subsetI subsetIl /= -setIA. rewrite -sub_morphim_pre ?subsetIl //. by rewrite morphimIdom !ker_coset (setIidPr _) ?pmorphimF ?gFsub. have sOF := pcore_sub pi (G / F _ G); have sDD: D :&: G \subset D :&: G by []. rewrite -sub_morphim_pre -?quotientE; last first. by apply: subset_trans (gFnorm F _); rewrite morphimS ?pcore_mod_sub. suffices im_fact (H : {group gT}) : F _ G \subset H -> H \subset G -> factm sFK sDD @* (H / F _ G) = f @* H / F _ (f @* G). - rewrite -2?im_fact ?pcore_mod_sub ?gFsub //; try by rewrite -{1}[F _ G]ker_coset morphpreS ?sub1G. by rewrite quotient_pcore_mod morphim_pcore. move=> sFH sHG; rewrite -(morphimIdom _ (H / _)) /= {2}morphim_restrm setIid. rewrite -morphimIG ?ker_coset //. rewrite -(morphim_restrm sDF) morphim_factm morphim_restrm. by rewrite morphim_comp -quotientE -setIA morphimIdom (setIidPr _). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)