Matrices of nilpotent adjoint exponentials

Module.Basis.toMatrixAlgEquiv_expAd expresses the matrix of the inner automorphism exp(ad(t • e)) as Matrix.expSeries in the matrix of ad e. Any truncation degree annihilating ad e suffices. This identifies adjoint exponentials with polynomial matrix families in the scalar parameter, without assumptions on Cartan subalgebras or roots.

theorem Module.Basis.toMatrixAlgEquiv_expAd {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [CharZero K] [LieAlgebra ℚ L] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Basis ι K L) {e : L} {d : ℕ} (hd : (LieAlgebra.ad K L) e ^ d = 0) (t : K) (ht : IsNilpotent ((LieAlgebra.ad K L) (t • e))) : (LinearMap.toMatrixAlgEquiv b) ↑(TauCeti.expAd (t • e) ⋯).toLinearEquiv = ((LinearMap.toMatrixAlgEquiv b) ((LieAlgebra.ad K L) e)).expSeries d t

The truncated exponential series of the matrix of ad e is the matrix of exp (ad (t • e)), once the truncation degree kills ad e.