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.
theorem
charmatrix_apply_nat_degree
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
{M : matrix n n R}
[nontrivial R]
(i j : n) :
(charmatrix M i j).nat_degree = ite (i = j) 1 0
theorem
charmatrix_apply_nat_degree_le
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
{M : matrix n n R}
(i j : n) :
(charmatrix M i j).nat_degree ≤ ite (i = j) 1 0
theorem
matrix.charpoly_sub_diagonal_degree_lt
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq 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}
[comm_ring R]
{n : Type v}
[decidable_eq 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}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(h : fintype.card n = 0)
(M : matrix n n R) :
theorem
matrix.charpoly_degree_eq_dim
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
[nontrivial R]
(M : matrix n n R) :
M.charpoly.degree = ↑(fintype.card n)
theorem
matrix.charpoly_nat_degree_eq_dim
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
[nontrivial R]
(M : matrix n n R) :
theorem
matrix.charpoly_monic
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
theorem
matrix.trace_eq_neg_charpoly_coeff
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
[nonempty n]
(M : matrix n n R) :
⇑(matrix.trace n R R) M = -M.charpoly.coeff (fintype.card n - 1)
theorem
matrix.mat_poly_equiv_eval
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R[X])
(r : R)
(i j : n) :
polynomial.eval (⇑(matrix.scalar n) r) (⇑mat_poly_equiv M) i j = polynomial.eval r (M i j)
theorem
matrix.eval_det
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R[X])
(r : R) :
polynomial.eval r M.det = (polynomial.eval (⇑(matrix.scalar n) r) (⇑mat_poly_equiv M)).det
theorem
matrix.det_eq_sign_charpoly_coeff
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
theorem
mat_poly_equiv_eq_X_pow_sub_C
{n : Type v}
[decidable_eq n]
[fintype n]
{K : Type u_1}
(k : ℕ)
[field K]
(M : matrix n n K) :
⇑mat_poly_equiv (⇑(↑(polynomial.expand K k).map_matrix) (charmatrix (M ^ k))) = polynomial.X ^ k - ⇑polynomial.C (M ^ k)
@[simp]
theorem
finite_field.matrix.charpoly_pow_card
{n : Type v}
[decidable_eq n]
[fintype n]
{K : Type u_1}
[field K]
[fintype K]
(M : matrix n n K) :
(M ^ fintype.card K).charpoly = M.charpoly
theorem
finite_field.trace_pow_card
{n : Type v}
[decidable_eq n]
[fintype n]
{K : Type u_1}
[field K]
[fintype K]
(M : matrix n n K) :
⇑(matrix.trace n K K) (M ^ fintype.card K) = ⇑(matrix.trace n K K) M ^ fintype.card K
theorem
zmod.trace_pow_card
{n : Type v}
[decidable_eq n]
[fintype n]
{p : ℕ}
[fact (nat.prime p)]
(M : matrix n n (zmod p)) :
theorem
matrix.is_integral
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
{M : matrix n n R} :
is_integral R M
theorem
matrix.minpoly_dvd_charpoly
{n : Type v}
[decidable_eq n]
[fintype n]
{K : Type u_1}
[field K]
(M : matrix n n K) :
theorem
matrix.aeval_eq_aeval_mod_charpoly
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R)
(p : R[X]) :
⇑(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}
[comm_ring R]
{n : Type v}
[decidable_eq 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
charpoly_left_mul_matrix
{K : Type u_1}
{S : Type u_2}
[field K]
[comm_ring S]
[algebra K S]
(h : power_basis K S) :
The characteristic polynomial of the map λ x, a * x is the minimal polynomial of a.
In combination with det_eq_sign_charpoly_coeff or trace_eq_neg_charpoly_coeff
and a bit of rewriting, this will allow us to conclude the
field norm resp. trace of x is the product resp. sum of x's conjugates.