proposition: Lemma injm_narrow G H (f : {morphism G >-> rT}) : 'injm f -> H \subset G -> p.-narrow (f @* H) = p.-narrow H.
proof: Proof. move=> injf sHG; rewrite /narrow injm_p_rank //; congr (_ ==> _). apply/set0Pn/set0Pn=> [] [E /setIP[Ep2E maxE]]. exists (invm injf @* E)%G; rewrite -[H](group_inj (morphim_invm injf _)) //. have sEfG: E \subset f @* G. by rewrite (subset_trans _ (morphimS _ sHG)) //; case/pnElemP: Ep2E. by rewrite inE injm_pnElem ?injm_pmaxElem ?injm_invm ?morphimS // Ep2E. have sEG: E \subset G by rewrite (subset_trans _ sHG) //; case/pnElemP: Ep2E. by exists (f @* E)%G; rewrite inE injm_pnElem ?injm_pmaxElem // Ep2E. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finset prime fingroup morphism perm automorphism action) mathcomp(quotient cyclic gfunctor pgroup gproduct center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection4)