Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi Cyril, it's somewhat easier (and perhaps more natural) to derive this 
from the directness of the total sum, which can be proved arithmetically:

Lemma mxdirect_delta (F : fieldType) (I : finType) n (P : pred T)  f  :
  injective f -> mxdirect (\sum_(i | P i) <<delta_mx 0 (f i) : 'rV[F]_n>>).
Proof.
pose fP := image f P => Uf; have UfP: uniq fP by apply/dinjectiveP/(in2W Uf).
suffices /mxdirectP: mxdirect (\sum_i <<delta_mx 0 i : 'rV[F]_n>>).
  rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_filter.
  by move/mxdirectP; rewrite mxdirect_addsE => /andP[].
apply/mxdirectP=> /=; transitivity (mxrank (1%:M : 'M[F]_n)).
  apply/eqmx_rank; rewrite submx1 mx1_sum_delta summx_sub_sums // => i _.
  by rewrite -(mul_delta_mx (0 : 'I_1)) genmxE submxMl.
rewrite mxrank1 -[LHS]card_ord -sum1_card.
by apply/eq_bigr=> i _; rewrite /= mxrank_gen mxrank_delta.
Qed.

  Cheers,
Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Cyril
Sent: 20 November 2015 07:26
To: ssreflect 
<>
Subject: Re: [ssreflect] Direct sum of delta_mx

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