Characteristic polynomials and the Cayley-Hamilton theorem

We define characteristic polynomials of matrices and prove the Cayley–Hamilton theorem over arbitrary commutative rings.

See the file Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean for corollaries of this theorem.

Main definitions

• Matrix.charpoly is the characteristic polynomial of a matrix.

Implementation details

We follow a nice proof from http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf

def Matrix.charmatrix {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) : Matrix n n (Polynomial R)

The "characteristic matrix" of M : Matrix n n R is the matrix of polynomials $tI-M$. The determinant of this matrix is the characteristic polynomial.

Equations

• Matrix.charmatrix M = (Matrix.scalar n) Polynomial.X - (RingHom.mapMatrix Polynomial.C) M

theorem Matrix.charmatrix_apply {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (i : n) (j : n) : Matrix.charmatrix M i j = Matrix.diagonal (fun (x : n) => Polynomial.X) i j - Polynomial.C (M i j)

@[simp]

theorem Matrix.charmatrix_apply_eq {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (i : n) : Matrix.charmatrix M i i = Polynomial.X - Polynomial.C (M i i)

@[simp]

theorem Matrix.charmatrix_apply_ne {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (i : n) (j : n) (h : i ≠ j) : Matrix.charmatrix M i j = -Polynomial.C (M i j)

theorem Matrix.matPolyEquiv_charmatrix {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) : matPolyEquiv (Matrix.charmatrix M) = Polynomial.X - Polynomial.C M

theorem Matrix.charmatrix_reindex {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (M : Matrix n n R) (e : n ≃ m) : Matrix.charmatrix ((Matrix.reindex e e) M) = (Matrix.reindex e e) (Matrix.charmatrix M)

theorem Matrix.charmatrix_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (f : R →+* S) : Matrix.charmatrix (Matrix.map M ⇑f) = Matrix.map (Matrix.charmatrix M) (Polynomial.map f)

theorem Matrix.charmatrix_fromBlocks {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₁ : Matrix n m R) (M₂₂ : Matrix n n R) : Matrix.charmatrix (Matrix.fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) = Matrix.fromBlocks (Matrix.charmatrix M₁₁) (-Matrix.map M₁₂ ⇑Polynomial.C) (-Matrix.map M₂₁ ⇑Polynomial.C) (Matrix.charmatrix M₂₂)

def Matrix.charpoly {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) : Polynomial R

The characteristic polynomial of a matrix M is given by $det(tI-M)$.

Equations

• Matrix.charpoly M = Matrix.det (Matrix.charmatrix M)

theorem Matrix.charpoly_reindex {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (e : n ≃ m) (M : Matrix n n R) : Matrix.charpoly ((Matrix.reindex e e) M) = Matrix.charpoly M

theorem Matrix.charpoly_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (f : R →+* S) : Matrix.charpoly (Matrix.map M ⇑f) = Polynomial.map f (Matrix.charpoly M)

@[simp]

theorem Matrix.charpoly_fromBlocks_zero₁₂ {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (M₁₁ : Matrix m m R) (M₂₁ : Matrix n m R) (M₂₂ : Matrix n n R) : Matrix.charpoly (Matrix.fromBlocks M₁₁ 0 M₂₁ M₂₂) = Matrix.charpoly M₁₁ * Matrix.charpoly M₂₂

@[simp]

theorem Matrix.charpoly_fromBlocks_zero₂₁ {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₂ : Matrix n n R) : Matrix.charpoly (Matrix.fromBlocks M₁₁ M₁₂ 0 M₂₂) = Matrix.charpoly M₁₁ * Matrix.charpoly M₂₂

theorem Matrix.aeval_self_charpoly {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) : (Polynomial.aeval M) (Matrix.charpoly M) = 0

The Cayley-Hamilton Theorem, that the characteristic polynomial of a matrix, applied to the matrix itself, is zero.

This holds over any commutative ring.

See LinearMap.aeval_self_charpoly for the equivalent statement about endomorphisms.