Cramer's rule and adjugate matrices

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 cramerMap. After defining cramerMap and showing it is linear, we will restrict our proofs to using cramer.

def Matrix.cramerMap {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) (i : n) : α

cramerMap A b i is the determinant of the matrix A with column i replaced with b, and thus cramerMap A b is the vector output by Cramer's rule on A and b.

If A * x = b has a unique solution in x, cramerMap A sends the vector b to A.det • x. Otherwise, the outcome of cramerMap is well-defined but not necessarily useful.

Equations

• Matrix.cramerMap A b i = Matrix.det (Matrix.updateColumn A i b)

theorem Matrix.cramerMap_is_linear {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) : IsLinearMap α fun (b : n → α) => Matrix.cramerMap A b i

theorem Matrix.cramer_is_linear {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : IsLinearMap α (Matrix.cramerMap A)

def Matrix.cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (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

• Matrix.cramer A = IsLinearMap.mk' (Matrix.cramerMap A) (_ : IsLinearMap α (Matrix.cramerMap A))

theorem Matrix.cramer_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) (i : n) : (Matrix.cramer A) b i = Matrix.det (Matrix.updateColumn A i b)

theorem Matrix.cramer_transpose_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) (i : n) : (Matrix.cramer (Matrix.transpose A)) b i = Matrix.det (Matrix.updateRow A i b)

theorem Matrix.cramer_transpose_row_self {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) : (Matrix.cramer (Matrix.transpose A)) (A i) = Pi.single i (Matrix.det A)

theorem Matrix.cramer_row_self {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) (i : n) (h : ∀ (j : n), b j = A j i) : (Matrix.cramer A) b = Pi.single i (Matrix.det A)

@[simp]

theorem Matrix.cramer_one {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] : Matrix.cramer 1 = 1

