proposition: Lemma iso_quotient_homocyclic_sdprod gT (V G : {group gT}) p m : minnormal V G -> coprime p #|G| -> p.-abelem V -> m > 0 -> is_iso_quotient_homocyclic_sdprod V G m.
proof: Proof. move=> minV copG abelV m_gt0; pose q := (p ^ m)%N. have [ntV nVG] := andP (mingroupp minV). have [p_pr pVdvdn [n Vpexpn]] := pgroup_pdiv (abelem_pgroup abelV) ntV. move/(abelem_mx_irrP abelV ntV nVG): (minV) => mx_irrV. have dim_lt0 : 'dim V > 0 by rewrite (dim_abelemE abelV) // Vpexpn pfactorK. have q_gt1: q > 1 by rewrite (ltn_exp2l 0) // prime_gt1. have p_q: p.-nat q by rewrite pnatX pnat_id. have p_dv_q: p %| q := dvdn_exp2l p m_gt0. pose rG := regular_repr 'Z_q G; pose MR_G := ('MR rG)%gact. have [wT [fL injL [fX injX fJ]]]: exists wT : finGroupType, exists2 fL : {morphism setT >-> wT}, 'injm fL & exists2 fX : {morphism G >-> wT}, 'injm fX & {in setT & G, morph_act MR_G 'J fL fX}. - exists (sdprod_groupType MR_G). exists (sdpair1_morphism MR_G); first exact: injm_sdpair1. by exists (sdpair2_morphism MR_G); [apply: injm_sdpair2 | apply: sdpair_act]. move imfL: (fL @* [set: _])%G => L; move imfX: (fX @* G)%G => X. have cLL: abelian L by rewrite -imfL morphim_abelian // zmod_abelian. have pL: p.-group L. by rewrite -imfL morphim_pgroup /= -?pnat_exponent ?exponent_mx_group ?cardG_gt0. have tiVG: V :&: G = 1 by rewrite coprime_TIg // Vpexpn coprime_pexpl. have{copG} p'G: p^'.-group G by rewrite /pgroup p'natE // -prime_coprime. have p'X: p^'.-group X by rewrite -imfX morphim_pgroup. have nXL: X \subset 'N(L). rewrite -imfX -imfL; apply/subsetP=> _ /morphimP[x Gx _ ->]; rewrite inE. apply/subsetP=> _ /imsetP[_ /morphimP[v rVv _ ->] ->]. by rewrite -fJ // mem_morphim ?in_setT. have [/= S defL im_S] := coprime_act_abelian_pgroup_structure cLL pL p'X nXL. pose gi (z : 'Z_q) := z%:R : 'F_p. have gia : additive gi. move=> z1 z2. apply: canRL (addrK _) _; apply: val_inj. by rewrite -{2}(subrK z2 z1) -natrD /= !val_Fp_nat ?modn_dvdm // Zp_cast. have gim : multiplicative gi. split=> // z1 z2. by apply: val_inj; rewrite -natrM /= !val_Fp_nat ?modn_dvdm // Zp_cast. pose giaM := GRing.isAdditive.Build _ _ gi gia. pose gimM := GRing.isMultiplicative.Build _ _ gi gim. pose giRM : GRing.RMorphism.type _ _ := HB.pack gi giaM gimM. have [gL [DgL _ _ _]] := domP (invm_morphism injL) (congr_group imfL). pose g u := map_mx giRM (gL u). have gM: {in L &, {morph g : u v / u * v}}. by move=> u v Lu Lv /=; rewrite {1}/g morphM // map_mxD. have kerg: 'ker (Morphism gM) = 'Phi(L). rewrite (Phi_Mho pL cLL) (MhoEabelian 1 pL cLL). apply/setP=> u; apply/idP/imsetP=> [ | [v Lv ->{u}]]; last first. rewrite !inE groupX //=; apply/eqP/rowP=> i; apply: val_inj. rewrite !mxE morphX // mulmxnE Zp_mulrn /= val_Fp_nat //=. by move: {i}(_ i); rewrite Zp_cast // => vi; rewrite modn_dvdm // modnMl. case/morphpreP; rewrite -{1}imfL => /morphimP[v rVv _ ->{u}] /set1P /=. rewrite /g DgL /= invmE // => /rowP vp0. pose x := fL (map_mx (fun t : 'Z_q => (t %/ p)%:R) v). exists x; first by rewrite -imfL mem_morphim ?inE. rewrite -morphX ?in_setT //; congr (fL _); apply/rowP=> i. rewrite mulmxnE -{1}(natr_Zp (v 0 i)) {1}(divn_eq (v 0 i) p) addnC. by have:= congr1 val (vp0 i); rewrite !mxE -mulrnA /= val_Fp_nat // => ->. have [gX [DgX KgX _ imgX]] := domP (invm_morphism injX) (congr_group imfX). pose aG := regular_repr 'F_p G. have GgX: {in X, forall x, gX x \in G}. by rewrite DgX -imfX => _ /morphimP[x Gx _ ->]; rewrite /= invmE. have XfX: {in G, forall x, fX x \in X}. by move=> x Gx; rewrite -imfX mem_morphim. have gJ: {in L & X, forall u x, g (u ^ x) = g u *m aG (gX x)}. rewrite -{1}imfL -{1}imfX => _ _ /morphimP[u rVu _ ->] /morphimP[x Gx _ ->]. rewrite -fJ // /g DgL DgX /= !invmE // mx_repr_actE ?inE //. by rewrite (map_mxM giRM) map_regular_mx. pose gMx U := rowg_mx (Morphism gM @* U). have simS: forall U, U \in S -> mxsimple aG (gMx U). move=> U S_U; have [_ nUX irrU] := im_S U S_U. have{irrU} [modU irrU] := mingroupP irrU; have{modU} [ntU _] := andP modU. have sUL: U \subset L by rewrite -(bigdprodWY defL) sub_gen // (bigcup_max U). split=> [||U2 modU2]. - rewrite (eqmx_module _ (genmxE _)); apply/mxmoduleP=> x Gx. apply/row_subP=> i; rewrite row_mul rowK. have [u Lu Uu def_u] := morphimP (enum_valP i). rewrite -(invmE injX Gx) -DgX def_u -gJ ?XfX //. set ux := u ^ _; apply: eq_row_sub (gring_index _ (g ux)) _. have Uux: ux \in U by rewrite memJ_norm // (subsetP nUX) ?XfX. by rewrite rowK gring_indexK //; apply: mem_morphim; rewrite ?(subsetP sUL). - apply: contra ntU; rewrite rowg_mx_eq0. rewrite -subG1 sub_morphim_pre // -kerE kerg => sU_Phi. rewrite /= quotientS1 //=; rewrite (big_setD1 U) //= in defL. have{defL} [[_ U' _ ->] defUU' cUU' tiUU'] := dprodP defL. have defL: U \* U' = L by rewrite cprodE. have:= cprod_modl (Phi_cprod pL defL) (Phi_sub U). rewrite -(setIidPl (Phi_sub U')) setIAC -setIA tiUU' setIg1 cprodg1 => ->. by rewrite subsetIidr. rewrite -!rowgS stable_rowg_mxK /= => [sU2gU nzU2|]; last first. apply/subsetP=> z _; rewrite !inE /=; apply/subsetP=> u gUu. by rewrite inE /= /scale_act -[val z]natr_Zp scaler_nat groupX. rewrite sub_morphim_pre // -subsetIidl. rewrite -(quotientSGK (normal_norm (Phi_normal U))) //=; last first. rewrite subsetI Phi_sub (subset_trans (PhiS pL sUL)) //. by rewrite -kerg ker_sub_pre. rewrite [(U :&: _) / _]irrU //; last by rewrite quotientS ?subsetIl. rewrite (contra _ nzU2) /=; last first. rewrite -subG1 quotient_sub1; last first. by rewrite subIset // normal_norm // Phi_normal. rewrite /= -(morphpre_restrm sUL). move/(morphimS (restrm_morphism sUL (Morphism gM))). rewrite morphpreK ?im_restrm // morphim_restrm => s_U2_1. rewrite -trivg_rowg -subG1 (subset_trans s_U2_1) //. rewrite -(morphim_ker (Morphism gM)) morphimS // kerg. by rewrite subIset ?(PhiS pL) ?orbT. rewrite actsQ //; first by rewrite gFnorm_trans. rewrite normsI //; apply/subsetP=> x Xx; rewrite inE. apply/subsetP=> _ /imsetP[u g'U2u ->]. have [Lu U2gu] := morphpreP g'U2u; rewrite mem_rowg in U2gu. rewrite inE memJ_norm ?(subsetP nXL) // Lu /= inE gJ //. by rewrite mem_rowg (mxmodule_trans modU2) ?GgX. have im_g: Morphism gM @* L = [set: 'rV_#|G|]. apply/eqP; rewrite eqEcard subsetT cardsT card_mx card_Fp //= mul1n. rewrite card_morphim kerg setIid (Phi_Mho pL cLL) -divgS ?Mho_sub //. rewrite -(mul_card_Ohm_Mho_abelian 1 cLL) mulnK ?cardG_gt0 //. rewrite (card_pgroup (pgroupS (Ohm_sub 1 L) pL)) -rank_abelian_pgroup //. by rewrite -imfL (injm_rank injL) //= rank_mx_group mul1n. have sumS: (\sum_(U in S) gMx U :=: 1%:M)%MS. apply/eqmxP; rewrite submx1; apply/rV_subP=> v _. have: v \in Morphism gM @* L by rewrite im_g inE. case/morphimP=> u Lu _ ->{v}. rewrite -mem_rowg -sub1set -morphim_set1 // sub_morphim_pre ?sub1set //. have [c [Uc -> _]] := mem_bigdprod defL Lu; rewrite group_prod //= => U S_U. have sUL: U \subset L by rewrite -(bigdprodWY defL) sub_gen // (bigcup_max U). rewrite inE (subsetP sUL) ?Uc // inE mem_rowg (sumsmx_sup U) // -mem_rowg. by rewrite (subsetP (sub_rowg_mx _)) // mem_morphim ?(subsetP sUL) ?Uc. have Fp'G: [char 'F_p]^'.-group G. by rewrite (eq_p'group _ (charf_eq (char_Fp p_pr))). have [VK [modVK defVK]] := rsim_regular_submod mx_irrV Fp'G. have [U S_U isoUV]: {U | U \in S & mx_iso (regular_repr _ G) (gMx U) VK}. apply: hom_mxsemisimple_iso (scalar_mx_hom _ 1 _) _ => [|U S_U _|]; auto. by apply/(submod_mx_irr modVK); apply: (mx_rsim_irr defVK). by rewrite mulmx1 sumS submx1. have simU := simS U S_U; have [modU _ _] := simU. pose rV := abelem_repr abelV ntV nVG. have{VK modVK defVK isoUV} [h dimU h_free hJ]: mx_rsim (submod_repr modU) rV. by apply: mx_rsim_trans (mx_rsim_sym defVK); apply/mx_rsim_iso. have sUL : U \subset L. by move: defL; rewrite (big_setD1 U) //= => /dprodP[[_ U1 _ ->] /mulG_sub[]]. pose W := [set: 'rV['Z_(p ^ m)](V)]%G. have [homU nUX _] := im_S U S_U; have [cUU _] := andP homU. have atypeU: abelian_type U == nseq ('dim V) (p ^ m)%N. rewrite (big_setD1 U) //= in defL. have [[_ U' _ defU'] defUU' _ tiUU'] := dprodP defL. rewrite defU' in defL defUU' tiUU'. have ->: 'dim V = 'r(U). apply/eqP; rewrite -dimU -(eqn_exp2l _ _ (prime_gt1 p_pr)). rewrite (rank_abelian_pgroup (pgroupS sUL pL) cUU). rewrite -(card_pgroup (pgroupS (Ohm_sub 1 U) (pgroupS sUL pL))). rewrite -{1}(card_Fp p_pr) -card_rowg stable_rowg_mxK; last first. apply/subsetP=> z _; rewrite !inE; apply/subsetP=> v gUv. by rewrite inE /= /scale_act -(natr_Zp (val z)) scaler_nat groupX. rewrite card_morphim kerg (Phi_Mho pL cLL) (setIidPr sUL) -divgI setIC. rewrite -(dprod_modl (Mho_dprod 1 defL) (Mho_sub 1 U)). rewrite [_ :&: _](trivgP _); last by rewrite -tiUU' setIC setSI ?Mho_sub. by rewrite dprodg1 -(mul_card_Ohm_Mho_abelian 1 cUU) mulnK ?cardG_gt0. have isoL: isog L [set: 'rV['Z_q]_#|G|] by rewrite -imfL isog_sym sub_isog. have homL: homocyclic L by rewrite (isog_homocyclic isoL) mx_group_homocyclic. have [-> _] := abelian_type_dprod_homocyclic defL pL homL. by rewrite (exponent_isog isoL) // exponent_mx_group. have pU: p.-group U by rewrite (pgroupS sUL). have isoWU: isog U W. by rewrite eq_abelian_type_isog ?zmod_abelian // abelian_type_mx_group ?mul1n. have {cUU atypeU} cardU : #|U| = (#|V| ^ m)%N. rewrite card_homocyclic // (exponent_isog isoWU) exponent_mx_group //. rewrite -size_abelian_type // (eqP atypeU) size_nseq. by rewrite (dim_abelemE abelV) // Vpexpn pfactorK // expnAC. pose f3 w := rVabelem abelV ntV (in_submod _ (g w) *m h). have f3M: {in U &, {morph f3: w1 w2 / w1 * w2}}. move=> w1 w2 Uw1 Uw2 /=; rewrite {1}/f3. rewrite gM ?(subsetP sUL) // linearD mulmxDl. by rewrite morphM ?mem_im_abelem_rV. have Ugw w : w \in U -> (g w <= gMx U)%MS. move=> Uw; rewrite -mem_rowg (subsetP (sub_rowg_mx _)) //. by rewrite (mem_morphim (Morphism gM)) ?(subsetP sUL). have KgU: 'ker_U (Morphism gM) = 'Mho^1(U). rewrite kerg (Phi_Mho pL cLL); rewrite (big_setD1 U) //= in defL. have [[_ U' _ defU'] _ _ tiUU'] := dprodP defL; rewrite defU' in defL tiUU'. rewrite setIC -(dprod_modl (Mho_dprod 1 defL) (Mho_sub 1 U)). by rewrite [_ :&: _](trivgP _) ?dprodg1 // -tiUU' setIC setSI ?Mho_sub. have{KgU} Kf3: 'ker (Morphism f3M) = 'Mho^1(U). apply/setP=> w; rewrite !inE /=. rewrite morph_injm_eq1 ?rVabelem_injm ?mem_im_abelem_rV //=. rewrite -[1](mul0mx _ h) (inj_eq (row_free_inj h_free)) in_submod_eq0. case Uw: (w \in U) => /=; last first. by apply/sym_eq; apply: contraFF Uw; apply: (subsetP (Mho_sub _ _)). rewrite -[(_ <= _)%MS]andTb -(Ugw _ Uw) -sub_capmx capmx_compl submx0. by rewrite -KgU !inE Uw (subsetP sUL). have cUU: abelian U := abelianS sUL cLL. have im_f3: Morphism f3M @* U = V. apply/eqP; rewrite eqEcard card_morphim setIid Kf3; apply/andP; split. by apply/subsetP=> _ /morphimP[w _ _ ->]; apply: mem_rVabelem. rewrite -divgS ?Mho_sub // -(mul_card_Ohm_Mho_abelian 1 cUU). rewrite mulnK ?cardG_gt0 // (card_pgroup (pgroupS (Ohm_sub 1 U) pU)). rewrite -rank_abelian_pgroup // (isog_rank isoWU) /W. by rewrite (dim_abelemE abelV) // rank_mx_group mul1n Vpexpn pfactorK. have f3J: {in U & X, morph_act 'J 'J (Morphism f3M) gX}. move=> u x Uu Xx; rewrite /f3 /= gJ ?(subsetP sUL) // in_submodJ ?Ugw //. by rewrite -mulmxA hJ ?GgX // mulmxA rVabelemJ ?GgX. have defUX: U ><| X = U <*> X. rewrite norm_joinEr; last by case: (im_S _ S_U). by rewrite sdprodE ?coprime_TIg ?(pnat_coprime pU). pose f := sdprodm defUX f3J. have{im_f3} fU_V: f @* U = V by rewrite morphim_sdprodml. have fX_G: f @* X = G by rewrite morphim_sdprodmr // imgX -imfX im_invm. suffices: 'ker f = 'Mho^1(U) by exists wT U (U <*> X)%G X [morphism of f]. rewrite -Kf3; apply/setP=> y; apply/idP/idP; last first. move=> /morphpreP[/= Uy /set1P f3y]. by rewrite !inE /= sdprodmEl //= f3y (subsetP (joing_subl _ X)) /=. rewrite ker_sdprodm => /imset2P[u t Uu /setIdP[Xt /eqP/= fu] ->{y}]. have: f3 u \in V :&: G. by rewrite inE -fU_V morphim_sdprodml //= imset_f ?setIid // fu GgX. rewrite tiVG in_set1 fu morph_injm_eq1 ?KgX ?injm_invm // => /eqP t1. by rewrite t1 invg1 mulg1 !inE Uu /= fu t1 morph1. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action gfunctor commutator) mathcomp(gproduct zmodp cyclic center pgroup gseries nilpotent sylow) mathcomp(finalg finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)