Characteristic polynomials and the Cayley-Hamilton theorem
We define characteristic polynomials of matrices and prove the Cayley–Hamilton theorem over arbitrary commutative rings.
Main definitions
char_polyis the characteristic polynomial of a matrix.
Implementation details
We follow a nice proof from http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf
def
char_matrix
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n] :
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
- char_matrix M = ⇑(matrix.scalar n) polynomial.X - ⇑(polynomial.C.map_matrix) M
@[simp]
theorem
char_matrix_apply_eq
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(M : matrix n n R)
(i : n) :
char_matrix M i i = polynomial.X - ⇑polynomial.C (M i i)
@[simp]
theorem
char_matrix_apply_ne
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(M : matrix n n R)
(i j : n) :
i ≠ j → char_matrix M i j = -⇑polynomial.C (M i j)
theorem
mat_poly_equiv_char_matrix
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
def
char_poly
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n] :
matrix n n R → polynomial R
The characteristic polynomial of a matrix M is given by $\det (t I - M)$.
Equations
- char_poly M = (char_matrix M).det
theorem
char_poly_map_eval_self
{R : Type u}
[comm_ring R]
{n : Type w}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
polynomial.eval M (polynomial.map (algebra_map R (matrix n n R)) (char_poly 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.