Matrices of dual numbers are isomorphic to dual numbers over matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Showing this for the more general case of triv_sq_zero_ext R M would require an action between
matrix n n R and matrix n n M, which would risk causing diamonds.
@[simp]
theorem
matrix.dual_number_equiv_symm_apply
{R n : Type}
[comm_semiring R]
[fintype n]
[decidable_eq n]
(d : dual_number (matrix n n R)) :
⇑(matrix.dual_number_equiv.symm) d = ⇑matrix.of (λ (i j : n), (triv_sq_zero_ext.fst d i j, triv_sq_zero_ext.snd d i j))
def
matrix.dual_number_equiv
{R n : Type}
[comm_semiring R]
[fintype n]
[decidable_eq n] :
matrix n n (dual_number R) ≃ₐ[R] dual_number (matrix n n R)
Matrices over dual numbers and dual numbers over matrices are isomorphic.
Equations
- matrix.dual_number_equiv = {to_fun := λ (A : matrix n n (dual_number R)), (⇑matrix.of (λ (i j : n), triv_sq_zero_ext.fst (A i j)), ⇑matrix.of (λ (i j : n), triv_sq_zero_ext.snd (A i j))), inv_fun := λ (d : dual_number (matrix n n R)), ⇑matrix.of (λ (i j : n), (triv_sq_zero_ext.fst d i j, triv_sq_zero_ext.snd d i j)), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
matrix.dual_number_equiv_apply
{R n : Type}
[comm_semiring R]
[fintype n]
[decidable_eq n]
(A : matrix n n (dual_number R)) :
⇑matrix.dual_number_equiv A = (⇑matrix.of (λ (i j : n), triv_sq_zero_ext.fst (A i j)), ⇑matrix.of (λ (i j : n), triv_sq_zero_ext.snd (A i j)))