Linear algebra in mathematical components
Extensive documentation in the header of:
Roadmap for the lesson:
- definition of matrices
- main theorems
- help with depend types
- vector spaces as matrices
Defining Matrices
(Credits ITP 2013 tutorial: The Mathematical Components library
by Enrico Tassi and Assia Mahboubi material here)
A matrix is a 2-dimension array
Some notations : size inside parentheses, type of coefficients inside
square brackets. NB: In the library, the type of coefficients can also
be ommitted.
matrix
is just a tag over ffun: it inherits from its structure We
can transfer
automatically all structures from the type of finite
functions by trivial subTyping
.
Test overloaded "_ == _" notation
Since matrices over nat are comparable with _ == _, matrices over
matrices over nat are also comparable
We define a coercion in order to access elements as if matrices were
functions.
We provide a notation to build matrices from a general term.
Main Theorems
We now show the most used theorems for matrix manipulation.
mxE
mxE is an equation to compute a term in the matrix at given
coordinates: it extracts the general term of the matrix and compute
the substitution of indexes. It is generally the right move when you
have
(A complicated matrix) i j
in your goal.
matrixP
matrixP is the extensionality theorem
for matrices, it says two
matrices are equal if and only if all their coefficients are pairwise
equal.
operations on matrices
specific operation: trace and transpose
(do not confuse the names)
specific operation scalar matrix
matrices on rings are provided with a R-module canonical structure.
But not a ring as the multiplication is heterogeneous.
square matrices with explicit non zero size have a ring canonical structure.
This ring product coincides with the matrix product.
specific operation: the determinant.
square matrices on a commutative unit ring with explicit non zero size have a unit ring canonical structure.
and these notions of inversibility are definitionally equivalent.
SUB VECTOR SPACES AS MATRICES
General understanding
- A specificity of the mathematical components library is to allow to
reason on matrices as if they represented their own image.
- The doc and the code are in mxalgebra)
- rows can be seen as vectors, and matrix can be seen as the familiy
of its row vectors.
- WARNING Following the english convention (which is
opposite to the french convention), composition/application of
linear maps represented by matrices should be done left to right:
applying A to u is
u *m A
.
- the scope MS (matrix space) contains all notions about this vision
of matrices (comparison, addition, intersection of spaces).
- as a consequence, membership to a space is the same operation as
comparison of spaces.
the rank of a matrix is also the dimension of the space it represents
Inclusion can be used both for elements (row vectors) and subspaces (matrices).
The total space is represented by 1, and the trivial space by 0.
Addition of subspaces is not the same thing as addition of matrices.
(In Coq: same notation, different scope)
Intersection of subspaces
Equality of subspaces is double inclusion.
Alternatively, the library provides an equivalent definition (via
eqmxP) that can be used for rewriting in inclusion statements or rank.
Usage.
- Im A is represented by the matrix A itself.
- vectors of a space represented by the matrix A are linear
combinations of the rows of A, which amount to making a product by
an element (i.e. row of coefficients, or coordinates in the family
generated by A) on the left.
- Ker A is represented by the square matrix kermx A.
Let's do an example together