proposition: Proposition mx_irr_prime_index F gT (G H : {group gT}) n M (nsHG : H <| G) (rG : mx_representation F G n) (rH := subg_repr rG (normal_sub nsHG)) : group_closure_field F gT -> mx_irreducible rG -> cyclic (G / H)%g -> mxsimple rH M -> {in G, forall x, mx_iso rH M (M *m rG x)} -> mx_irreducible rH.
proof: Proof. move=> closedF irrG /cyclicP[Hx defGH] simM isoM; have [sHG nHG] := andP nsHG. have [modM nzM _] := simM; pose E_H := enveloping_algebra_mx rH. have absM f: (M *m f <= M)%MS -> {a | (a \in E_H)%MS & M *m a = M *m f}. move=> sMf; set rM := submod_repr modM; set E_M := enveloping_algebra_mx rM. pose u := mxvec (in_submod M (val_submod 1%:M *m f)) *m pinvmx E_M. have EHu: (gring_mx rH u \in E_H)%MS := gring_mxP rH u. exists (gring_mx rH u) => //; rewrite -(in_submodK sMf). rewrite -(in_submodK (mxmodule_envelop modM EHu _)) //; congr (val_submod _). transitivity (in_submod M M *m gring_mx rM u). rewrite /gring_mx /= !mulmx_sum_row !linear_sum; apply: eq_bigr => i /= _. by rewrite !linearZ /= !rowK !mxvecK -in_submodJ. rewrite /gring_mx /= mulmxKpV ?submx_full ?mxvecK //; last first. by have/andP[]: mx_absolutely_irreducible rM by apply/closedF/submod_mx_irr. rewrite {1}[in_submod]lock in_submodE -mulmxA mulmxA -val_submodE -lock. by rewrite mulmxA -in_submodE in_submodK. have /morphimP[x nHx Gx defHx]: Hx \in (G / H)%g by rewrite defGH cycle_id. have{Hx defGH defHx} defG : G :=: <[x]> <*> H. rewrite -(quotientGK nsHG) defGH defHx -quotient_cycle //. by rewrite joingC quotientK ?norm_joinEr // cycle_subG. have [e def1]: exists e, 1%:M = \sum_(z in G) e z *m (M *m rG z). apply/sub_sumsmxP; have [X sXG [<- _]] := Clifford_basis irrG simM. by apply/sumsmx_subP=> z Xz; rewrite (sumsmx_sup z) ?(subsetP sXG). have [phi inj_phi hom_phi defMx] := isoM x Gx. have Mtau: (M *m (phi *m rG x^-1%g) <= M)%MS. by rewrite mulmxA (eqmxMr _ defMx) repr_mxK. have Mtau': (M *m (rG x *m invmx phi) <= M)%MS. by rewrite mulmxA -(eqmxMr _ defMx) mulmxK. have [[tau Htau defMtau] [tau' Htau' defMtau']] := (absM _ Mtau, absM _ Mtau'). have tau'K: tau' *m tau = 1%:M. rewrite -[tau']mul1mx def1 !mulmx_suml; apply: eq_bigr => z Gz. have [f _ hom_f] := isoM z Gz; move/eqmxP; case/andP=> _; case/submxP=> v ->. rewrite (mulmxA _ v) -2!mulmxA; congr (_ *m _). rewrite -(hom_envelop_mxC hom_f) ?envelop_mxM //; congr (_ *m _). rewrite mulmxA defMtau' -(mulmxKpV Mtau') -mulmxA defMtau (mulmxA _ M). by rewrite mulmxKpV // !mulmxA mulmxKV // repr_mxK. have cHtau_x: centgmx rH (tau *m rG x). apply/centgmxP=> y Hy; have [u defMy] := submxP (mxmoduleP modM y Hy). have Gy := subsetP sHG y Hy. rewrite mulmxA; apply: (canRL (repr_mxKV rG Gx)). rewrite -!mulmxA /= -!repr_mxM ?groupM ?groupV // (conjgC y) mulKVg. rewrite -[rG y]mul1mx -{1}[tau]mul1mx def1 !mulmx_suml. apply: eq_bigr => z Gz; have [f _ hom_f] := isoM z Gz. move/eqmxP; case/andP=> _; case/submxP=> v ->; rewrite -!mulmxA. congr (_ *m (_ *m _)); rewrite {v} !(mulmxA M). rewrite -!(hom_envelop_mxC hom_f) ?envelop_mxM ?(envelop_mx_id rH) //. congr (_ *m f); rewrite !mulmxA defMy -(mulmxA u) defMtau (mulmxA u) -defMy. rewrite !mulmxA (hom_mxP hom_phi) // -!mulmxA; congr (M *m (_ *m _)). by rewrite /= -!repr_mxM ?groupM ?groupV // -conjgC. by rewrite -mem_conjg (normsP nHG). have{cHtau_x} cGtau_x: centgmx rG (tau *m rG x). rewrite /centgmx {1}defG join_subG cycle_subG !inE Gx /= andbC. rewrite (subset_trans cHtau_x); last by rewrite rcent_subg subsetIr. apply/eqP; rewrite -{2 3}[rG x]mul1mx -tau'K !mulmxA; congr (_ *m _ *m _). case/envelop_mxP: Htau' => u ->. rewrite !(mulmx_suml, mulmx_sumr); apply: eq_bigr => y Hy. by rewrite -!(scalemxAl, scalemxAr) (centgmxP cHtau_x) ?mulmxA. have{cGtau_x} [a def_tau_x]: exists a, tau *m rG x = a%:M. by apply/is_scalar_mxP; apply: mx_abs_irr_cent_scalar cGtau_x; apply: closedF. apply: mx_iso_simple (eqmx_iso _ _) simM; apply/eqmxP; rewrite submx1 sub1mx. case/mx_irrP: (irrG) => _ -> //; rewrite /mxmodule {1}defG join_subG /=. rewrite cycle_subG inE Gx andbC (subset_trans modM) ?rstabs_subg ?subsetIr //=. rewrite -{1}[M]mulmx1 -tau'K mulmxA -mulmxA def_tau_x mul_mx_scalar. by rewrite scalemx_sub ?(mxmodule_envelop modM Htau'). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gfunctor commutator gproduct) mathcomp(ssralg finalg zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)