Matrices of dual numbers are isomorphic to dual numbers over matrices #
Showing this for the more general case of TrivSqZeroExt R M
would require an action between
Matrix n n R
and Matrix n n M
, which would risk causing diamonds.
@[simp]
theorem
Matrix.dualNumberEquiv_symm_apply
{R : Type}
{n : Type}
[CommSemiring R]
[Fintype n]
[DecidableEq n]
(d : DualNumber (Matrix n n R))
:
↑(AlgEquiv.symm Matrix.dualNumberEquiv) d = ↑Matrix.of fun i j =>
(TrivSqZeroExt.fst (Matrix n n R) (Matrix n n R) d i j, TrivSqZeroExt.snd (Matrix n n R) (Matrix n n R) d i j)
@[simp]
theorem
Matrix.dualNumberEquiv_apply
{R : Type}
{n : Type}
[CommSemiring R]
[Fintype n]
[DecidableEq n]
(A : Matrix n n (DualNumber R))
:
↑Matrix.dualNumberEquiv A = (↑Matrix.of fun i j => TrivSqZeroExt.fst (A i j), ↑Matrix.of fun i j => TrivSqZeroExt.snd (A i j))
def
Matrix.dualNumberEquiv
{R : Type}
{n : Type}
[CommSemiring R]
[Fintype n]
[DecidableEq n]
:
Matrix n n (DualNumber R) ≃ₐ[R] DualNumber (Matrix n n R)
Matrices over dual numbers and dual numbers over matrices are isomorphic.