proposition: Lemma mx_rsim_socle (sG : socleType rG) (W : sG) (rW : representation) : let modW : mxmodule rG W := component_mx_module rG (socle_base W) in mx_rsim (socle_repr W) rW -> mx_rsim (submod_repr modW) (muln_grepr rW (socle_mult W)).
proof: Proof. set M := socle_base W => modW rsimM. have simM: mxsimple rG M := socle_simple W. have rankM_gt0: (\rank M > 0)%N by rewrite lt0n mxrank_eq0; case: simM. have [I /= U_I simU]: mxsemisimple rG W by apply: component_mx_semisimple. pose U (i : 'I_#|I|) := U_I (enum_val i). have reindexI := reindex _ (onW_bij I (enum_val_bij I)). rewrite mxdirectE /= !reindexI -mxdirectE /= => defW dxW. have isoU: forall i, mx_iso rG M (U i). move=> i; have sUiW: (U i <= W)%MS by rewrite -defW (sumsmx_sup i). exact: component_mx_iso (simU _) sUiW. have ->: socle_mult W = #|I|. rewrite -(mulnK #|I| rankM_gt0); congr (_ %/ _)%N. rewrite -defW (mxdirectP dxW) /= -sum_nat_const reindexI /=. by apply: eq_bigr => i _; rewrite -(mxrank_iso (isoU i)). have modU: mxmodule rG (U _) := mxsimple_module (simU _). suff: mx_rsim (submod_repr (modU _)) rW by apply: mx_rsim_dsum defW dxW. by move=> i; apply: mx_rsim_trans (mx_rsim_sym _) rsimM; apply/mx_rsim_iso. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)