Characteristic polynomials

We give methods for computing coefficients of the characteristic polynomial.

Main definitions

• Matrix.charpoly_degree_eq_dim proves that the degree of the characteristic polynomial over a nonzero ring is the dimension of the matrix
• Matrix.det_eq_sign_charpoly_coeff proves that the determinant is the constant term of the characteristic polynomial, up to sign.
• Matrix.trace_eq_neg_charpoly_coeff proves 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.coeff_det_one_add_X_smul_eq_sum_minors proves that the k-th coefficient of det (1 + X • M) equals the sum of all k×k principal minors of M.
• Matrix.charpoly_coeff_eq_sum_minors expresses the coefficients of the characteristic polynomial as signed sums of principal minors.
• Matrix.charpolyRev the reverse of the characteristic polynomial.
• Matrix.reverse_charpoly characterises 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 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 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

@[simp]

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.trace_eq_neg_charpoly_nextCoeff {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : M.trace = -M.charpoly.nextCoeff

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.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 Matrix.charpoly_of_card_eq_two {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) [Nontrivial R] (hn : Fintype.card n = 2) : M.charpoly = Polynomial.X ^ 2 - Polynomial.C M.trace * Polynomial.X + Polynomial.C M.det

theorem Matrix.charpoly_fin_two {R : Type u} [CommRing R] [Nontrivial R] (M : Matrix (Fin 2) (Fin 2) R) : M.charpoly = Polynomial.X ^ 2 - Polynomial.C M.trace * Polynomial.X + Polynomial.C M.det

theorem matPolyEquiv_eq_X_pow_sub_C {n : Type v} [DecidableEq n] [Fintype n] {K : Type u_1} (k : ℕ) [CommRing 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)

noncomputable def Matrix.charpolyRev {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : Polynomial 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

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

theorem Matrix.charpoly_inv {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (A : Matrix n n R) (h : IsUnit A) : A⁻¹.charpoly = (-1) ^ Fintype.card n * Polynomial.C (Ring.inverse A.det) * A.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)

theorem Matrix.det_piecewise_one_eq_submatrix_det {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) (s : Finset n) : (of (s.piecewise M.row (row 1))).det = (M.submatrix Subtype.val Subtype.val).det

The determinant of the matrix obtained by replacing rows outside s with identity rows equals the determinant of the principal submatrix indexed by s.

theorem Matrix.coeff_det_one_add_X_smul_eq_sum_minors {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) (k : ℕ) : (1 + Polynomial.X • M.map ⇑Polynomial.C).det.coeff k = ∑ s ∈ Finset.powersetCard k Finset.univ, (M.submatrix Subtype.val Subtype.val).det

The k-th coefficient of det (1 + X • M) equals the sum of all k×k principal minors of M. This generalizes coeff_det_one_add_X_smul_one (the k = 1 case, which gives the trace) and det_eq_sign_charpoly_coeff (the k = n case, which gives the determinant).

theorem Matrix.charpoly_coeff_eq_sum_minors {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) (k : ℕ) (hk : k ≤ Fintype.card n) : M.charpoly.coeff (Fintype.card n - k) = (-1) ^ k * ∑ s ∈ Finset.powersetCard k Finset.univ, (M.submatrix Subtype.val Subtype.val).det

The coefficients of the characteristic polynomial are signed sums of principal minors. Specifically, the (n-k)-th coefficient of the characteristic polynomial of M equals (-1)^k times the sum of all k×k principal minors of M.