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.charpolyis 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 $t I - M$.
The determinant of this matrix is the characteristic polynomial.
Equations
- M.charmatrix = (Matrix.scalar n) Polynomial.X - Polynomial.C.mapMatrix M
Instances For
theorem
Matrix.charmatrix_apply
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
(i j : n)
:
M.charmatrix 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)
:
theorem
Matrix.matPolyEquiv_charmatrix
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
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.reindex e e) M).charmatrix = (Matrix.reindex e e) M.charmatrix
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)
:
(M.map ⇑f).charmatrix = M.charmatrix.map (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.fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix = Matrix.fromBlocks M₁₁.charmatrix (-M₁₂.map ⇑Polynomial.C) (-M₂₁.map ⇑Polynomial.C) M₂₂.charmatrix
theorem
Matrix.BlockTriangular.of_charmatrix
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
{α : Type u_5}
[Preorder α]
{M : Matrix n n R}
{b : n → α}
:
M.charmatrix.BlockTriangular b → M.BlockTriangular b
Alias of the forward direction of Matrix.charmatrix_blockTriangular_iff.
theorem
Matrix.BlockTriangular.charmatrix
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
{α : Type u_5}
[Preorder α]
{M : Matrix n n R}
{b : n → α}
:
M.BlockTriangular b → M.charmatrix.BlockTriangular b
Alias of the reverse direction of Matrix.charmatrix_blockTriangular_iff.
def
Matrix.charpoly
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
The characteristic polynomial of a matrix M is given by $\det (t I - M)$.
Equations
- M.charpoly = M.charmatrix.det
Instances For
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.reindex e e) M).charpoly = M.charpoly
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)
:
(M.map ⇑f).charpoly = Polynomial.map f M.charpoly
@[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.fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
@[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.fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
theorem
Matrix.charmatrix_toSquareBlock
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
{α : Type u_5}
[DecidableEq α]
{b : n → α}
{a : α}
:
(M.toSquareBlock b a).charmatrix = M.charmatrix.toSquareBlock b a
theorem
Matrix.BlockTriangular.charpoly
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
{α : Type u_5}
{b : n → α}
[LinearOrder α]
(h : M.BlockTriangular b)
:
M.charpoly = ∏ a ∈ Finset.image b Finset.univ, (M.toSquareBlock b a).charpoly
theorem
Matrix.charpoly_of_upperTriangular
{R : Type u_1}
[CommRing R]
{n : Type u_4}
[DecidableEq n]
[Fintype n]
[LinearOrder n]
(M : Matrix n n R)
(h : M.BlockTriangular id)
:
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) 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 LinearMap.aeval_self_charpoly for the equivalent statement about endomorphisms.