proposition: Lemma cprod_by_uniq : exists f : {morphism G >-> cprod_by}, [/\ isom G C f, f @* GH = CH & f @* GK = CK].
proof: Proof. have [_ defGHK cGKH] := cprodP defG. have AutZinH := Aut_sub_fullP sZH AutZHfull. have [fH injfH defGH]:= isogP (isog_symr isoGH). have [fK injfK defGK]:= isogP (isog_symr isoGK). have sfHZfK: fH @* 'Z(H) \subset fK @* K. by rewrite injm_center //= defGH defGK -ziGHK subsetIr. have gzZ_id: gz @* 'Z(H) = invm injfK @* (fH @* 'Z(H)). apply: gzZ_lone => /=. rewrite injm_center // defGH -ziGHK sub_morphim_pre /= ?defGK ?subsetIr //. by rewrite setIC morphpre_invm injm_center // defGK setIS 1?centsC. rewrite -morphim_comp. apply: isog_trans (sub_isog _ _); first by rewrite isog_sym sub_isog. by rewrite -sub_morphim_pre. by rewrite !injm_comp ?injm_invm. have: 'dom (invm injfH \o fK \o gz) = 'Z(H). rewrite /dom /= -(morphpreIdom gz); apply/setIidPl. by rewrite -2?sub_morphim_pre // gzZ_id morphim_invmE morphpreK ?morphimS. case/domP=> gzH [def_gzH ker_gzH _ im_gzH]. have{ker_gzH} injgzH: 'injm gzH by rewrite ker_gzH !injm_comp ?injm_invm. have{AutZinH} [|gH [injgH gH_H def_gH]] := AutZinH _ injgzH. by rewrite im_gzH !morphim_comp /= gzZ_id !morphim_invmE morphpreK ?injmK. have: 'dom (fH \o gH) = H by rewrite /dom /= -{3}gH_H injmK. case/domP=> gfH [def_gfH ker_gfH _ im_gfH]. have{im_gfH} gfH_H: gfH @* H = GH by rewrite im_gfH morphim_comp gH_H. have cgfHfK: fK @* K \subset 'C(gfH @* H) by rewrite gfH_H defGK. have eq_gfHK: {in 'Z(H), gfH =1 fK \o gz}. move=> z Zz; rewrite def_gfH /= def_gH //= def_gzH /= invmK //. have {Zz}: gz z \in gz @* 'Z(H) by rewrite mem_morphim. rewrite gzZ_id morphim_invmE; case/morphpreP=> _. exact: (subsetP (morphimS _ _)). pose f := xcprodm cgfHfK eq_gfHK. have injf: 'injm f by rewrite injm_xcprodm ker_gfH injm_comp. have fCH: f @* CH = GH by rewrite im_xcprodml gfH_H. have fCK: f @* CK = GK by rewrite im_xcprodmr defGK. have fC: f @* C = G by rewrite im_xcprodm gfH_H defGK defGHK. have [f' [_ ker_f' _ im_f']] := domP (invm_morphism injf) fC. exists f'; rewrite -fCH -fCK !{1}im_f' !{1}morphim_invm ?subsetT //. by split=> //; apply/isomP; rewrite ker_f' injm_invm im_f' -fC im_invm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)