The determinant of a matrix exponential

For a square matrix A over ℝ or ℂ (any RCLike field),

det (exp A) = exp (trace A).

This is listed as a TODO in Mathlib's Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean. No diagonalization is involved, so the identity holds for every matrix, including the real matrices that are not diagonalizable over ℂ either.

The argument

The function f t = det (exp (t • A)) is a homomorphism from the additive group of the field to its multiplicative monoid, because the exponentials of the commuting matrices s • A and t • A multiply. Its derivative at 0 is trace A: the curve t ↦ exp (t • A) leaves the identity with velocity A, and the derivative of the determinant at the identity is the trace (Matrix.hasFDerivAt_det_one). The homomorphism property transports this to every point, so f' = trace A • f, and then t ↦ f t * exp (-t • trace A) has vanishing derivative and is the constant 1. Evaluating at t = 1 gives the identity.

Main results

• Matrix.det_exp: det (exp A) = exp (trace A).

References

• B. C. Hall, Lie Groups, Lie Algebras, and Representations, 2nd ed., Springer GTM 222 (2015), Chapter 2, where the identity is proved by triangularizing A; the differential argument used here avoids any normal form.

theorem Matrix.det_exp {n : Type u_1} [Fintype n] [DecidableEq n] {𝕂 : Type u_2} [RCLike 𝕂] (A : Matrix n n 𝕂) : (NormedSpace.exp A).det = NormedSpace.exp A.trace

The determinant of the exponential of a matrix is the exponential of its trace.