Characteristic roots of matrices

Over any field, if p(A) is invertible then p does not vanish at any characteristic root of A.

Over an algebraically closed field, the characteristic polynomial of a square matrix of positive size has a root. This file records that fact as a Nonempty instance on the root multiset, so that families indexed by the characteristic roots, counted with algebraic multiplicity, have a nonempty index type.

It also records the determinant form of the spectral mapping theorem: for a polynomial p, the determinant of p(A) is the product of p(λ) over the characteristic roots λ of A, counted with algebraic multiplicity. Mathlib's Matrix.det_eq_prod_roots_charpoly is the case p = X.

More generally, over an integral domain, when the characteristic polynomial of A splits, the characteristic roots of p(A) are the values p(λ) at the characteristic roots λ of A, counted with algebraic multiplicity. So the determinant of p(A) is the product of the p(λ) and its trace is their sum; Mathlib's Matrix.det_eq_prod_roots_charpoly_of_splits and Matrix.trace_eq_sum_roots_charpoly_of_splits are the case p = X. These are proved by evaluating the resultant formulas Matrix.det_aeval_eq_resultant and Matrix.charpoly_aeval_eq_resultant over the split characteristic polynomial. In particular det (1 - X A), the reverse of χ_A = ∏ (X - λ), factors as ∏ (1 - λ X).

Main results

• Matrix.eval_ne_zero_of_det_aeval_ne_zero: if det (p(A)) ≠ 0, then p(λ) ≠ 0 for every characteristic root λ of A.
• Matrix.nonempty_roots_charpoly — a square matrix of positive size over an algebraically closed field has a characteristic root.
• Matrix.charpoly_roots_filter_ne_zero_mul_eq — the nonzero characteristic roots of rectangular products A * B and B * A agree, counted with multiplicity.
• Matrix.det_aeval_eq_prod_roots_charpoly: det (p(A)) = ∏ p(λ) over the characteristic roots λ of A.
• Matrix.det_aeval_eq_prod_roots_charpoly_of_splits: the same when the characteristic polynomial of A splits.
• Matrix.charpoly_aeval_eq_prod_roots_charpoly_of_splits: the characteristic polynomial of p(A) is ∏ (X - p(λ)).
• Matrix.trace_aeval_eq_sum_roots_charpoly_of_splits: tr (p(A)) = ∑ p(λ); for p = X ^ k the trace of A ^ k is the k-th power sum of the characteristic roots.
• Matrix.charpolyRev_eq_prod_roots_charpoly_of_splits: det (1 - X A) = ∏ (1 - λ X).
• Matrix.coeff_charpolyRev_eq_esymm_roots_charpoly_of_splits: Vieta's formula for det (1 - X A), whose r-th coefficient is (-1) ^ r times the r-th elementary symmetric function of the characteristic roots.

theorem Matrix.charpoly_roots_filter_ne_zero_mul_eq {m : Type u_1} {n : Type u_2} {K : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [CommRing K] [IsDomain K] (A : Matrix m n K) (B : Matrix n m K) : Multiset.filter (fun (z : K) => z ≠ 0) (A * B).charpoly.roots = Multiset.filter (fun (z : K) => z ≠ 0) (B * A).charpoly.roots

Rectangular products A * B and B * A have the same nonzero characteristic roots, counted with algebraic multiplicity.

theorem Matrix.eval_ne_zero_of_det_aeval_ne_zero {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] (A : Matrix n n K) (p : Polynomial K) (h : ((Polynomial.aeval A) p).det ≠ 0) {x : K} (hx : x ∈ A.charpoly.roots) : Polynomial.eval x p ≠ 0

If det (p(A)) ≠ 0 for a square matrix A over a field, then p does not vanish at any characteristic root of A: by spectral mapping, p(λ) is in the spectrum of p(A).

theorem Matrix.det_aeval_eq_prod_roots_charpoly_of_splits {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] [IsDomain K] {A : Matrix n n K} (hA : A.charpoly.Splits) (p : Polynomial K) : ((Polynomial.aeval A) p).det = (Multiset.map (fun (x : K) => Polynomial.eval x p) A.charpoly.roots).prod

Spectral mapping for determinants. If the characteristic polynomial of A splits, the determinant of p(A) is the product of p(λ) over the characteristic roots λ of A, counted with algebraic multiplicity.

theorem Matrix.charpoly_aeval_eq_prod_roots_charpoly_of_splits {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] [IsDomain K] {A : Matrix n n K} (hA : A.charpoly.Splits) (p : Polynomial K) : ((Polynomial.aeval A) p).charpoly = (Multiset.map (fun (μ : K) => Polynomial.X - Polynomial.C (Polynomial.eval μ p)) A.charpoly.roots).prod

Spectral mapping for characteristic polynomials. If the characteristic polynomial of A splits, the characteristic polynomial of p(A) is ∏ (X - p(λ)) over the characteristic roots λ of A, counted with algebraic multiplicity.

theorem Matrix.trace_aeval_eq_sum_roots_charpoly_of_splits {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] [IsDomain K] {A : Matrix n n K} (hA : A.charpoly.Splits) (p : Polynomial K) : ((Polynomial.aeval A) p).trace = (Multiset.map (fun (x : K) => Polynomial.eval x p) A.charpoly.roots).sum

Spectral mapping for traces. If the characteristic polynomial of A splits, the trace of p(A) is the sum of p(λ) over the characteristic roots λ of A, counted with algebraic multiplicity.

theorem Matrix.charpolyRev_eq_prod_roots_charpoly_of_splits {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] [IsDomain K] {A : Matrix n n K} (hA : A.charpoly.Splits) : A.charpolyRev = (Multiset.map (fun (μ : K) => 1 - Polynomial.C μ * Polynomial.X) A.charpoly.roots).prod

If the characteristic polynomial of A splits, det (1 - X A) is the product of the linear factors 1 - λ X over the characteristic roots λ of A, counted with algebraic multiplicity.

theorem Matrix.coeff_charpolyRev_eq_esymm_roots_charpoly_of_splits {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] [IsDomain K] {A : Matrix n n K} (hA : A.charpoly.Splits) (r : ℕ) : A.charpolyRev.coeff r = (-1) ^ r * A.charpoly.roots.esymm r

Vieta's formula for det (1 - X A). If the characteristic polynomial of A splits, the r-th coefficient of det (1 - X A) is (-1) ^ r times the r-th elementary symmetric function of the characteristic roots of A, counted with algebraic multiplicity.

instance Matrix.nonempty_roots_charpoly {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] [Field K] [IsAlgClosed K] [DecidableEq K] (A : Matrix n n K) : Nonempty A.charpoly.roots.ToType

A square matrix of positive size over an algebraically closed field has a characteristic root.

theorem Matrix.det_aeval_eq_prod_roots_charpoly {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] [IsAlgClosed K] (A : Matrix n n K) (p : Polynomial K) : ((Polynomial.aeval A) p).det = (Multiset.map (fun (x : K) => Polynomial.eval x p) A.charpoly.roots).prod

Spectral mapping for determinants. Over an algebraically closed field, the determinant of p(A) is the product of p(λ) over the characteristic roots λ of A, counted with algebraic multiplicity.