proposition: Lemma DecSocleType : socleType rG.
proof: Proof. have [n0 | n_gt0] := posnP n. by exists [::] => // M [_]; rewrite -mxrank_eq0 -leqn0 -n0 rank_leq_row. have n2_gt0: n ^ 2 > 0 by rewrite muln_gt0 n_gt0. pose span Ms := (\sum_(M <- Ms) component_mx rG M)%MS. have: {in [::], forall M, mxsimple rG M} by []. have [m] := ubnP (n - \rank (span [::])). elim: m [::] => // m IHm Ms /ltnSE-Ms_ge_n simMs. pose V := span Ms; pose Vt := mx_term V. pose Ut i := vec_mx (row_var F (n * n) i); pose Zt := mx_term (0 : 'M[F]_n). pose exU i f := Exists_row_form (n * n) i (~ submx_form (Ut i) Zt /\ f (Ut i)). pose meetUVf U := exU 1 (fun W => submx_form W Vt /\ submx_form W U)%T. pose mx_sat := GRing.sat (@row_env F (n * n) [::]). have ev_sub0 := GRing.qf_evalP _ (submx_form_qf _ Zt). have ev_mod := GRing.qf_evalP _ (mxmodule_form_qf rG _). pose ev := (eval_mxmodule, eval_submx, eval_vec_mx, eval_row_var, eval_mx_term). case haveU: (mx_sat (exU 0 (fun U => mxmodule_form rG U /\ ~ meetUVf _ U)%T)). have [U modU]: {U : 'M_n | mxmodule rG U & (U != 0) && ((U :&: V)%MS == 0)}. apply: sig2W; case/Exists_rowP: (satP haveU) => //= u [nzU [modU tiUV]]. exists (vec_mx u); first by move/ev_mod: modU; rewrite !ev. set W := (_ :&: V)%MS; move/ev_sub0: nzU; rewrite !ev -!submx0 => -> /=. apply/idPn=> nzW; case: tiUV; apply/Exists_rowP=> //; exists (mxvec W). apply/GRing.qf_evalP; rewrite /= ?submx_form_qf // !ev mxvecK nzW /=. by rewrite andbC -sub_capmx. case/andP=> nzU tiUV; have [M simM sMU] := dec_mxsimple_exists modU nzU. apply: (IHm (M :: Ms)) => [|M']; last first. by case/predU1P=> [-> //|]; apply: simMs. have [_ nzM _] := simM. suffices ltVMV: \rank V < \rank (span (M :: Ms)). rewrite (leq_trans _ Ms_ge_n) // ltn_sub2l ?(leq_trans ltVMV) //. exact: rank_leq_row. rewrite /span big_cons (ltn_leqif (mxrank_leqif_sup (addsmxSr _ _))). apply: contra nzM; rewrite addsmx_sub -submx0 -(eqP tiUV) sub_capmx sMU. by case/andP=> sMV _; rewrite (submx_trans _ sMV) ?component_mx_id. exists Ms => // M simM; have [modM nzM minM] := simM. have sMV: (M <= V)%MS. apply: contraFT haveU => not_sMV; apply/satP/Exists_rowP=> //. exists (mxvec M); split; first by apply/ev_sub0; rewrite !ev mxvecK submx0. split; first by apply/ev_mod; rewrite !ev mxvecK. apply/Exists_rowP=> // [[w]]. apply/GRing.qf_evalP; rewrite /= ?submx_form_qf // !ev /= mxvecK submx0. rewrite -nz_row_eq0 -(cyclic_mx_eq0 rG); set W := cyclic_mx _ _. apply: contra not_sMV => /and3P[nzW Vw Mw]. have{Vw Mw} [sWV sWM]: (W <= V /\ W <= M)%MS. rewrite !cyclic_mx_sub ?(submx_trans (nz_row_sub _)) //. by rewrite sumsmx_module // => M' _; apply: component_mx_module. by rewrite (submx_trans _ sWV) // minM ?cyclic_mx_module. wlog sG: / socleType rG by apply: socle_exists. have sVS: (V <= \sum_(W : sG | has (fun Mi => Mi <= W) Ms) W)%MS. rewrite [V](big_nth 0) big_mkord; apply/sumsmx_subP=> i _. set Mi := Ms`_i; have MsMi: Mi \in Ms by apply: mem_nth. have simMi := simMs _ MsMi; have S_Mi := component_socle sG simMi. rewrite (sumsmx_sup (PackSocle S_Mi)) ?PackSocleK //. by apply/hasP; exists Mi; rewrite ?component_mx_id. have [W MsW isoWM] := subSocle_iso simM (submx_trans sMV sVS). have [Mi MsMi sMiW] := hasP MsW; apply/hasP; exists Mi => //. have [simMi simW] := (simMs _ MsMi, socle_simple W); apply/mxsimple_isoP=> //. exact: mx_iso_trans (mx_iso_sym isoWM) (component_mx_iso simW simMi sMiW). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)