proposition: Lemma repr_rsim_diag (G : {group gT}) f (rG : mx_representation algC G f) x : x \in G -> let chi := cfRepr rG in exists e, [/\ exists2 B, B \in unitmx & rG x = invmx B *m diag_mx e *m B, (forall i, e 0 i ^+ #[x] = 1) /\ (forall i, `|e 0 i| = 1), chi x = \sum_i e 0 i /\ `|chi x| <= chi 1%g & chi x^-1%g = (chi x)^*].
proof: Proof. move=> Gx; without loss cGG: G rG Gx / abelian G. have sXG: <[x]> \subset G by rewrite cycle_subG. move/(_ _ (subg_repr rG sXG) (cycle_id x) (cycle_abelian x)). by rewrite /= !cfunE !groupV Gx (cycle_id x) !group1. have [I U W simU W1 dxW]: mxsemisimple rG 1%:M. rewrite -(reducible_Socle1 (DecSocleType rG) (mx_Maschke _ (algC'G G))). exact: Socle_semisimple. have linU i: \rank (U i) = 1. by apply: mxsimple_abelian_linear cGG (simU i); apply: groupC. have castI: f = #|I|. by rewrite -(mxrank1 algC f) -W1 (eqnP dxW) /= -sum1_card; apply/eq_bigr. pose B := \matrix_j nz_row (U (enum_val (cast_ord castI j))). have rowU i: (nz_row (U i) :=: U i)%MS. apply/eqmxP; rewrite -(geq_leqif (mxrank_leqif_eq (nz_row_sub _))) linU. by rewrite lt0n mxrank_eq0 (nz_row_mxsimple (simU i)). have unitB: B \in unitmx. rewrite -row_full_unit -sub1mx -W1; apply/sumsmx_subP=> i _. pose j := cast_ord (esym castI) (enum_rank i). by rewrite (submx_trans _ (row_sub j B)) // rowK cast_ordKV enum_rankK rowU. pose e := \row_j row j (B *m rG x *m invmx B) 0 j. have rGx: rG x = invmx B *m diag_mx e *m B. rewrite -mulmxA; apply: canRL (mulKmx unitB) _. apply/row_matrixP=> j; rewrite 2!row_mul; set u := row j B. have /sub_rVP[a def_ux]: (u *m rG x <= u)%MS. rewrite /u rowK rowU (eqmxMr _ (rowU _)). exact: (mxmoduleP (mxsimple_module (simU _))). rewrite def_ux [u]rowE scalemxAl; congr (_ *m _). apply/rowP=> k; rewrite 5!mxE !row_mul def_ux [u]rowE scalemxAl mulmxK //. by rewrite !mxE !eqxx !mulr_natr eq_sym. have exp_e j: e 0 j ^+ #[x] = 1. suffices: (diag_mx e j j) ^+ #[x] = (B *m rG (x ^+ #[x])%g *m invmx B) j j. by rewrite expg_order repr_mx1 mulmx1 mulmxV // [e]lock !mxE eqxx. elim: #[x] => [|n IHn]; first by rewrite repr_mx1 mulmx1 mulmxV // !mxE eqxx. rewrite expgS repr_mxM ?groupX // {1}rGx -!mulmxA mulKVmx //. by rewrite mul_diag_mx mulmxA [M in _ = M]mxE -IHn exprS {1}mxE eqxx. have norm1_e j: `|e 0 j| = 1. by apply/eqP; rewrite -(@pexpr_eq1 _ _ #[x]) // -normrX exp_e normr1. exists e; split=> //; first by exists B. rewrite cfRepr1 !cfunE Gx rGx mxtrace_mulC mulKVmx // mxtrace_diag. split=> //=; apply: (le_trans (ler_norm_sum _ _ _)). by rewrite (eq_bigr _ (in1W norm1_e)) sumr_const card_ord lexx. rewrite !cfunE groupV !mulrb Gx rGx mxtrace_mulC mulKVmx //. rewrite -trace_map_mx map_diag_mx; set d' := diag_mx _. rewrite -[d'](mulKVmx unitB) mxtrace_mulC -[_ *m _](repr_mxK rG Gx) rGx. rewrite -!mulmxA mulKVmx // (mulmxA d'). suffices->: d' *m diag_mx e = 1%:M by rewrite mul1mx mulKmx. rewrite mulmx_diag -diag_const_mx; congr diag_mx; apply/rowP=> j. by rewrite [e]lock !mxE mulrC -normCK -lock norm1_e expr1n. 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)