Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

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 #

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) :

The "characteristic matrix" of M : Matrix n n R is the matrix of polynomials tIM. The determinant of this matrix is the characteristic polynomial.

Equations
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 = 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) :
@[simp]
theorem Matrix.charmatrix_apply_ne {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (i j : n) (h : i j) :
M.charmatrix i j = -Polynomial.C (M i j)
@[simp]
@[simp]
theorem Matrix.charmatrix_diagonal {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (d : nR) :
@[simp]
theorem Matrix.charmatrix_one {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] :
charmatrix 1 = diagonal fun (x : n) => Polynomial.X - 1
@[simp]
theorem Matrix.charmatrix_natCast {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (k : ) :
(↑k).charmatrix = diagonal fun (x : n) => Polynomial.X - k
@[simp]
theorem Matrix.charmatrix_ofNat {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (k : ) [k.AtLeastTwo] :
@[simp]
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) :
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) :
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) :
(fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix = fromBlocks M₁₁.charmatrix (-M₁₂.map Polynomial.C) (-M₂₁.map Polynomial.C) M₂₂.charmatrix
@[simp]
theorem Matrix.charmatrix_blockTriangular_iff {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α} :
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α} :

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α} :

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(tIM).

Equations
theorem Matrix.eval_charpoly {R : Type u_1} [CommRing R] {m : Type u_3} [DecidableEq m] [Fintype m] (M : Matrix m m R) (t : R) :
@[simp]
theorem Matrix.charpoly_diagonal {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (d : nR) :
(diagonal d).charpoly = i : n, (Polynomial.X - Polynomial.C (d i))
theorem Matrix.charpoly_natCast {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (k : ) :
@[simp]
theorem Matrix.charpoly_transpose {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
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) :
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) :
@[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) :
(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) :
(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 : α} :
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) :
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) :
M.charpoly = i : n, (Polynomial.X - Polynomial.C (M i i))
theorem Matrix.aeval_self_charpoly {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) :

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.