Ssreflect Users Discussion List

[Cyril <>]

On 20/11/2015 15:43, Cyril wrote:
> Hi, I would like to prove that the subspaces generated by the delta_mx form
> a direct sum. I expected it to be immediate and I can't find a solution.
> 
> Any help ?
> 
> Lemma mxdirect_delta (F : fieldType) (T : finType)
>   (n : nat) (P : pred T) (f : T -> 'I_n) :
>   injective f ->
>   mxdirect (\sum_(i | P i) <<delta_mx 0 (f i) : 'rV[F]_n>>)%MS.
> 
> Best,
> 

FYI, this is my proof:

Lemma mxdirect_delta (F : fieldType) (T : finType)
  (n : nat) (P : pred T) (f : T -> 'I_n) :
  injective f ->
  mxdirect (\sum_(i | P i) <<delta_mx 0 (f i) : 'rV[F]_n>>)%MS.
Proof.
move=> f_inj; apply/mxdirectP => /=.
transitivity (\rank (\sum_(j | P j) (delta_mx (f j) (f j) : 'M[F]_n))).
  apply: eqmx_rank; apply/genmxP; rewrite !genmx_sums.
  apply/eq_bigr => i Pi; rewrite genmx_id.
  apply/genmxP/andP; split; apply/submxP.
    by exists (delta_mx 0 (f i)); rewrite mul_delta_mx.
  by exists (delta_mx (f i) 0); rewrite mul_delta_mx.
rewrite [RHS](eq_bigr (fun j : T => \rank (delta_mx (f j) (f j) : 'M[F]_n)));
  last by move=> i Pi; rewrite mxrank_gen !mxrank_delta.
apply/mxdirectP => /=.
apply/mxdirect_sumsP => /= s Ps.
apply/eqP; rewrite -submx0; apply/rV_subP => u.
rewrite sub_capmx => /andP [/submxP [x ->]].
move=> /(submxMr (delta_mx (f s) (f s))).
rewrite sumsmxMr_gen big1; first by rewrite -mulmxA mul_delta_mx.
by move=> i /andP [Pi neq_is]; rewrite mul_delta_mx_0 ?genmx0 ?(inj_eq f_inj).
Qed.

-- 
Cyril