Infinitesimal matrices over the dual numbers

A matrix over R becomes infinitesimal over the dual numbers TrivSqZeroExt R R when its entries are multiplied by ε, that is, mapped entrywise by TrivSqZeroExt.inr. Products of two such matrices vanish, so a product of matrices 1 + ε M_a is 1 + ε ∑ M_a, and 1 + ε M acts on a dual vector u + ε u' as u + ε (M u + u'). These are the computations behind reading off a differential from an evaluation at dual numbers.

theorem Matrix.map_inr_mul_map_inr {R : Type u_1} [Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix l m R) (N : Matrix m n R) : M.map TrivSqZeroExt.inr * N.map TrivSqZeroExt.inr = 0

The product of two infinitesimal matrices vanishes.

theorem Matrix.one_add_map_inr_mulVec {R : Type u_1} [Semiring R] {n : Type u_4} [Fintype n] [DecidableEq n] (M : Matrix n n R) (u u' : n → R) : ((1 + M.map TrivSqZeroExt.inr).mulVec fun (i : n) => TrivSqZeroExt.inl (u i) + TrivSqZeroExt.inr (u' i)) = fun (i : n) => TrivSqZeroExt.inl (u i) + TrivSqZeroExt.inr ((M.mulVec u + u') i)

The matrix 1 + ε M acts on the dual vector u + ε u' as u + ε (M u + u').

theorem List.prod_map_one_add_map_inr {R : Type u_1} [Semiring R] {α : Type u_2} {n : Type u_3} [Fintype n] [DecidableEq n] (l : List α) (M : α → Matrix n n R) : (map (fun (a : α) => 1 + (M a).map TrivSqZeroExt.inr) l).prod = 1 + (map M l).sum.map TrivSqZeroExt.inr

A product of matrices 1 + ε M_a is 1 + ε ∑ M_a, since products of infinitesimal matrices vanish.