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 matrix/charpoly/coeff for corollaries of this theorem.
Main definitions #
matrix.charpolyis the characteristic polynomial of a matrix.
Implementation details #
We follow a nice proof from http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf
noncomputable
def
charmatrix
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(M : matrix n n 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
@[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)
@[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)
theorem
mat_poly_equiv_charmatrix
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
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)
noncomputable
def
matrix.charpoly
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
R[X]
The characteristic polynomial of a matrix M is given by $\det (t I - M)$.
Equations
- M.charpoly = (charmatrix M).det
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
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.