Jacobi's formula on a manifold

Let A be a square-matrix-valued function on a manifold whose entries are differentiable at x, with A x invertible. Then the determinant of A is differentiable at x, and along a tangent vector v its derivative is given by Jacobi's formula

d (det A) (v) = det (A x) * trace ((A x)⁻¹ * dA (v)),

where dA (v) is the matrix of the derivatives of the entries of A along v. The statement only involves derivatives of scalar functions, so no normed structure on matrices appears in it; the proof reads A as a map into the product space of its entries and applies the flat formula Matrix.fderiv_det_apply.

The determinant has every nonzero scalar as a regular value for a nonempty matrix index. At the identity its model-valued derivative is the trace, with no completeness assumption.

Main declarations

• TauCeti.mvfderiv_det_apply: Jacobi's formula along a manifold-valued map.
• Matrix.mvfderiv_det_one: the trace formula at the identity.
• Matrix.isRegularValue_det: nonzero values of the determinant are regular.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 7, Example 7.18(c),(e).

theorem TauCeti.mvfderiv_det_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : Type u_5} [Fintype n] [DecidableEq n] {A : M → Matrix n n 𝕜} {x : M} (hA : ∀ (i j : n), (MDiffAt fun (y : M) => A y i j) x) (hdet : IsUnit (A x).det) (v : TangentSpace I x) : ((d% fun (y : M) => (A y).det) x) v = (A x).det * ((A x)⁻¹ * Matrix.of fun (i j : n) => ((d% fun (y : M) => A y i j) x) v).trace

Jacobi's formula on a manifold. If the entries of a matrix-valued function A are differentiable at x and A x has invertible determinant, then along a tangent vector v the derivative of det A is det (A x) * trace ((A x)⁻¹ * dA (v)), where dA (v) is the matrix of the derivatives of the entries of A along v.

theorem Matrix.mvfderiv_det_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (v : TangentSpace (modelWithCornersSelf 𝕜 (Matrix n n 𝕜)) 1) : (d% det 1) v = ((NormedSpace.fromTangentSpace 1) v).trace

The determinant's model-valued differential at the identity is the matrix trace.

theorem Matrix.isRegularValue_det {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] {c : 𝕜} (hc : c ≠ 0) : TauCeti.IsRegularValue (modelWithCornersSelf 𝕜 (Matrix n n 𝕜)) (modelWithCornersSelf 𝕜 𝕜) det c

Every nonzero scalar is a regular value of the determinant for a nonempty matrix index.