mathlib3 documentation

linear_algebra.matrix.adjugate

Cramer's rule and adjugate matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The adjugate matrix is the transpose of the cofactor matrix. It 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 minors of A. Instead of defining a minor by deleting row i and column j of A, we replace the ith row of A with the jth basis vector; the resulting matrix has the same determinant 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⁻¹.

Main definitions #

matrix.cramer A b: the vector output by Cramer's rule on A and b.
matrix.adjugate A: the adjugate (or classical adjoint) of the matrix A.

References #

https://en.wikipedia.org/wiki/Cramer's_rule#Finding_inverse_matrix

Tags #

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 v} {α : Type w} [decidable_eq n] [fintype n] [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 v} {α : Type w} [decidable_eq n] [fintype n] [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 v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) :

is_linear_map α A.cramer_map

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

⇑(A.cramer) b i = (A.update_column i b).det

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

⇑(A.transpose.cramer) b i = (A.update_row i b).det

theorem matrix.cramer_transpose_row_self {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (i : n) :

⇑(A.transpose.cramer) (A i) = pi.single i A.det

theorem matrix.cramer_row_self {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (b : n → α) (i : n) (h : ∀ (j : n), b j = A j i) :

⇑(A.cramer) b = pi.single i A.det

@[simp]

theorem matrix.cramer_one {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] :

theorem matrix.cramer_smul {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (r : α) (A : matrix n n α) :

(r • A).cramer = r ^ (fintype.card n - 1) • A.cramer

@[simp]

theorem matrix.cramer_subsingleton_apply {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] [subsingleton n] (A : matrix n n α) (b : n → α) (i : n) :

⇑(A.cramer) b i = b i

theorem matrix.cramer_zero {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] [nontrivial n] :

theorem matrix.sum_cramer {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) {β : Type u_1} (s : finset β) (f : β → n → α) :

s.sum (λ (x : β), ⇑(A.cramer) (f x)) = ⇑(A.cramer) (s.sum (λ (x : β), f x))

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

theorem matrix.sum_cramer_apply {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) {β : Type u_1} (s : finset β) (f : n → β → α) (i : n) :

s.sum (λ (x : β), ⇑(A.cramer) (λ (j : n), f j x) i) = ⇑(A.cramer) (λ (j : n), s.sum (λ (x : β), f j x)) i

Use linearity of cramer and vector evaluation to take cramer A _ i out of a summation.

theorem matrix.cramer_submatrix_equiv {m : Type u} {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] [comm_ring α] (A : matrix m m α) (e : n ≃ m) (b : n → α) :

⇑((A.submatrix ⇑e ⇑e).cramer) b = ⇑(A.cramer) (b ∘ ⇑(e.symm)) ∘ ⇑e

theorem matrix.cramer_reindex {m : Type u} {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] [comm_ring α] (e : m ≃ n) (A : matrix m m α) (b : n → α) :

⇑((⇑(matrix.reindex e e) A).cramer) b = ⇑(A.cramer) (b ∘ ⇑e) ∘ ⇑(e.symm)

`adjugate` section #

Define the adjugate matrix and a few equations. These will hold for any matrix over a commutative ring.

def matrix.adjugate {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [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 minors, i.e. the determinant of the matrix with a row and column removed. However, the proof of mul_adjugate becomes a lot easier if we use the matrix replacing a column with a basis vector, since it allows us to use facts about the cramer map.

Equations

A.adjugate = ⇑matrix.of (λ (i : n), ⇑(A.transpose.cramer) (pi.single i 1))

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

A.adjugate = ⇑matrix.of (λ (i : n), ⇑(A.transpose.cramer) (pi.single i 1))

theorem matrix.adjugate_apply {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (i j : n) :

A.adjugate i j = (A.update_row j (pi.single i 1)).det

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

A.adjugate.transpose = A.transpose.adjugate

@[simp]

theorem matrix.adjugate_submatrix_equiv_self {m : Type u} {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] [comm_ring α] (e : n ≃ m) (A : matrix m m α) :

(A.submatrix ⇑e ⇑e).adjugate = A.adjugate.submatrix ⇑e ⇑e

theorem matrix.adjugate_reindex {m : Type u} {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] [comm_ring α] (e : m ≃ n) (A : matrix m m α) :

(⇑(matrix.reindex e e) A).adjugate = ⇑(matrix.reindex e e) A.adjugate

theorem matrix.cramer_eq_adjugate_mul_vec {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [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 v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (i j k : n) :

A i k * A.adjugate k j = ⇑(A.transpose.cramer) (pi.single k (A i k)) j

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

A.mul A.adjugate = A.det • 1

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

A.adjugate.mul A = A.det • 1

theorem matrix.adjugate_smul {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (r : α) (A : matrix n n α) :

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

@[simp]

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

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

A stronger form of Cramer's rule that allows us to solve some instances of A ⬝ x = b even if the determinant is not a unit. A sufficient (but still not necessary) condition is that A.det divides b.

theorem matrix.adjugate_subsingleton {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] [subsingleton n] (A : matrix n n α) :

theorem matrix.adjugate_eq_one_of_card_eq_one {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] {A : matrix n n α} (h : fintype.card n = 1) :

@[simp]

theorem matrix.adjugate_zero {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] [nontrivial n] :

@[simp]

theorem matrix.adjugate_one {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] :

@[simp]

theorem matrix.adjugate_diagonal {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (v : n → α) :

(matrix.diagonal v).adjugate = matrix.diagonal (λ (i : n), (finset.univ.erase i).prod (λ (j : n), v j))

theorem ring_hom.map_adjugate {n : Type v} [decidable_eq n] [fintype n] {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R →+* S) (M : matrix n n R) :

⇑(f.map_matrix) M.adjugate = (⇑(f.map_matrix) M).adjugate

theorem alg_hom.map_adjugate {n : Type v} [decidable_eq n] [fintype n] {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (M : matrix n n A) :

⇑(f.map_matrix) M.adjugate = (⇑(f.map_matrix) M).adjugate

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

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

@[simp]

theorem matrix.adjugate_fin_zero {α : Type w} [comm_ring α] (A : matrix (fin 0) (fin 0) α) :

@[simp]

theorem matrix.adjugate_fin_one {α : Type w} [comm_ring α] (A : matrix (fin 1) (fin 1) α) :

theorem matrix.adjugate_fin_two {α : Type w} [comm_ring α] (A : matrix (fin 2) (fin 2) α) :

A.adjugate = ⇑matrix.of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]]

@[simp]

theorem matrix.adjugate_fin_two_of {α : Type w} [comm_ring α] (a b c d : α) :

(⇑matrix.of ![![a, b], ![c, d]]).adjugate = ⇑matrix.of ![![d, -b], ![-c, a]]

theorem matrix.adjugate_fin_succ_eq_det_submatrix {α : Type w} [comm_ring α] {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) α) (i j : fin n.succ) :

A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix ⇑(j.succ_above) ⇑(i.succ_above)).det

theorem matrix.det_eq_sum_mul_adjugate_row {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (i : n) :

A.det = finset.univ.sum (λ (j : n), A i j * A.adjugate j i)

theorem matrix.det_eq_sum_mul_adjugate_col {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (j : n) :

A.det = finset.univ.sum (λ (i : n), A i j * A.adjugate j i)

theorem matrix.adjugate_conj_transpose {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] [star_ring α] (A : matrix n n α) :

A.adjugate.conj_transpose = A.conj_transpose.adjugate

theorem matrix.is_regular_of_is_left_regular_det {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] {A : matrix n n α} (hA : is_left_regular A.det) :

theorem matrix.adjugate_mul_distrib_aux {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A B : matrix n n α) (hA : is_left_regular A.det) (hB : is_left_regular B.det) :

(A.mul B).adjugate = B.adjugate.mul A.adjugate

theorem matrix.adjugate_mul_distrib {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A B : matrix n n α) :

(A.mul B).adjugate = B.adjugate.mul A.adjugate

Proof follows from "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3

@[simp]

theorem matrix.adjugate_pow {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (k : ℕ) :

(A ^ k).adjugate = A.adjugate ^ k

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

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

theorem matrix.adjugate_adjugate {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) (h : fintype.card n ≠ 1) :

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

Note that this is not true for fintype.card n = 1 since 1 - 2 = 0 and not -1.

theorem matrix.adjugate_adjugate' {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : matrix n n α) [nontrivial n] :

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

A weaker version of matrix.adjugate_adjugate that uses nontrivial.