Characteristic polynomials #
We give methods for computing coefficients of the characteristic polynomial.
Main definitions #
Matrix.charpoly_degree_eq_dimproves that the degree of the characteristic polynomial over a nonzero ring is the dimension of the matrixMatrix.det_eq_sign_charpoly_coeffproves that the determinant is the constant term of the characteristic polynomial, up to sign.Matrix.trace_eq_neg_charpoly_coeffproves that the trace is the negative of the (d-1)th coefficient of the characteristic polynomial, where d is the dimension of the matrix. For a nonzero ring, this is the second-highest coefficient.Matrix.charpolyRevthe reverse of the characteristic polynomial.Matrix.reverse_charpolycharacterises the reverse of the characteristic polynomial.
theorem
Matrix.charmatrix_apply_natDegree
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
{M : Matrix n n R}
[Nontrivial R]
(i : n)
(j : n)
:
Polynomial.natDegree (Matrix.charmatrix M i j) = if i = j then 1 else 0
theorem
Matrix.charmatrix_apply_natDegree_le
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
{M : Matrix n n R}
(i : n)
(j : n)
:
Polynomial.natDegree (Matrix.charmatrix M i j) ≤ if i = j then 1 else 0
theorem
Matrix.charpoly_sub_diagonal_degree_lt
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
Polynomial.degree (Matrix.charpoly M - Finset.prod Finset.univ fun (i : n) => Polynomial.X - Polynomial.C (M i i)) < ↑(Fintype.card n - 1)
theorem
Matrix.charpoly_coeff_eq_prod_coeff_of_le
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
{k : ℕ}
(h : Fintype.card n - 1 ≤ k)
:
Polynomial.coeff (Matrix.charpoly M) k = Polynomial.coeff (Finset.prod Finset.univ fun (i : n) => Polynomial.X - Polynomial.C (M i i)) k
theorem
Matrix.det_of_card_zero
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(h : Fintype.card n = 0)
(M : Matrix n n R)
:
Matrix.det M = 1
theorem
Matrix.charpoly_degree_eq_dim
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
[Nontrivial R]
(M : Matrix n n R)
:
Polynomial.degree (Matrix.charpoly M) = ↑(Fintype.card n)
@[simp]
theorem
Matrix.charpoly_natDegree_eq_dim
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
[Nontrivial R]
(M : Matrix n n R)
:
theorem
Matrix.charpoly_monic
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
theorem
Matrix.trace_eq_neg_charpoly_coeff
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
[Nonempty n]
(M : Matrix n n R)
:
Matrix.trace M = -Polynomial.coeff (Matrix.charpoly M) (Fintype.card n - 1)
See also Matrix.coeff_charpolyRev_eq_neg_trace.
theorem
Matrix.matPolyEquiv_symm_map_eval
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Polynomial (Matrix n n R))
(r : R)
:
Matrix.map ((AlgEquiv.symm matPolyEquiv) M) (Polynomial.eval r) = Polynomial.eval ((Matrix.scalar n) r) M
theorem
Matrix.matPolyEquiv_eval_eq_map
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n (Polynomial R))
(r : R)
:
Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) = Matrix.map M (Polynomial.eval r)
theorem
Matrix.matPolyEquiv_eval
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n (Polynomial R))
(r : R)
(i : n)
(j : n)
:
Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) i j = Polynomial.eval r (M i j)
theorem
Matrix.eval_det
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n (Polynomial R))
(r : R)
:
Polynomial.eval r (Matrix.det M) = Matrix.det (Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M))
theorem
Matrix.det_eq_sign_charpoly_coeff
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
Matrix.det M = (-1) ^ Fintype.card n * Polynomial.coeff (Matrix.charpoly M) 0
theorem
Matrix.eval_det_add_X_smul
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(A : Matrix n n (Polynomial R))
(M : Matrix n n R)
:
Polynomial.eval 0 (Matrix.det (A + Polynomial.X • Matrix.map M ⇑Polynomial.C)) = Polynomial.eval 0 (Matrix.det A)
theorem
Matrix.derivative_det_one_add_X_smul_aux
{R : Type u}
[CommRing R]
{n : ℕ}
(M : Matrix (Fin n) (Fin n) R)
:
Polynomial.eval 0 (Polynomial.derivative (Matrix.det (1 + Polynomial.X • Matrix.map M ⇑Polynomial.C))) = Matrix.trace M
theorem
Matrix.derivative_det_one_add_X_smul
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
Polynomial.eval 0 (Polynomial.derivative (Matrix.det (1 + Polynomial.X • Matrix.map M ⇑Polynomial.C))) = Matrix.trace M
The derivative of det (1 + M X) at 0 is the trace of M.
theorem
Matrix.coeff_det_one_add_X_smul_one
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
Polynomial.coeff (Matrix.det (1 + Polynomial.X • Matrix.map M ⇑Polynomial.C)) 1 = Matrix.trace M
theorem
Matrix.det_one_add_X_smul
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
Matrix.det (1 + Polynomial.X • Matrix.map M ⇑Polynomial.C) = 1 + Matrix.trace M • Polynomial.X + Polynomial.divX (Polynomial.divX (Matrix.det (1 + Polynomial.X • Matrix.map M ⇑Polynomial.C))) * Polynomial.X ^ 2
theorem
Matrix.det_one_add_smul
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(r : R)
(M : Matrix n n R)
:
Matrix.det (1 + r • M) = 1 + Matrix.trace M * r + Polynomial.eval r (Polynomial.divX (Polynomial.divX (Matrix.det (1 + Polynomial.X • Matrix.map M ⇑Polynomial.C)))) * r ^ 2
The first two terms of the taylor expansion of det (1 + r • M) at r = 0.
theorem
matPolyEquiv_eq_X_pow_sub_C
{n : Type v}
[DecidableEq n]
[Fintype n]
{K : Type u_1}
(k : ℕ)
[Field K]
(M : Matrix n n K)
:
matPolyEquiv ((RingHom.mapMatrix ↑(Polynomial.expand K k)) (Matrix.charmatrix (M ^ k))) = Polynomial.X ^ k - Polynomial.C (M ^ k)
theorem
Matrix.aeval_eq_aeval_mod_charpoly
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
(p : Polynomial R)
:
(Polynomial.aeval M) p = (Polynomial.aeval M) (p %ₘ Matrix.charpoly M)
Any matrix polynomial p is equivalent under evaluation to p %ₘ M.charpoly; that is, p
is equivalent to a polynomial with degree less than the dimension of the matrix.
theorem
Matrix.pow_eq_aeval_mod_charpoly
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
(k : ℕ)
:
M ^ k = (Polynomial.aeval M) (Polynomial.X ^ k %ₘ Matrix.charpoly M)
Any matrix power can be computed as the sum of matrix powers less than Fintype.card n.
TODO: add the statement for negative powers phrased with zpow.
theorem
Matrix.coeff_charpoly_mem_ideal_pow
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
{M : Matrix n n R}
{I : Ideal R}
(h : ∀ (i j : n), M i j ∈ I)
(k : ℕ)
:
Polynomial.coeff (Matrix.charpoly M) k ∈ I ^ (Fintype.card n - k)
def
Matrix.charpolyRev
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
The reverse of the characteristic polynomial of a matrix.
It has some advantages over the characteristic polynomial, including the fact that it can be extended to infinite dimensions (for appropriate operators). In such settings it is known as the "characteristic power series".
Equations
- Matrix.charpolyRev M = Matrix.det (1 - Polynomial.X • Matrix.map M ⇑Polynomial.C)
Instances For
theorem
Matrix.reverse_charpoly
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
@[simp]
theorem
Matrix.eval_charpolyRev
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
{M : Matrix n n R}
:
Polynomial.eval 0 (Matrix.charpolyRev M) = 1
@[simp]
theorem
Matrix.coeff_charpolyRev_eq_neg_trace
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
(M : Matrix n n R)
:
theorem
Matrix.isUnit_charpolyRev_of_isNilpotent
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
{M : Matrix n n R}
(hM : IsNilpotent M)
:
theorem
Matrix.isNilpotent_trace_of_isNilpotent
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
{M : Matrix n n R}
(hM : IsNilpotent M)
:
theorem
Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
{R : Type u}
[CommRing R]
{n : Type v}
[DecidableEq n]
[Fintype n]
{M : Matrix n n R}
(hM : IsNilpotent M)
:
IsNilpotent (Matrix.charpoly M - Polynomial.X ^ Fintype.card n)