Ssreflect Users Discussion List

[Xavier Allamigeon <>]

Dear SSReflect-list,

Ricardo Katz (cc'ed) and myself are currently working on polyhedra and 
polyhedral cones within SSReflect. For this purpose, we need some basic 
linear algebra operations and statements.
So far, we used matrices and vectors through the module Matrix, but now 
comes the time make some proof involving the dimension of some 
subspaces, kernel of linear maps, completion of free families of 
vectors, etc.

As far as we can see, mxalgebra provides several useful constructions. 
However, the more abstract interface provided by the module Vector would 
better suited for our needs (and proofs would be more elegant).
Even though the implementation of Vector is based on matrices, this part 
is supposed to be hidden, according to the documentation of 
Vector.InternalTheory. In consequence, we don't understand how to easily 
make the connections between the two layers.

As an example, we would like to define the kernel of the linear map 
associated with a matrix A: 'M_(m,n), and relate its dimension with the 
rank of the matrix A. For this purpose, we introduced the linear map
linfun_mx A := linfun (mulmx A): 'Hom(Vm, Vn)
where Vm and Vn are matrix_vectType of dimension m 1 and n 1 
respectively. Then, we defined
ker A := lker (linfun_mx A)
and we could  straightforwardly check that it consists the vectors x: 
'cV_n such that A *m x == 0.
But now, we don't see how to prove that
\dim ker A = n - \rank A
unless going into the internal representation of the module Vector 
(which we would like to avoid...).

Which is the best approach for this problem?

Thanks in advance,

Best regards.
Xavier