mathlib documentation

linear_algebra.nonsingular_inverse

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 which we do not consider here.

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 row i and column j deleted, we replace the ith row 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

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.

def matrix.cramer_map {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] :
matrix n n α(n → α)n → α

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 A sends the vector b to A.det • x. Otherwise, the outcome of cramer_map is well-defined but not necessarily useful.

Equations
theorem matrix.cramer_map_is_linear {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (i : n) :
is_linear_map α (λ (b : n → α), A.cramer_map b i)

theorem matrix.cramer_is_linear {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :

def matrix.cramer {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] :
matrix n n α((n → α) →ₗ[α] n → α)

cramer A b i is the determinant of the matrix A with column i replaced with b, and thus cramer 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 A sends the vector b to A.det • x. Otherwise, the outcome of cramer is well-defined but not necessarily useful.

Equations
theorem matrix.cramer_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (b : n → α) (i : n) :
(A.cramer) b i = (A.update_column i b).det

theorem matrix.cramer_transpose_row_self {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (i : n) :
(A.cramer) (A i) = λ (j : n), ite (i = j) A.det 0

theorem matrix.sum_cramer {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) {β : Type u_1} (s : finset β) (f : β → n → α) :
∑ (x : β) in s, (A.cramer) (f x) = (A.cramer) (∑ (x : β) in s, f x)

Use linearity of cramer to take it out of a summation.

theorem matrix.sum_cramer_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) {β : Type u_1} (s : finset β) (f : n → β → α) (i : n) :
∑ (x : β) in s, (A.cramer) (λ (j : n), f j x) i = (A.cramer) (λ (j : n), ∑ (x : β) in s, f j x) i

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.

def matrix.adjugate {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] :
matrix n n αmatrix n n α

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.

Equations
theorem matrix.adjugate_def {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :
A.adjugate = λ (i : n), (A.cramer) (λ (j : n), ite (i = j) 1 0)

theorem matrix.adjugate_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (i j : n) :
A.adjugate i j = (A.update_row j (λ (j : n), ite (i = j) 1 0)).det

theorem matrix.adjugate_transpose {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :

theorem matrix.cramer_eq_adjugate_mul_vec {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (b : n → α) :

Since the map b ↦ cramer A b is linear in b, it must be multiplication by some matrix. This matrix is A.adjugate.

theorem matrix.mul_adjugate_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (i j k : n) :
(A i k) * A.adjugate k j = (A.cramer) (λ (j : n), ite (k = j) (A i k) 0) j

theorem matrix.mul_adjugate {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :
A A.adjugate = A.det 1

theorem matrix.adjugate_mul {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :
A.adjugate A = A.det 1

theorem matrix.det_adjugate_of_cancel {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] {A : matrix n n α} :
(∀ (b : α), (A.det) * b = A.det ^ fintype.card nb = A.det ^ (fintype.card n - 1))A.adjugate.det = A.det ^ (fintype.card n - 1)

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.

theorem matrix.adjugate_eq_one_of_card_eq_one {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] {A : matrix n n α} :
fintype.card n = 1A.adjugate = 1

@[simp]
theorem matrix.adjugate_zero {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] :
1 < fintype.card n0.adjugate = 0

theorem matrix.det_adjugate_eq_one {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] {A : matrix n n α} :
A.det = 1A.adjugate.det = 1

theorem matrix.det_adjugate_of_is_unit {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] {A : matrix n 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.

theorem matrix.is_unit_det_transpose {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :

def matrix.nonsing_inv {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] :
matrix n n αmatrix n n α

The inverse of a square matrix, when it is invertible (and zero otherwise).

Equations
@[instance]
def matrix.has_inv {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] :
has_inv (matrix n n α)

Equations
theorem matrix.nonsing_inv_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (h : is_unit A.det) :

theorem matrix.transpose_nonsing_inv {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :

@[simp]
theorem matrix.mul_nonsing_inv {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :
is_unit A.detA A⁻¹ = 1

The nonsing_inv of A is a right inverse.

@[simp]
theorem matrix.nonsing_inv_mul {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :
is_unit A.detA⁻¹ A = 1

The nonsing_inv of A is a left inverse.

@[simp]
theorem matrix.nonsing_inv_det {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :
is_unit A.det(A⁻¹.det) * A.det = 1

theorem matrix.is_unit_nonsing_inv_det {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :

@[simp]
theorem matrix.nonsing_inv_nonsing_inv {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :

def matrix.nonsing_inv_unit {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :
is_unit A.detunits (matrix n n α)

A matrix whose determinant is a unit is itself a unit.

Equations
theorem matrix.is_unit_iff_is_unit_det {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) :

theorem matrix.is_unit_det_of_left_inverse {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A B : matrix n n α) :
B A = 1is_unit A.det

theorem matrix.is_unit_det_of_right_inverse {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A B : matrix n n α) :
A B = 1is_unit A.det

theorem matrix.nonsing_inv_left_right {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A B : matrix n n α) :
A B = 1B A = 1

theorem matrix.nonsing_inv_right_left {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A B : matrix n n α) :
B A = 1A B = 1

@[simp]
theorem matrix.det_smul_inv_mul_vec_eq_cramer {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (b : n → α) :

@[simp]
theorem matrix.mul_vec_cramer {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (b : n → α) :
A.mul_vec ((A.cramer) b) = A.det b