proposition: Proposition mxdirect_sum_eigenspace_cycle : (sumV :=: 1%:M)%MS /\ mxdirect sumV.
proof: Proof. have splitF: group_splitting_field F (Zp_group h). move: prim_eps (abelianS (subsetT (Zp h)) (Zp_abelian _)). by rewrite -{1}(card_Zp h_gt0); apply: primitive_root_splitting_abelian. have F'Zh: [char F]^'.-group (Zp h). apply/pgroupP=> p p_pr; rewrite card_Zp // => /dvdnP[d def_h]. apply/negP=> /= charFp. have d_gt0: d > 0 by move: h_gt0; rewrite def_h; case d. have: eps ^+ d == 1. rewrite -(inj_eq (fmorph_inj (Frobenius_aut charFp))). by rewrite rmorph1 /= Frobenius_autE -exprM -def_h eps_h. by rewrite -(prim_order_dvd prim_eps) gtnNdvd // def_h ltn_Pmulr // prime_gt1. case: (ltngtP h 1) => [|h_gt1|h1]; last first; last by rewrite ltnNge h_gt0. rewrite /sumV mxdirectE /= h1 !big_ord1; split=> //. apply/eqmxP; rewrite submx1; apply/eigenspaceP. by rewrite mul1mx scale1r idmxE -gh1 h1. pose mxZ (i : 'Z_h) := g ^+ i. have mxZ_repr: mx_repr (Zp h) mxZ. by split=> // i j _ _; rewrite /mxZ /= {3}Zp_cast // expr_mod // exprD. pose rZ := MxRepresentation mxZ_repr. have ZhT: Zp h = setT by rewrite /Zp h_gt1. have memZh: _ \in Zp h by move=> i; rewrite ZhT inE. have def_g: g = rZ Zp1 by []. have lin_rZ m (U : 'M_(m, q)) a: U *m g = a *: U -> forall i, U *m rZ i%:R = (a ^+ i) *: U. - move=> defUg i; rewrite repr_mxX //. elim: i => [|i IHi]; first by rewrite mulmx1 scale1r. by rewrite !exprS -scalerA mulmxA defUg -IHi scalemxAl. rewrite mxdirect_sum_eigenspace => [|j k _ _]; last exact: inj_eps. split=> //; apply/eqmxP; rewrite submx1. wlog [I M /= simM <- _]: / mxsemisimple rZ 1. exact: mx_reducible_semisimple (mxmodule1 _) (mx_Maschke rZ F'Zh) _. apply/sumsmx_subP=> i _; have simMi := simM i; have [modMi _ _] := simMi. set v := nz_row (M i); have nz_v: v != 0 by apply: nz_row_mxsimple simMi. have rankMi: \rank (M i) = 1%N. by rewrite (mxsimple_abelian_linear splitF _ simMi) //= ZhT Zp_abelian. have defMi: (M i :=: v)%MS. apply/eqmxP; rewrite andbC -(geq_leqif (mxrank_leqif_eq _)) ?nz_row_sub //. by rewrite rankMi lt0n mxrank_eq0. have [a defvg]: exists a, v *m rZ 1%R = a *: v. by apply/sub_rVP; rewrite -defMi mxmodule_trans ?socle_module ?defMi. have: a ^+ h - 1 == 0. apply: contraR nz_v => nz_pZa; rewrite -(eqmx_eq0 (eqmx_scale _ nz_pZa)). by rewrite scalerBl scale1r -lin_rZ // subr_eq0 char_Zp ?mulmx1. rewrite subr_eq0; move/eqP; case/(prim_rootP prim_eps) => k def_a. by rewrite defMi (sumsmx_sup k) // /V_ -def_a; apply/eigenspaceP. 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)