Nonsingular inverses
In this file, we define an inverse for square matrices of invertible
determinant. For matrices that are not square or not of full rank, there is a
more general notion of pseudoinverses. Unfortunately, the definition of
pseudoinverses is typically in terms of inverses of nonsingular matrices, so we
need to define those first. The file also doesn't define a has_inv instance
for matrix so that can be used for the pseudoinverse instead.
The definition of inverse used in this file is the adjugate divided by the determinant.
The adjugate is calculated with Cramer's rule, which we introduce first.
The vectors returned by Cramer's rule are given by the linear map cramer,
which sends a matrix A and vector b to the vector consisting of the
determinant of replacing the ith column of A with b at index i
(written as (A.update_column i b).det).
Using Cramer's rule, we can compute for each matrix A the matrix adjugate A.
The entries of the adjugate are the determinants of each minor of A.
Instead of defining a minor to be A with column i and row j deleted, we
replace the ith column of A with the jth basis vector; this has the same
determinant as the minor but more importantly equals Cramer's rule applied
to A and the jth basis vector, simplifying the subsequent proofs.
We prove the adjugate behaves like det A • A⁻¹. Finally, we show that dividing
the adjugate by det A (if possible), giving a matrix nonsing_inv A, will
result in a multiplicative inverse to A.
References
- https://en.wikipedia.org/wiki/Cramer's_rule#Finding_inverse_matrix
Tags
matrix inverse, cramer, cramer's rule, adjugate
cramer section
Introduce the linear map cramer with values defined by cramer_map.
After defining cramer_map and showing it is linear,
we will restrict our proofs to using cramer.
cramer_map A b i is the determinant of the matrix A with column i replaced with b,
and thus cramer_map A b is the vector output by Cramer's rule on A and b.
If A ⬝ x = b has a unique solution in x, cramer_map sends a square matrix A
and vector b to the vector x such that A ⬝ x = b.
Otherwise, the outcome of cramer_map is well-defined but not necessarily useful.
Equations
- A.cramer_map b i = (A.update_row i b).det
The linear map of vectors associated to Cramer's rule.
To help the elaborator, we need to make the type α an explicit argument to
cramer. Otherwise, the coercion ⇑(cramer A) : (n → α) → (n → α) gives an
error because it fails to infer the type (even though α can be inferred from
A : matrix n n α).
Equations
- matrix.cramer α A = is_linear_map.mk' A.cramer_map _
Applying Cramer's rule to a column of the matrix gives a scaled basis vector.
Use linearity of cramer to take it out of a summation.
Use linearity of cramer and vector evaluation to take cramer A _ i out of a summation.
adjugate section
Define the adjugate matrix and a few equations.
These will hold for any matrix over a commutative ring,
while the inv section is specifically for invertible matrices.
The adjugate matrix is the transpose of the cofactor matrix.
Typically, the cofactor matrix is defined by taking the determinant of minors,
i.e. the matrix with a row and column removed.
However, the proof of mul_adjugate becomes a lot easier if we define the
minor as replacing a column with a basis vector, since it allows us to use
facts about the cramer map.
det_adjugate_of_cancel is an auxiliary lemma for computing (adjugate A).det,
used in det_adjugate_eq_one and det_adjugate_of_is_unit.
The formula for the determinant of the adjugate of an n by n matrix A
is in general (adjugate A).det = A.det ^ (n - 1), but the proof differs in several cases.
This lemma det_adjugate_of_cancel covers the case that det A cancels
on the left of the equation A.det * b = A.det ^ n.
det_adjugate_of_is_unit gives the formula for (adjugate A).det if A.det has an inverse.
The formula for the determinant of the adjugate of an n by n matrix A
is in general (adjugate A).det = A.det ^ (n - 1), but the proof differs in several cases.
This lemma det_adjugate_of_is_unit covers the case that det A has an inverse.
inv section
Defines the matrix nonsing_inv A and proves it is the inverse matrix
of a square matrix A as long as det A has a multiplicative inverse.
The inverse of a square matrix, when it is invertible (and zero otherwise).
Equations
- matrix.has_inv = {inv := matrix.nonsing_inv _inst_3}
A matrix whose determinant is a unit is itself a unit.