diff options
| author | Cyril Cohen | 2017-12-12 20:01:11 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2017-12-14 13:22:31 +0100 |
| commit | c6e4012ec499b100abfd19320b6790d9849eba9e (patch) | |
| tree | b1d361fbd85bcd474d9fd6a937297f25a8aa36aa | |
| parent | 3e0f4874ce1d421e6a65eb8e745c666cb0313373 (diff) | |
The spaces generated by some delta_mx are in a direct sum
proof by @ggonthier
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index da61dfb..1b6200e 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2087,6 +2087,25 @@ Notation "\bigcap_ ( i 'in' A | P ) B" := Notation "\bigcap_ ( i 'in' A ) B" := (\big[capmx/1%:M]_(i in A) B%MS) : matrix_set_scope. +Section DirectSums. +Variables (F : fieldType) (I : finType) (P : pred I). + +Lemma mxdirect_delta n f : {in P &, 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. +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. + +End DirectSums. + Section CardGL. Variable F : finFieldType. |