Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Characteristic polynomials #

We give methods for computing coefficients of the characteristic polynomial.

Main definitions #

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) :
(M.charmatrix i j).natDegree = 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) :
(M.charmatrix i j).natDegree 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) :
(M.charpoly - i : n, (Polynomial.X - Polynomial.C (M i i))).degree < (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) :
M.charpoly.coeff k = (i : n, (Polynomial.X - Polynomial.C (M i i))).coeff 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) :
M.det = 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) :
M.charpoly.degree = (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) :
M.charpoly.natDegree = Fintype.card n
theorem Matrix.charpoly_monic {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
M.charpoly.Monic
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) :
M.trace = -M.charpoly.coeff (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) :
(matPolyEquiv.symm M).map (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) = M.map (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 M.det = (Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M)).det
theorem Matrix.det_eq_sign_charpoly_coeff {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 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 (A + Polynomial.X M.map Polynomial.C).det = Polynomial.eval 0 A.det
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 (1 + Polynomial.X M.map Polynomial.C).det) = M.trace
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 (1 + Polynomial.X M.map Polynomial.C).det) = M.trace

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) :
(1 + Polynomial.X M.map Polynomial.C).det.coeff 1 = M.trace
theorem Matrix.det_one_add_X_smul {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
(1 + Polynomial.X M.map Polynomial.C).det = 1 + M.trace Polynomial.X + (1 + Polynomial.X M.map Polynomial.C).det.divX.divX * 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) :
(1 + r M).det = 1 + M.trace * r + Polynomial.eval r (1 + Polynomial.X M.map Polynomial.C).det.divX.divX * 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 (((Polynomial.expand K k)).mapMatrix (M ^ k).charmatrix) = 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 %ₘ M.charpoly)

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 %ₘ M.charpoly)

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 : ) :
M.charpoly.coeff 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
  • M.charpolyRev = (1 - Polynomial.X M.map Polynomial.C).det
Instances For
    theorem Matrix.reverse_charpoly {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
    M.charpoly.reverse = M.charpolyRev
    @[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 M.charpolyRev = 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) :
    M.charpolyRev.coeff 1 = -M.trace
    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) :
    IsUnit M.charpolyRev
    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) :
    IsNilpotent M.trace
    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 (M.charpoly - Polynomial.X ^ Fintype.card n)