Stream: math-comp users

Topic: About vectType


view this post on Zulip Sylvie Boldo (May 03 2022 at 11:17):

Hello! I am looking for information about math-comp type VectType (for finite-dimensional vector space)
1) Is there information other than https://math-comp.github.io/htmldoc_1_12_0/mathcomp.algebra.vector.html ?
2) Are there bijections from and to different VectTypes when their dimension is equal?
3) Is there a proof that polynomials of a given degree (smaller than n) form a VectType?
Thanks!

view this post on Zulip Cyril Cohen (May 03 2022 at 12:02):

Sylvie Boldo said:

Hello! I am looking for information about math-comp type VectType (for finite-dimensional vector space)
1) Is there information other than https://math-comp.github.io/htmldoc_1_12_0/mathcomp.algebra.vector.html ?

I don't think there is another doc, no.

2) Are there bijections from and to different VectTypes when their dimension is equal?

I'm not aware of such a contribution. It wouldn't be too hard to add though, I could do it or guide anyone trying to do it.

3) Is there a proof that polynomials of a given degree (smaller than n) form a VectType?

There is this old PR which should be refreshed and merged.

view this post on Zulip Cyril Cohen (May 03 2022 at 12:17):

I suggest to define:

Definition vspace_fun {vT vT' : vectType} (U : {vspace vT}) (V : {vspace vT'}) (v : vT) :=
  \sum_(i < \dim U) coord (vbasis U) i v *: (vbasis V)`_i

And prove stuff like:

Lemma  vspace_fun (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) : \dim U <= \dim V ->
  cancel (vspace_fun U V) (vspace_fun V U).
Proof. ... Admitted.

and

Lemma vspace_is_linear (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) :
  linear (vspace_fun U V).
Proof. ... Admitted.
Canonical vspace_fun_linear (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) :=
  Linear (vspace_is_linear U V).

view this post on Zulip Sylvie Boldo (May 03 2022 at 12:31):

Thanks! I'll have a look at all that.

view this post on Zulip Sylvie Boldo (May 03 2022 at 14:25):

(U <= V)%VS was not typing indeed. I also changed it to (\dim U <= \dim V)%nat :-)
But I have problems proving the cancel property on vspace_fun as it seems to require that v \in U. Did I miss something?


Last updated: Mar 28 2024 at 18:02 UTC