diff options
| author | Cyril Cohen | 2018-01-26 17:55:39 +0100 |
|---|---|---|
| committer | GitHub | 2018-01-26 17:55:39 +0100 |
| commit | 64c6b07ff318b9eee032e929f0cd25b2e2ddaeda (patch) | |
| tree | 4beb94be944e8772dc95d1a544ce9ce2201d51dc /mathcomp | |
| parent | d4bd8f6a29a225cf7418c54008b6493501c62bd3 (diff) | |
| parent | c6e4012ec499b100abfd19320b6790d9849eba9e (diff) | |
Merge pull request #171 from CohenCyril/mxdirect_delta
The spaces generated by some delta_mx are in a direct sum
Diffstat (limited to 'mathcomp')
| -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. |