Linear algebra in mathematical components

Extensive documentation in the header of:

• 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`

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)

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.

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`
.

• as a consequence, membership to a space is the same operation as comparison of spaces.

Addition of subspaces is not the same thing as addition of matrices.

(In Coq: same notation, different scope)

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