How a matrix interacts with the cross product

A 3 × 3 matrix M acts on R³, and the cross product is a bilinear map R³ × R³ → R³, so one may ask how the two compose. The answer is the infinitesimal form of the Cauchy--Binet identity (M u) ⨯₃ (M w) = (adj M)ᵀ (u ⨯₃ w): replacing M by 1 + ε M and reading off the linear term in ε,

(M u) ⨯₃ w + u ⨯₃ (M w) = (tr M) • (u ⨯₃ w) - Mᵀ (u ⨯₃ w).

So the cross product is not preserved by an arbitrary matrix, but a trace-zero matrix acts on it as a derivation with -Mᵀ in the target slot, which is the form the identity is used in.

Main results

• Matrix.mulVec_cross_add_cross_mulVec: the identity above.
• Matrix.mulVec_cross_add_cross_mulVec_of_trace_eq_zero: its trace-zero case.

theorem Matrix.mulVec_cross_add_cross_mulVec {R : Type u_1} [CommRing R] (M : Matrix (Fin 3) (Fin 3) R) (u w : Fin 3 → R) : (crossProduct (M.mulVec u)) w + (crossProduct u) (M.mulVec w) = M.trace • (crossProduct u) w - M.transpose.mulVec ((crossProduct u) w)

A matrix acting on a cross product. Applying M to one factor at a time and adding gives the trace of M times the cross product, corrected by -Mᵀ applied to it. This is the derivative at the identity of the Cauchy--Binet identity (M u) ⨯₃ (M w) = (adj M)ᵀ (u ⨯₃ w).

theorem Matrix.mulVec_cross_add_cross_mulVec_of_trace_eq_zero {R : Type u_1} [CommRing R] (M : Matrix (Fin 3) (Fin 3) R) (hM : M.trace = 0) (u w : Fin 3 → R) : (crossProduct (M.mulVec u)) w + (crossProduct u) (M.mulVec w) = -M.transpose.mulVec ((crossProduct u) w)

A trace-zero matrix acts on the cross product as a derivation, with the transpose acting on the target: (M u) ⨯₃ w + u ⨯₃ (M w) = -(Mᵀ (u ⨯₃ w)).