proposition: Lemma codiagonalizable_on m n (V_ : 'I_n -> 'M[F]_m) (As : seq 'M[F]_m) : (\sum_i V_ i :=: 1%:M)%MS -> mxdirect (\sum_i V_ i) -> (forall i, all (fun A => stablemx (V_ i) A) As) -> (forall i, codiagonalizable (map (restrictmx (V_ i)) As)) -> codiagonalizable As.
proof: Proof. move=> V1 Vdirect /(_ _)/allP AV /(_ _) /sig2W/= Pof. pose P_ i := tag (Pof i). have P_unit i : P_ i \in unitmx by rewrite /P_; case: {+}Pof. have P_diag i A : A \in As -> diagonalizable_for (P_ i *m row_base (V_ i)) A. move=> AAs; rewrite /P_; case: {+}Pof => /= P Punit. rewrite all_map => /allP/(_ A AAs); rewrite /= !/(diagonalizable_for _ _). by rewrite conjuMmx ?row_base_free ?stablemx_row_base ?AV. pose P := \mxcol_i (P_ i *m row_base (V_ i)). have P_full i : row_full (P_ i) by rewrite row_full_unit. have PrV i : (P_ i *m row_base (V_ i) :=: V_ i)%MS. exact/(eqmx_trans _ (eq_row_base _))/eqmxMfull. apply/codiagonalizablePfull; eexists _; last exists P; rewrite /=. - rewrite -sub1mx eqmx_col. by under eq_bigr do rewrite (eq_genmx (PrV _)); rewrite -genmx_sums genmxE V1. apply/allP => A AAs /=; rewrite diagonalizable_for_sum. - by apply/forallP => i; apply: P_diag. - rewrite mxdirectE/=. under eq_bigr do rewrite (eq_genmx (PrV _)); rewrite -genmx_sums genmxE V1. by under eq_bigr do rewrite genmxE PrV; rewrite -(mxdirectP Vdirect)//= V1. - by move=> i; rewrite (eqmx_stable _ (PrV _)) ?AV. - by move=> i; rewrite /row_free eqmxMfull ?eq_row_base ?row_full_unit. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)