proposition: Proposition diag_sum_proj_eigenspace_cycle m : (diagE m :=: 'E_m)%MS /\ mxdirect (diagE m).
proof: Proof. have sub_diagE n: (diagE n <= 'E_n)%MS. apply/sumsmx_subP=> [[i t] /= def_t]. apply: submx_trans (proj_eigenspace_cycle_sub_quasi_cent i n). by rewrite /E2_ -(Vi_mod (i + n)) (eqP def_t) Vi_mod. pose sum_diagE := (\sum_(n < h) diagE n)%MS. pose p (it : 'I_h * 'I_h) := inh (h - it.1 + it.2). have def_diag: sum_diagE = sumE. rewrite /sumE (partition_big p xpredT) //. apply: eq_bigr => n _; apply: eq_bigl => [[i t]] /=. rewrite /p -val_eqE /= -(eqn_modDl (h - i)). by rewrite addnA subnK 1?ltnW // modnDl modn_small. have [Efull dxE] := mxdirect_sum_proj_eigenspace_cycle. have /mxdirect_sumsE[/= dx_diag rank_diag]: mxdirect sum_diagE. apply/mxdirectP; rewrite /= -/sum_diagE def_diag (mxdirectP dxE) /=. rewrite (partition_big p xpredT) //. apply: eq_bigr => n _; apply: eq_bigl => [[i t]] /=. symmetry; rewrite /p -val_eqE /= -(eqn_modDl (h - i)). by rewrite addnA subnK 1?ltnW // modnDl modn_small. have dx_sumE1: mxdirect (\sum_(i < h) 'E_i). by apply: mxdirect_sum_eigenspace => i j _ _; apply: inj_eps. have diag_mod n: diagE (n %% h) = diagE n. by apply: eq_bigl=> it; rewrite modnDmr. split; last first. apply/mxdirectP; rewrite /= -/(diagE m) -diag_mod. rewrite (mxdirectP (dx_diag (inh m) _)) //=. by apply: eq_bigl=> it; rewrite modnDmr. apply/eqmxP; rewrite sub_diagE /=. rewrite -(capmx_idPl (_ : _ <= sumE))%MS ?Efull ?submx1 //. rewrite -def_diag /sum_diagE (bigD1 (inh m)) //= addsmxC. rewrite diag_mod -matrix_modr ?sub_diagE //. rewrite ((_ :&: _ =P 0)%MS _) ?adds0mx // -submx0. rewrite -{2}(mxdirect_sumsP dx_sumE1 (inh m)) ?capmxS //. by rewrite /E_ eps_mod_h. by apply/sumsmx_subP=> i ne_i_m; rewrite (sumsmx_sup i) ?sub_diagE. 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)