Derivations of determinants and norms

A derivation D differentiates a finite product termwise (Derivation.leibniz_prod), and hence a determinant by Jacobi's formula D (det M) = tr (adj M * D M), where D M applies D to every entry of the square matrix M (Derivation.leibniz_det).

Let S be a finite free algebra over a commutative ring A, and let D' be a derivation of S extending a derivation D of A, in the sense that D' (algebraMap A S a) = algebraMap A S (D a). Then the norm of a unit u of S has logarithmic derivative the trace of the logarithmic derivative of u (Derivation.leibniz_norm):

D (Algebra.norm A u) = Algebra.norm A u * Algebra.trace A S (u⁻¹ * D' u).

In a basis of S over A, the derivation D' acts on coordinates as D plus a connection matrix Γ, so D applied to the matrix of multiplication by u is the matrix of multiplication by D' u plus the commutator of that matrix with Γ (Derivation.map_leftMulMatrix). The commutator does not contribute to Jacobi's formula. This is the infinitesimal form of the identity log (Algebra.norm A (1 + x)) = Algebra.trace A S (log (1 + x)) in complete filtered algebras where both logarithms converge, such as Novikov rings.

References

• N. Bourbaki, Algebra I, Chapter III, §8 and §9 (determinants, norms and traces).

theorem Derivation.leibniz_det {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (D : Derivation R A A) {n : Type u_3} [Fintype n] [DecidableEq n] (M : Matrix n n A) : D M.det = (M.adjugate * M.map ⇑D).trace

Jacobi's formula: a derivation D differentiates the determinant of M as the trace of the adjugate of M times the entrywise derivative of M.

theorem Derivation.leibniz_norm {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (D : Derivation R A A) {S : Type u_3} [CommRing S] [Algebra A S] [Algebra R S] (D' : Derivation R S S) (hD : ∀ (a : A), D' ((algebraMap A S) a) = (algebraMap A S) (D a)) [Module.Free A S] [Module.Finite A S] (u : Sˣ) : D ((Algebra.norm A) ↑u) = (Algebra.norm A) ↑u * (Algebra.trace A S) (↑u⁻¹ * D' ↑u)

Logarithmic derivative of the norm: if D' is a derivation of a finite free A-algebra S extending the derivation D of A, then for every unit u of S, D (N u) = N u * Tr (u⁻¹ * D' u).