Derivations applied entrywise to matrices

A derivation D of a commutative algebra A acts on matrices over A entry by entry, through Matrix.map. This entrywise action satisfies the Leibniz rule for matrix multiplication, (M * N).map D = M.map D * N + M * N.map D, because each entry of a product is a sum of products of entries.

A consequence is used to show that trace polynomials are invariant: if D acts on a square matrix M as the commutator with some matrix B, so M.map D = B * M - M * B, then it acts on every power M ^ m as the commutator with the same B. Since D commutes with the trace and the trace of a commutator vanishes, D then kills every trace (M ^ m).trace.

Let S be an A-algebra with a basis b, and let D' be a derivation of S extending D, in the sense that D' (algebraMap A S a) = algebraMap A S (D a). Then D' acts on coordinates in b as D plus the connection matrix Γ whose columns are the coordinates of the D' (b q). Consequently D, applied entrywise to the matrix of multiplication by s, gives the matrix of multiplication by D' s plus the commutator of the matrix of s with Γ.

Main results

• Derivation.map_matrix_mul: the Leibniz rule for the entrywise action on matrix products.
• Derivation.map_matrix_pow_of_map_eq_mul_sub_mul: if D acts on M as the commutator with B, it acts on each power of M as the commutator with B.
• Derivation.trace_pow_eq_zero_of_map_eq_mul_sub_mul: under the same hypothesis, D kills the traces of the powers of M.
• Derivation.basis_repr_apply: the coordinates of D' x in a basis, for a derivation D' extending D.
• Derivation.map_leftMulMatrix: the entrywise derivative of the matrix of multiplication.

theorem Derivation.map_matrix_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) {l : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype m] (M : Matrix l m A) (N : Matrix m n A) : (M * N).map ⇑D = M.map ⇑D * N + M * N.map ⇑D

The Leibniz rule for matrices: a derivation applied entrywise to a product of matrices is M.map D * N + M * N.map D.

theorem Derivation.map_matrix_pow_of_map_eq_mul_sub_mul {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 B : Matrix n n A} (h : M.map ⇑D = B * M - M * B) (m : ℕ) : (M ^ m).map ⇑D = B * M ^ m - M ^ m * B

If a derivation acts on a square matrix M as the commutator with B, then it acts on every power of M as the commutator with B.

theorem Derivation.trace_pow_eq_zero_of_map_eq_mul_sub_mul {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 B : Matrix n n A} (h : M.map ⇑D = B * M - M * B) (m : ℕ) : D (M ^ m).trace = 0

If a derivation acts on a square matrix M as the commutator with B, then it kills the trace of every power of M.

theorem Derivation.basis_repr_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (D : Derivation R A A) {S : Type u_4} [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)) {ι : Type u_5} [Fintype ι] (b : Module.Basis ι A S) (x : S) (p : ι) : (b.repr (D' x)) p = D ((b.repr x) p) + ∑ r : ι, (b.repr x) r * (b.repr (D' (b r))) p

In a basis b, the coordinates of D' x are the derivatives of the coordinates of x plus the connection term ∑ r, b.repr x r * b.repr (D' (b r)) p.

theorem Derivation.map_leftMulMatrix {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (D : Derivation R A A) {S : Type u_4} [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)) {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι A S) (s : S) : ((Algebra.leftMulMatrix b) s).map ⇑D = (Algebra.leftMulMatrix b) (D' s) + (((Algebra.leftMulMatrix b) s * Matrix.of fun (p q : ι) => (b.repr (D' (b q))) p) - (Matrix.of fun (p q : ι) => (b.repr (D' (b q))) p) * (Algebra.leftMulMatrix b) s)

In a basis b, the entrywise derivative of the matrix of multiplication by s is the matrix of multiplication by D' s plus the commutator of that matrix with the connection matrix of D' in b.