proposition: Theorem Clifford_component_basis M : mxsimple rH M -> {t : nat & {x_ : sH -> 'I_t -> gT | forall W, let sW := (\sum_j M *m rG (x_ W j))%MS in [/\ forall j, x_ W j \in G, (sW :=: W)%MS & mxdirect sW]}}.
proof: Proof. move=> simM; pose t := (n %/ #|sH| %/ \rank M)%N; exists t. have [X /subsetP sXG [defX1 dxX1]] := Clifford_basis simM. pose sMv (W : sH) x := (M *m rG x <= W)%MS; pose Xv := [pred x in X | sMv _ x]. have sXvG W: {subset Xv W <= G} by move=> x /andP[/sXG]. have defW W: (\sum_(x in Xv W) M *m rG x :=: W)%MS. apply/eqmxP; rewrite -(geq_leqif (mxrank_leqif_eq _)); last first. by apply/sumsmx_subP=> x /andP[]. rewrite -(leq_add2r (\sum_(W' | W' != W) \rank W')) -((bigD1 W) predT) //=. rewrite -(mxdirectP (Socle_direct sH)) /= -/(Socle _) Clifford_Socle1 -defX1. apply: leq_trans (mxrankS _) (mxrank_sum_leqif _).1 => /=. rewrite (bigID (sMv W))%MS addsmxS //=. apply/sumsmx_subP=> x /andP[Xx notW_Mx]; have Gx := sXG x Xx. have simMx := Clifford_simple simM Gx. pose Wx := PackSocle (component_socle sH simMx). have sMxWx: (M *m rG x <= Wx)%MS by rewrite PackSocleK component_mx_id. by rewrite (sumsmx_sup Wx) //; apply: contra notW_Mx => /eqP <-. have dxXv W: mxdirect (\sum_(x in Xv W) M *m rG x). move: dxX1; rewrite !mxdirectE /= !(bigID (sMv W) [in X]) /=. by rewrite -mxdirectE mxdirect_addsE /= => /andP[]. have def_t W: #|Xv W| = t. rewrite /t -{1}(Clifford_rank_components W) mulKn 1?(cardD1 W) //. rewrite -defW (mxdirectP (dxXv W)) /= (eq_bigr (fun _ => \rank M)) => [|x]. rewrite sum_nat_const mulnK //; last by rewrite lt0n mxrank_eq0; case simM. by move/sXvG=> Gx; rewrite mxrankMfree // row_free_unit repr_mx_unit. exists (fun W i => enum_val (cast_ord (esym (def_t W)) i)) => W. case: {def_t}t / (def_t W) => sW. case: (pickP (Xv W)) => [x0 XvWx0 | XvW0]; last first. by case/negP: (nz_socle W); rewrite -submx0 -defW big_pred0. have{x0 XvWx0} reXv := reindex _ (enum_val_bij_in XvWx0). have def_sW: (sW :=: W)%MS. apply: eqmx_trans (defW W); apply/eqmxP; apply/genmxP; congr <<_>>%MS. rewrite reXv /=; apply: eq_big => [j | j _]; first by have:= enum_valP j. by rewrite cast_ord_id. split=> // [j|]; first by rewrite (sXvG W) ?enum_valP. apply/mxdirectP; rewrite def_sW -(defW W) /= (mxdirectP (dxXv W)) /= reXv /=. by apply: eq_big => [j | j _]; [move: (enum_valP j) | rewrite cast_ord_id]. 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)