Determinants of polynomials in a matrix as resultants

For a square matrix A of size n over a commutative ring and a polynomial f of degree at most m, the determinant of f(A) is the resultant of the characteristic polynomial χ_A and f:

det f(A) = Res(χ_A, f), read with the degree bounds n and m (Matrix.det_aeval_eq_resultant).

If χ_A = ∏ (X - αᵢ) this is ∏ f(αᵢ), the determinant form of the spectral mapping theorem. Applied over R[T] to T - f it identifies the characteristic polynomial of f(A) (Matrix.charpoly_aeval_eq_resultant): χ_{f(A)}(T) = Res_X(χ_A(X), T - f(X)). In particular χ_{f(A)} depends on A only through χ_A. These identities hold over every commutative ring, including rings with zero divisors, where no factorisation of χ_A is available.

Main results

• Matrix.det_aeval_eq_resultant: det f(A) = Res(χ_A, f).
• Matrix.charmatrix_aeval: the characteristic matrix of f(A) is T - f evaluated at A.
• Matrix.charpoly_aeval_eq_resultant: χ_{f(A)}(T) = Res_X(χ_A(X), T - f(X)).

theorem Matrix.det_aeval_eq_resultant {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] (A : Matrix ι ι R) (f : Polynomial R) {m : ℕ} (hm : f.natDegree ≤ m) : ((Polynomial.aeval A) f).det = A.charpoly.resultant f (Fintype.card ι) m

Determinants of polynomials in a matrix are resultants. For a square matrix A of size n and a polynomial f of degree at most m, det f(A) = Res(χ_A, f), the resultant of the characteristic polynomial of A and f with degree bounds n and m. If χ_A = ∏ (X - αᵢ), the right-hand side is ∏ f(αᵢ).

theorem Matrix.charmatrix_aeval {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] (A : Matrix ι ι R) (f : Polynomial R) : ((Polynomial.aeval A) f).charmatrix = (Polynomial.aeval (A.map ⇑Polynomial.C)) (Polynomial.C Polynomial.X - Polynomial.map Polynomial.C f)

The characteristic matrix of f(A) is T - f evaluated at A, read over R[T].

theorem Matrix.charpoly_aeval_eq_resultant {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] (A : Matrix ι ι R) (f : Polynomial R) {m : ℕ} (hm : f.natDegree ≤ m) : ((Polynomial.aeval A) f).charpoly = (Polynomial.map Polynomial.C A.charpoly).resultant (Polynomial.C Polynomial.X - Polynomial.map Polynomial.C f) (Fintype.card ι) m

The characteristic polynomial of a polynomial in a matrix. For a square matrix A of size n and a polynomial f of degree at most m, χ_{f(A)}(T) = Res_X(χ_A(X), T - f(X)), the resultant over R[T] with degree bounds n and m. In particular χ_{f(A)} depends on A only through χ_A.