Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear all,

mathcomp provide a strong library for linear algebra, providing the theory of
matrices and on top of it a notion of finite dimensional vector
space. However, as in usual textbook about linear algebra matrix as well
vector have their coordinate indexed by integer in some 'I_n. While this is
sufficient in theory, this is often non very pratical. More precisely in
various usage one lives in a free module (or vector space if the scalar comes
from a field) over a set which caries some important extra structure. Here
are two basic examples, but there are a lot more:

1 - The Group algebra K[G] for a finite group G. It is very natural to write 
the
  elements as

     x = \sum_(g : G) x_g *: e_g

  where x_g : K and e_g is the basis element indexed by g.

2 - When doing linear algebra inside multivariate polynomials as for example 
in
  a Groebner basis computation. In this case, we have to bound the degree to
  be on a finType.

Of course one can always go back and forth to the canonical enumeration using
enum_val (as it is for example done for class function) but it carries no
information at all on the interesting structure on the basic set.  Think for
example in the two previous examples statement such as

     x = \sum_(g | G \in H) e_g   (where H is a subgroup).

Or

     p = \sum_(m | m <= m' for a monomial order) a_m m.

Is there some infrastructure to deal with those kinds of linear algebra
manipulation in mathcomp ? Is there any suggestion for playing with those kind
of things ?

Cheers,

Florent