Characteristic polynomials and the Cayley-Hamilton theorem #

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

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

See the file matrix/charpoly/coeff 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

source

noncomputable def charmatrix {R : Type u} [comm_ring R] {n : Type w} [decidable_eq 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 $t I - M$. The determinant of this matrix is the characteristic polynomial.

Equations

charmatrix M = ⇑(matrix.scalar n) polynomial.X - ⇑(polynomial.C.map_matrix) M

source

theorem charmatrix_apply {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : matrix n n R) (i j : n) :

charmatrix M i j = polynomial.X * 1 i j - ⇑polynomial.C (M i j)

source

@[simp]

theorem charmatrix_apply_eq {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : matrix n n R) (i : n) :

charmatrix M i i = polynomial.X - ⇑polynomial.C (M i i)

source

@[simp]

theorem charmatrix_apply_ne {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : matrix n n R) (i j : n) (h : i ≠ j) :

charmatrix M i j = -⇑polynomial.C (M i j)

source

theorem mat_poly_equiv_charmatrix {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : matrix n n R) :

⇑mat_poly_equiv (charmatrix M) = polynomial.X - ⇑polynomial.C M

source

theorem charmatrix_reindex {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] {m : Type v} [decidable_eq m] [fintype m] (e : n ≃ m) (M : matrix n n R) :

charmatrix (⇑(matrix.reindex e e) M) = ⇑(matrix.reindex e e) (charmatrix M)

source

noncomputable def matrix.charpoly {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : matrix n n R) :

polynomial R

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

Equations

M.charpoly = (charmatrix M).det

source

theorem matrix.charpoly_reindex {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] {m : Type v} [decidable_eq m] [fintype m] (e : n ≃ m) (M : matrix n n R) :

(⇑(matrix.reindex e e) M).charpoly = M.charpoly

source

theorem matrix.aeval_self_charpoly {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : matrix n n R) :

⇑(polynomial.aeval M) M.charpoly = 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 linear_map.aeval_self_charpoly for the equivalent statement about endomorphisms.