Jacobi's formula and Newton's identity for traces of matrix powers

Let R be a commutative ring and M a square matrix over R.

The resolvent series Matrix.resolventSeries M is the matrix of formal power series whose (i, j) entry is ∑ₖ (Mᵏ) i j Xᵏ. It is the two-sided inverse of 1 - X • M in Matrix n n R⟦X⟧, and its trace is the generating function ∑ₖ trace (Mᵏ) Xᵏ.

Jacobi's formula expresses the derivative of the determinant of a matrix of polynomials as derivative (det A) = trace (adjugate A * A.map derivative).

Combining the two gives Newton's identity for traces: the logarithmic derivative of the reversed characteristic polynomial Matrix.charpolyRev M = det (1 - X • M) is minus the generating function of the traces of the powers of M. No eigenvalues and no assumption on R are needed.

Main definitions

• Matrix.resolventSeries M: the matrix ∑ₖ Mᵏ Xᵏ over R⟦X⟧.

Main results

• Matrix.one_sub_X_smul_mul_resolventSeries, Matrix.resolventSeries_mul_one_sub_X_smul, Matrix.resolventSeries_eq_inv: resolventSeries M = (1 - X • M)⁻¹.
• Matrix.trace_resolventSeries: trace (resolventSeries M) = ∑ₖ trace (Mᵏ) Xᵏ.
• Matrix.det_smul_resolventSeries: det (1 - X • M) • resolventSeries M = adjugate (1 - X • M).
• Matrix.derivative_det: Jacobi's formula.
• Matrix.coe_derivative_charpolyRev_eq_neg_mul_mk_trace_pow: Newton's identity (charpolyRev M)′ = - charpolyRev M * ∑ₖ trace (Mᵏ⁺¹) Xᵏ in R⟦X⟧. Its constant coefficient is Matrix.coeff_charpolyRev_eq_neg_trace. Matrix.derivative_coe_charpolyRev is the same identity with the derivative taken in R⟦X⟧.

The resolvent series

noncomputable def Matrix.resolventSeries {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : Matrix n n (PowerSeries R)

The resolvent series of M: the matrix over R⟦X⟧ whose (i, j) entry is ∑ₖ (Mᵏ) i j Xᵏ. It is the inverse of 1 - X • M, see Matrix.resolventSeries_eq_inv.

Equations

• M.resolventSeries = Matrix.of fun (i j : n) => PowerSeries.mk fun (k : ℕ) => (M ^ k) i j

theorem Matrix.resolventSeries_apply {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) (i j : n) : M.resolventSeries i j = PowerSeries.mk fun (k : ℕ) => (M ^ k) i j

@[simp]

theorem Matrix.coeff_resolventSeries_apply {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) (i j : n) (k : ℕ) : (PowerSeries.coeff k) (M.resolventSeries i j) = (M ^ k) i j

theorem Matrix.map_C_mul_resolventSeries {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : M.map ⇑PowerSeries.C * M.resolventSeries = of fun (i j : n) => PowerSeries.mk fun (k : ℕ) => (M ^ (k + 1)) i j

Multiplying the resolvent series on the left by M shifts the powers by one.

theorem Matrix.resolventSeries_mul_map_C {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : M.resolventSeries * M.map ⇑PowerSeries.C = of fun (i j : n) => PowerSeries.mk fun (k : ℕ) => (M ^ (k + 1)) i j

Multiplying the resolvent series on the right by M shifts the powers by one.

theorem Matrix.one_sub_X_smul_mul_resolventSeries {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : (1 - PowerSeries.X • M.map ⇑PowerSeries.C) * M.resolventSeries = 1

The resolvent series is a right inverse of 1 - X • M.

theorem Matrix.resolventSeries_mul_one_sub_X_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : M.resolventSeries * (1 - PowerSeries.X • M.map ⇑PowerSeries.C) = 1

The resolvent series is a left inverse of 1 - X • M.

theorem Matrix.resolventSeries_eq_inv {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : M.resolventSeries = (1 - PowerSeries.X • M.map ⇑PowerSeries.C)⁻¹

The resolvent series is the inverse of 1 - X • M in Matrix n n R⟦X⟧.

theorem Matrix.trace_resolventSeries {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : M.resolventSeries.trace = PowerSeries.mk fun (k : ℕ) => (M ^ k).trace

The trace of the resolvent series is the generating function of the traces of the powers.

theorem Matrix.trace_resolventSeries_mul_map_C {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : (M.resolventSeries * M.map ⇑PowerSeries.C).trace = PowerSeries.mk fun (k : ℕ) => (M ^ (k + 1)).trace

The trace of resolventSeries M * M is ∑ₖ trace (Mᵏ⁺¹) Xᵏ.

theorem Matrix.det_smul_resolventSeries {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : (1 - PowerSeries.X • M.map ⇑PowerSeries.C).det • M.resolventSeries = (1 - PowerSeries.X • M.map ⇑PowerSeries.C).adjugate

adjugate (1 - X • M) = det (1 - X • M) • resolventSeries M.

Jacobi's formula

theorem Matrix.derivative_det {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (A : Matrix n n (Polynomial R)) : Polynomial.derivative A.det = (A.adjugate * A.map ⇑Polynomial.derivative).trace

Jacobi's formula: for a square matrix A of polynomials, derivative (det A) = trace (adjugate A * A.map derivative).

theorem Matrix.map_derivative_one_sub_X_smul {n : Type u_1} {R : Type u_2} [DecidableEq n] [CommRing R] (M : Matrix n n R) : (1 - Polynomial.X • M.map ⇑Polynomial.C).map ⇑Polynomial.derivative = -M.map ⇑Polynomial.C

The entrywise derivative of 1 - X • M is -M.

Newton's identity for traces

theorem Matrix.coe_derivative_charpolyRev_eq_neg_mul_mk_trace_pow {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : ↑(Polynomial.derivative M.charpolyRev) = -↑M.charpolyRev * PowerSeries.mk fun (k : ℕ) => (M ^ (k + 1)).trace

Newton's identity for traces of matrix powers: in R⟦X⟧, (charpolyRev M)′ = - charpolyRev M * ∑ₖ trace (Mᵏ⁺¹) Xᵏ. Equivalently, ∑ₖ₌₁^∞ trace (Mᵏ) Xᵏ = - X (charpolyRev M)′ / charpolyRev M.

theorem Matrix.derivative_coe_charpolyRev {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (M : Matrix n n R) : PowerSeries.derivative ↑M.charpolyRev = -↑M.charpolyRev * PowerSeries.mk fun (k : ℕ) => (M ^ (k + 1)).trace

Newton's identity for traces with the derivative taken in R⟦X⟧: d⁄dX (charpolyRev M) = - charpolyRev M * ∑ₖ trace (Mᵏ⁺¹) Xᵏ.