proposition: Lemma mx_Jacobson_density : ('C(Hom_G) <= E_G)%MS.
proof: Proof. apply/row_subP=> iB; rewrite -[row iB _]vec_mxK; move defB: (vec_mx _) => B. have{defB} cBcE: (B \in 'C(Hom_G))%MS by rewrite -defB vec_mxK row_sub. have rGnP: mx_repr G (fun x => lin_mx (mulmxr (rG x)) : 'A_n). split=> [|x y Gx Gy]; apply/row_matrixP=> i. by rewrite !rowE mul_rV_lin repr_mx1 /= !mulmx1 vec_mxK. by rewrite !rowE mulmxA !mul_rV_lin repr_mxM //= mxvecK mulmxA. move def_rGn: (MxRepresentation rGnP) => rGn. pose E_Gn := enveloping_algebra_mx rGn. pose e1 : 'rV[F]_(n ^ 2) := mxvec 1%:M; pose U := cyclic_mx rGn e1. have U_e1: (e1 <= U)%MS by rewrite cyclic_mx_id. have modU: mxmodule rGn U by rewrite cyclic_mx_module. pose Bn : 'M_(n ^ 2) := lin_mx (mulmxr B). suffices U_e1Bn: (e1 *m Bn <= U)%MS. rewrite mul_vec_lin /= mul1mx in U_e1Bn; apply: submx_trans U_e1Bn _. rewrite genmxE; apply/row_subP=> i; rewrite row_mul rowK mul_vec_lin_row. by rewrite -def_rGn mul_vec_lin /= mul1mx (eq_row_sub i) ?rowK. have{cBcE} cBncEn A: centgmx rGn A -> A *m Bn = Bn *m A. rewrite -def_rGn => cAG; apply/row_matrixP; case/mxvec_indexP=> j k /=. rewrite !rowE !mulmxA -mxvec_delta -(mul_delta_mx (0 : 'I_1)). rewrite mul_rV_lin mul_vec_lin /= -mulmxA; apply: (canLR vec_mxK). apply/row_matrixP=> i; set dj0 := delta_mx j 0. pose Aij := row i \o vec_mx \o mulmxr A \o mxvec \o mulmx dj0. have defAij := mul_rV_lin1 (GRing.Linear.clone _ _ _ _ Aij _). rewrite /= {2}/Aij /= in defAij. rewrite -defAij row_mul -defAij -!mulmxA (cent_mxP cBcE) {k}//. rewrite memmx_cent_envelop; apply/centgmxP=> x Gx; apply/row_matrixP=> k. rewrite !row_mul !rowE !{}defAij /= -row_mul mulmxA mul_delta_mx. congr (row i _); rewrite -(mul_vec_lin (mulmxr (rG x))) -mulmxA. by rewrite -(centgmxP cAG) // mulmxA mx_rV_lin. suffices redGn: mx_completely_reducible rGn 1%:M. have [V modV defUV] := redGn _ modU (submx1 _); move/mxdirect_addsP=> dxUV. rewrite -(proj_mx_id dxUV U_e1) -mulmxA {}cBncEn 1?mulmxA ?proj_mx_sub //. by rewrite -row_full_dom_hom -sub1mx -defUV proj_mx_hom. pose W i : 'M[F]_(n ^ 2) := <<lin1_mx (mxvec \o mulmx (delta_mx i 0))>>%MS. have defW: (\sum_i W i :=: 1%:M)%MS. apply/eqmxP; rewrite submx1; apply/row_subP; case/mxvec_indexP=> i j. rewrite row1 -mxvec_delta (sumsmx_sup i) // genmxE; apply/submxP. by exists (delta_mx 0 j); rewrite mul_rV_lin1 /= mul_delta_mx. apply: mxsemisimple_reducible; apply: (intro_mxsemisimple defW) => i _ nzWi. split=> // [|Vi modVi sViWi nzVi]. apply/mxmoduleP=> x Gx; rewrite genmxE (eqmxMr _ (genmxE _)) -def_rGn. apply/row_subP=> j; rewrite rowE mulmxA !mul_rV_lin1 /= mxvecK -mulmxA. by apply/submxP; move: (_ *m rG x) => v; exists v; rewrite mul_rV_lin1. do [rewrite !genmxE; set f := lin1_mx _] in sViWi *. have f_free: row_free f. apply/row_freeP; exists (lin1_mx (row i \o vec_mx)); apply/row_matrixP=> j. by rewrite row1 rowE mulmxA !mul_rV_lin1 /= mxvecK rowE !mul_delta_mx. pose V := <<Vi *m pinvmx f>>%MS; have Vidf := mulmxKpV sViWi. suffices: (1%:M <= V)%MS by rewrite genmxE -(submxMfree _ _ f_free) mul1mx Vidf. case: irrG => _ _ ->; rewrite ?submx1 //; last first. by rewrite -mxrank_eq0 genmxE -(mxrankMfree _ f_free) Vidf mxrank_eq0. apply/mxmoduleP=> x Gx; rewrite genmxE (eqmxMr _ (genmxE _)). rewrite -(submxMfree _ _ f_free) Vidf. apply: submx_trans (mxmoduleP modVi x Gx); rewrite -{2}Vidf. apply/row_subP=> j; apply: (eq_row_sub j); rewrite row_mul -def_rGn. by rewrite !(row_mul _ _ f) !mul_rV_lin1 /= mxvecK !row_mul !mulmxA. 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)