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 #

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.

def matrix.cramer_map {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (A : matrix n n α) (b : n → α) (i : 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

A.cramer_map b i = (A.update_column i b).det

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 α) :

is_linear_map α A.cramer_map

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

A.cramer = is_linear_map.mk' A.cramer_map _

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 α] (A : 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

A.adjugate = λ (i : n), ⇑(Aᵀ.cramer) (λ (j : n), ite (i = j) 1 0)

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 α) :

(A.adjugate)ᵀ = Aᵀ.adjugate

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 → α) :

⇑(A.cramer) b = A.adjugate.mul_vec b

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 α} (h : ∀ (b : α), (A.det) * b = A.det ^ fintype.card n → b = 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 α} (h : fintype.card n = 1) :

@[simp]

theorem matrix.adjugate_zero {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] (h : 1 < fintype.card n) :

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

A.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 α} (h : is_unit A.det) :

A.adjugate.det = A.det ^ (fintype.card n - 1)

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 α) (h : is_unit A.det) :

is_unit Aᵀ.det

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

matrix n n α

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

Equations

A.nonsing_inv = dite (is_unit A.det) (λ (h : is_unit A.det), ↑(h.unit)⁻¹ • A.adjugate) (λ (h : ¬is_unit A.det), 0)

@[protected, instance]

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

has_inv (matrix n n α)

Equations

matrix.has_inv = {inv := matrix.nonsing_inv _inst_3}

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) :

A⁻¹ = ↑(h.unit)⁻¹ • A.adjugate

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

A⁻¹ ᵀ = Aᵀ ⁻¹

@[simp]

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

A ⬝ 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 α) (h : is_unit A.det) :

A⁻¹ ⬝ 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 α) (h : 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 α) (h : is_unit A.det) :

is_unit A⁻¹.det

@[simp]

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

A⁻¹ ⁻¹ = A

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

units (matrix n n α)

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

Equations

A.nonsing_inv_unit h = {val := A, inv := A⁻¹, val_inv := _, inv_val := _}

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

is_unit A ↔ is_unit A.det

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 α) (h : B ⬝ A = 1) :

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 α) (h : A ⬝ B = 1) :

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

B ⬝ 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 α) (h : B ⬝ A = 1) :

A ⬝ 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 → α) (h : is_unit A.det) :

A.det • A⁻¹.mul_vec b = ⇑(A.cramer) b

@[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