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

source

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

Equations

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

Instances For

source

theorem charmatrix_apply {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) (i : n) (j : n) :

charmatrix M i j = Polynomial.X * OfNat.ofNat 1 i j - ↑Polynomial.C (M i j)

source

@[simp]

theorem charmatrix_apply_eq {R : Type u} [CommRing R] {n : Type w} [DecidableEq 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} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) (i : n) (j : n) (h : i ≠ j) :

charmatrix M i j = -↑Polynomial.C (M i j)

source

theorem matPolyEquiv_charmatrix {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) :

↑matPolyEquiv (charmatrix M) = Polynomial.X - ↑Polynomial.C M

source

theorem charmatrix_reindex {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type v} [DecidableEq m] [Fintype m] (e : n ≃ m) (M : Matrix n n R) :

charmatrix (↑(Matrix.reindex e e) M) = ↑(Matrix.reindex e e) (charmatrix M)

source

def Matrix.charpoly {R : Type u} [CommRing R] {n : Type w} [DecidableEq 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

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

Instances For

source

theorem Matrix.charpoly_reindex {R : Type u} [CommRing R] {n : Type w} [DecidableEq n] [Fintype n] {m : Type v} [DecidableEq m] [Fintype m] (e : n ≃ m) (M : Matrix n n R) :

Matrix.charpoly (↑(Matrix.reindex e e) M) = Matrix.charpoly M

source

theorem Matrix.aeval_self_charpoly {R : Type u} [CommRing R] {n : Type w} [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.