-
Notifications
You must be signed in to change notification settings - Fork 251
/
DualNumber.lean
44 lines (37 loc) · 1.69 KB
/
DualNumber.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
/-
Copyright (c) 2023 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
import Mathlib.Algebra.DualNumber
import Mathlib.Data.Matrix.Basic
#align_import data.matrix.dual_number from "leanprover-community/mathlib"@"eb0cb4511aaef0da2462207b67358a0e1fe1e2ee"
/-!
# 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.
-/
variable {R n : Type} [CommSemiring R] [Fintype n] [DecidableEq n]
open Matrix TrivSqZeroExt
/-- Matrices over dual numbers and dual numbers over matrices are isomorphic. -/
@[simps]
def Matrix.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)
left_inv A := Matrix.ext fun i j => TrivSqZeroExt.ext rfl rfl
right_inv d := TrivSqZeroExt.ext (Matrix.ext fun i j => rfl) (Matrix.ext fun i j => rfl)
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' A B := TrivSqZeroExt.ext rfl rfl
commutes' r := by
simp_rw [algebraMap_eq_inl', algebraMap_eq_diagonal, Pi.algebraMap_def,
Algebra.id.map_eq_self, algebraMap_eq_inl, ← diagonal_map (inl_zero R), map_apply, fst_inl,
snd_inl]
rfl
#align matrix.dual_number_equiv Matrix.dualNumberEquiv