The derivative of the determinant at the identity

The determinant of a square matrix over a complete nontrivially normed field is a polynomial in the entries, hence differentiable, and its derivative at the identity matrix is the trace:

det (1 + H) = 1 + trace H + o(H).

This is Jacobi's formula at the identity. Along a line it is the statement that the polynomial t ↦ det (1 + t • B) has linear coefficient trace B, which Mathlib records as Matrix.derivative_det_one_add_X_smul; differentiability of the determinant then upgrades that directional derivative to the Fréchet derivative.

The normed structure on matrices is Mathlib's L∞ operator norm, available through open scoped Matrix.Norms.Operator; any other norm on the finite-dimensional space of matrices gives the same derivative.

Main results

• Matrix.hasDerivAt_det_one_add_smul: t ↦ det (1 + t • B) has derivative trace B at 0.
• Matrix.differentiable_det: the determinant is differentiable.
• Matrix.hasFDerivAt_det_one: the derivative of the determinant at the identity is the trace.

theorem Matrix.hasDerivAt_det_one_add_smul {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] (B : Matrix n n 𝕜) : HasDerivAt (fun (t : 𝕜) => (1 + t • B).det) B.trace 0

The determinant along the line through the identity in the direction B has derivative trace B at the identity.

theorem Matrix.differentiable_det {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] : Differentiable 𝕜 det

The determinant is differentiable: it is a sum of products of matrix entries.

theorem Matrix.hasFDerivAt_det_one {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] : HasFDerivAt det (LinearMap.toContinuousLinearMap (traceLinearMap n 𝕜 𝕜)) 1

The derivative of the determinant at the identity is the trace (Jacobi's formula at the identity).