theorem Matrix.cramer_smul {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (r : α) (A : Matrix n n α) : Matrix.cramer (r • A) = r ^ (Fintype.card n - 1) • Matrix.cramer A

@[simp]

theorem Matrix.cramer_subsingleton_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [Subsingleton n] (A : Matrix n n α) (b : n → α) (i : n) : (Matrix.cramer A) b i = b i

theorem Matrix.cramer_zero {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [Nontrivial n] : Matrix.cramer 0 = 0

theorem Matrix.sum_cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) {β : Type u_1} (s : Finset β) (f : β → n → α) : (Finset.sum s fun (x : β) => (Matrix.cramer A) (f x)) = (Matrix.cramer A) (Finset.sum s fun (x : β) => f x)

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

theorem Matrix.sum_cramer_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) {β : Type u_1} (s : Finset β) (f : n → β → α) (i : n) : (Finset.sum s fun (x : β) => (Matrix.cramer A) (fun (j : n) => f j x) i) = (Matrix.cramer A) (fun (j : n) => Finset.sum s fun (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} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (A : Matrix m m α) (e : n ≃ m) (b : n → α) : (Matrix.cramer (Matrix.submatrix A ⇑e ⇑e)) b = (Matrix.cramer A) (b ∘ ⇑e.symm) ∘ ⇑e

theorem Matrix.cramer_reindex {m : Type u} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (e : m ≃ n) (A : Matrix m m α) (b : n → α) : (Matrix.cramer ((Matrix.reindex e e) A)) b = (Matrix.cramer A) (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} [DecidableEq n] [Fintype n] [CommRing α] (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

• Matrix.adjugate A = Matrix.of fun (i : n) => (Matrix.cramer (Matrix.transpose A)) (Pi.single i 1)

theorem Matrix.adjugate_def {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : Matrix.adjugate A = Matrix.of fun (i : n) => (Matrix.cramer (Matrix.transpose A)) (Pi.single i 1)

theorem Matrix.adjugate_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) (j : n) : Matrix.adjugate A i j = Matrix.det (Matrix.updateRow A j (Pi.single i 1))

theorem Matrix.adjugate_transpose {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : Matrix.transpose (Matrix.adjugate A) = Matrix.adjugate (Matrix.transpose A)

@[simp]

theorem Matrix.adjugate_submatrix_equiv_self {m : Type u} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (e : n ≃ m) (A : Matrix m m α) : Matrix.adjugate (Matrix.submatrix A ⇑e ⇑e) = Matrix.submatrix (Matrix.adjugate A) ⇑e ⇑e

theorem Matrix.adjugate_reindex {m : Type u} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (e : m ≃ n) (A : Matrix m m α) : Matrix.adjugate ((Matrix.reindex e e) A) = (Matrix.reindex e e) (Matrix.adjugate A)

theorem Matrix.cramer_eq_adjugate_mulVec {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) : (Matrix.cramer A) b = Matrix.mulVec (Matrix.adjugate A) 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} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) (j : n) (k : n) : A i k * Matrix.adjugate A k j = (Matrix.cramer (Matrix.transpose A)) (Pi.single k (A i k)) j

theorem Matrix.mul_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : A * Matrix.adjugate A = Matrix.det A • 1

theorem Matrix.adjugate_mul {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : Matrix.adjugate A * A = Matrix.det A • 1

theorem Matrix.adjugate_smul {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (r : α) (A : Matrix n n α) : Matrix.adjugate (r • A) = r ^ (Fintype.card n - 1) • Matrix.adjugate A

@[simp]

theorem Matrix.mulVec_cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : n → α) : Matrix.mulVec A ((Matrix.cramer A) b) = Matrix.det A • 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} [DecidableEq n] [Fintype n] [CommRing α] [Subsingleton n] (A : Matrix n n α) : Matrix.adjugate A = 1

theorem Matrix.adjugate_eq_one_of_card_eq_one {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] {A : Matrix n n α} (h : Fintype.card n = 1) : Matrix.adjugate A = 1

@[simp]

theorem Matrix.adjugate_zero {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [Nontrivial n] : Matrix.adjugate 0 = 0

@[simp]

theorem Matrix.adjugate_one {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] : Matrix.adjugate 1 = 1

@[simp]

theorem Matrix.adjugate_diagonal {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (v : n → α) : Matrix.adjugate (Matrix.diagonal v) = Matrix.diagonal fun (i : n) => Finset.prod (Finset.erase Finset.univ i) fun (j : n) => v j

theorem RingHom.map_adjugate {n : Type v} [DecidableEq n] [Fintype n] {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (M : Matrix n n R) : (RingHom.mapMatrix f) (Matrix.adjugate M) = Matrix.adjugate ((RingHom.mapMatrix f) M)

theorem AlgHom.map_adjugate {n : Type v} [DecidableEq n] [Fintype n] {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (M : Matrix n n A) : (AlgHom.mapMatrix f) (Matrix.adjugate M) = Matrix.adjugate ((AlgHom.mapMatrix f) M)

theorem Matrix.det_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : Matrix.det (Matrix.adjugate A) = Matrix.det A ^ (Fintype.card n - 1)

@[simp]

theorem Matrix.adjugate_fin_zero {α : Type w} [CommRing α] (A : Matrix (Fin 0) (Fin 0) α) : Matrix.adjugate A = 0

@[simp]

theorem Matrix.adjugate_fin_one {α : Type w} [CommRing α] (A : Matrix (Fin 1) (Fin 1) α) : Matrix.adjugate A = 1

theorem Matrix.adjugate_fin_two {α : Type w} [CommRing α] (A : Matrix (Fin 2) (Fin 2) α) : Matrix.adjugate A = Matrix.of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]]

@[simp]

theorem Matrix.adjugate_fin_two_of {α : Type w} [CommRing α] (a : α) (b : α) (c : α) (d : α) : Matrix.adjugate (Matrix.of ![![a, b], ![c, d]]) = Matrix.of ![![d, -b], ![-c, a]]

theorem Matrix.adjugate_fin_succ_eq_det_submatrix {α : Type w} [CommRing α] {n : ℕ} (A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α) (i : Fin (Nat.succ n)) (j : Fin (Nat.succ n)) : Matrix.adjugate A i j = (-1) ^ (↑j + ↑i) * Matrix.det (Matrix.submatrix A (Fin.succAbove j) (Fin.succAbove i))

theorem Matrix.det_eq_sum_mul_adjugate_row {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) : Matrix.det A = Finset.sum Finset.univ fun (j : n) => A i j * Matrix.adjugate A j i

theorem Matrix.det_eq_sum_mul_adjugate_col {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (j : n) : Matrix.det A = Finset.sum Finset.univ fun (i : n) => A i j * Matrix.adjugate A j i

theorem Matrix.adjugate_conjTranspose {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [StarRing α] (A : Matrix n n α) : Matrix.conjTranspose (Matrix.adjugate A) = Matrix.adjugate (Matrix.conjTranspose A)

theorem Matrix.isRegular_of_isLeftRegular_det {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] {A : Matrix n n α} (hA : IsLeftRegular (Matrix.det A)) : IsRegular A

theorem Matrix.adjugate_mul_distrib_aux {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) (hA : IsLeftRegular (Matrix.det A)) (hB : IsLeftRegular (Matrix.det B)) : Matrix.adjugate (A * B) = Matrix.adjugate B * Matrix.adjugate A

theorem Matrix.adjugate_mul_distrib {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) : Matrix.adjugate (A * B) = Matrix.adjugate B * Matrix.adjugate A

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

@[simp]

theorem Matrix.adjugate_pow {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (k : ℕ) : Matrix.adjugate (A ^ k) = Matrix.adjugate A ^ k

theorem Matrix.det_smul_adjugate_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : Matrix.det A • Matrix.adjugate (Matrix.adjugate A) = Matrix.det A ^ (Fintype.card n - 1) • A

theorem Matrix.adjugate_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (h : Fintype.card n ≠ 1) : Matrix.adjugate (Matrix.adjugate A) = Matrix.det A ^ (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} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) [Nontrivial n] : Matrix.adjugate (Matrix.adjugate A) = Matrix.det A ^ (Fintype.card n - 2) • A

A weaker version of Matrix.adjugate_adjugate that uses Nontrivial.