English
There is an algebra isomorphism between the algebra of n-by-n matrices over DualNumber(R) and the algebra of DualNumber-valued n-by-n matrices over R.
Русский
Существуют алгебраические изоморфизм между алгеброй матриц размером n×n над двойномерными числами DualNumber(R) и алгеброй двойномерных чисел над матрицами M_n(R).
LaTeX
$$$M_{n}(\mathrm{DualNumber}(R)) \cong_{R} \mathrm{DualNumber}(M_{n}(R)).$$$
Lean4
/-- Matrices over dual numbers and dual numbers over matrices are isomorphic. -/
@[simps]
def dualNumberEquiv : Matrix n n (DualNumber R) ≃ₐ[R] DualNumber (Matrix n n R)
where
toFun A := ⟨of fun i j => (A i j).fst, of fun i j => (A i j).snd⟩
invFun d := of fun i j => (d.fst i j, d.snd i j)
map_mul' A
B := by
ext
· dsimp [mul_apply]
simp_rw [fst_sum]
rfl
· simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]
simp only [mul_apply, snd_sum, DualNumber.snd_mul, snd_mk, of_apply, fst_mk, add_apply]
rw [← Finset.sum_add_distrib]
map_add' _ _ := TrivSqZeroExt.ext rfl rfl
commutes'
r :=
by
simp_rw [algebraMap_eq_inl', algebraMap_eq_diagonal, Pi.algebraMap_def, Algebra.algebraMap_self_apply,
algebraMap_eq_inl, ← diagonal_map (inl_zero R), map_apply, fst_inl, snd_inl]
rfl
