Truncated matrix exponential series over coefficient algebras

Matrix.expSeries A d x is the finite sum for exp(x • A) truncated below degree d. It is defined over any commutative algebra of the base field, including polynomial rings and dual numbers, without assuming that A is nilpotent. AlgHom.map_expSeries gives its naturality under change of coefficients, and Matrix.expSeries_inr computes its value at a purely infinitesimal dual number. These formulas let polynomial matrix families be evaluated and differentiated algebraically.

noncomputable def Matrix.expSeries {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] [DecidableEq ι] {S : Type u_3} [CommRing S] [Algebra K S] (A : Matrix ι ι K) (d : ℕ) (x : S) : Matrix ι ι S

The exponential series of x • A, truncated below degree d, for a matrix A over K and a scalar x in a commutative K-algebra S. It is a truncated sum rather than IsNilpotent.exp so that it is defined over every commutative K-algebra, polynomial rings and dual numbers included, and commutes with every K-algebra map.

theorem Matrix.expSeries_def {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] [DecidableEq ι] {S : Type u_3} [CommRing S] [Algebra K S] (A : Matrix ι ι K) (d : ℕ) (x : S) : A.expSeries d x = ∑ k ∈ Finset.range d, (x ^ k * (algebraMap K S) (↑k.factorial)⁻¹) • A.map ⇑(algebraMap K S) ^ k

The finite-sum formula for the truncated exponential series.

@[simp]

theorem AlgHom.map_expSeries {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] [DecidableEq ι] {S : Type u_3} {S' : Type u_4} [CommRing S] [Algebra K S] [CommRing S'] [Algebra K S'] (f : S →ₐ[K] S') (A : Matrix ι ι K) (d : ℕ) (x : S) : (A.expSeries d x).map ⇑f = A.expSeries d (f x)

The truncated exponential series is natural in the coefficient algebra.

theorem Matrix.expSeries_inr {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] [DecidableEq ι] {d : ℕ} (hd : 2 ≤ d) (A : Matrix ι ι K) (c : K) : A.expSeries d (TrivSqZeroExt.inr c) = 1 + (c • A).map TrivSqZeroExt.inr

With a square-zero coefficient ε c, the truncated exponential series is 1 + ε c A.