Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 536c256

Browse files
eric-wiesereric-wieser
committed
feat(algebra/dual_quaternion): two equivalent ways to construct the dual quaternions (#18383)
We show that the dual numbers with quaternion coefficients are isomorphic as an algebra to the quaternions with dual number coefficients. The result is trivial, but being able to state it turned out to require generalizations of existing typeclass instances, which are handled in prework PRs. This is very similar to #18386.
1 parent a51ce54 commit 536c256

1 file changed

Lines changed: 94 additions & 0 deletions

File tree

‎src/algebra/dual_quaternion.lean‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
/-
2+
Copyright (c) 2023 Eric Wieser. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Eric Wieser
5+
-/
6+
import algebra.dual_number
7+
import algebra.quaternion
8+
9+
/-!
10+
# Dual quaternions
11+
12+
Similar to the way that rotations in 3D space can be represented by quaternions of unit length,
13+
rigid motions in 3D space can be represented by dual quaternions of unit length.
14+
15+
## Main results
16+
17+
* `quaternion.dual_number_equiv`: quaternions over dual numbers or dual
18+
numbers over quaternions are equivalent constructions.
19+
20+
## References
21+
22+
* <https://en.wikipedia.org/wiki/Dual_quaternion>
23+
-/
24+
25+
variables {R : Type*} [comm_ring R]
26+
27+
namespace quaternion
28+
29+
/-- The dual quaternions can be equivalently represented as a quaternion with dual coefficients,
30+
or as a dual number with quaternion coefficients.
31+
32+
See also `matrix.dual_number_equiv` for a similar result. -/
33+
def dual_number_equiv :
34+
quaternion (dual_number R) ≃ₐ[R] dual_number (quaternion R) :=
35+
{ to_fun := λ q,
36+
(⟨q.re.fst, q.im_i.fst, q.im_j.fst, q.im_k.fst⟩,
37+
⟨q.re.snd, q.im_i.snd, q.im_j.snd, q.im_k.snd⟩),
38+
inv_fun := λ d,
39+
⟨(d.fst.re, d.snd.re), (d.fst.im_i, d.snd.im_i),
40+
(d.fst.im_j, d.snd.im_j), (d.fst.im_k, d.snd.im_k)⟩,
41+
left_inv := λ ⟨⟨r, rε⟩, ⟨i, iε⟩, ⟨j, jε⟩, ⟨k, kε⟩⟩, rfl,
42+
right_inv := λ ⟨⟨r, i, j, k⟩, ⟨rε, iε, jε, kε⟩⟩, rfl,
43+
map_mul' := begin
44+
rintros ⟨⟨xr, xrε⟩, ⟨xi, xiε⟩, ⟨xj, xjε⟩, ⟨xk, xkε⟩⟩,
45+
rintros ⟨⟨yr, yrε⟩, ⟨yi, yiε⟩, ⟨yj, yjε⟩, ⟨yk, ykε⟩⟩,
46+
ext : 1,
47+
{ refl },
48+
{ dsimp,
49+
congr' 1; ring },
50+
end,
51+
map_add' := begin
52+
rintros ⟨⟨xr, xrε⟩, ⟨xi, xiε⟩, ⟨xj, xjε⟩, ⟨xk, xkε⟩⟩,
53+
rintros ⟨⟨yr, yrε⟩, ⟨yi, yiε⟩, ⟨yj, yjε⟩, ⟨yk, ykε⟩⟩,
54+
refl
55+
end,
56+
commutes' := λ r, rfl }
57+
58+
/-! Lemmas characterizing `quaternion.dual_number_equiv`. -/
59+
60+
-- `simps` can't work on `dual_number` because it's not a structure
61+
@[simp] lemma re_fst_dual_number_equiv (q : quaternion (dual_number R)) :
62+
(dual_number_equiv q).fst.re = q.re.fst := rfl
63+
@[simp] lemma im_i_fst_dual_number_equiv (q : quaternion (dual_number R)) :
64+
(dual_number_equiv q).fst.im_i = q.im_i.fst := rfl
65+
@[simp] lemma im_j_fst_dual_number_equiv (q : quaternion (dual_number R)) :
66+
(dual_number_equiv q).fst.im_j = q.im_j.fst := rfl
67+
@[simp] lemma im_k_fst_dual_number_equiv (q : quaternion (dual_number R)) :
68+
(dual_number_equiv q).fst.im_k = q.im_k.fst := rfl
69+
@[simp] lemma re_snd_dual_number_equiv (q : quaternion (dual_number R)) :
70+
(dual_number_equiv q).snd.re = q.re.snd := rfl
71+
@[simp] lemma im_i_snd_dual_number_equiv (q : quaternion (dual_number R)) :
72+
(dual_number_equiv q).snd.im_i = q.im_i.snd := rfl
73+
@[simp] lemma im_j_snd_dual_number_equiv (q : quaternion (dual_number R)) :
74+
(dual_number_equiv q).snd.im_j = q.im_j.snd := rfl
75+
@[simp] lemma im_k_snd_dual_number_equiv (q : quaternion (dual_number R)) :
76+
(dual_number_equiv q).snd.im_k = q.im_k.snd := rfl
77+
@[simp] lemma fst_re_dual_number_equiv_symm (d : dual_number (quaternion R)) :
78+
(dual_number_equiv.symm d).re.fst = d.fst.re := rfl
79+
@[simp] lemma fst_im_i_dual_number_equiv_symm (d : dual_number (quaternion R)) :
80+
(dual_number_equiv.symm d).im_i.fst = d.fst.im_i := rfl
81+
@[simp] lemma fst_im_j_dual_number_equiv_symm (d : dual_number (quaternion R)) :
82+
(dual_number_equiv.symm d).im_j.fst = d.fst.im_j := rfl
83+
@[simp] lemma fst_im_k_dual_number_equiv_symm (d : dual_number (quaternion R)) :
84+
(dual_number_equiv.symm d).im_k.fst = d.fst.im_k := rfl
85+
@[simp] lemma snd_re_dual_number_equiv_symm (d : dual_number (quaternion R)) :
86+
(dual_number_equiv.symm d).re.snd = d.snd.re := rfl
87+
@[simp] lemma snd_im_i_dual_number_equiv_symm (d : dual_number (quaternion R)) :
88+
(dual_number_equiv.symm d).im_i.snd = d.snd.im_i := rfl
89+
@[simp] lemma snd_im_j_dual_number_equiv_symm (d : dual_number (quaternion R)) :
90+
(dual_number_equiv.symm d).im_j.snd = d.snd.im_j := rfl
91+
@[simp] lemma snd_im_k_dual_number_equiv_symm (d : dual_number (quaternion R)) :
92+
(dual_number_equiv.symm d).im_k.snd = d.snd.im_k := rfl
93+
94+
end quaternion

0 commit comments

Comments
 (0)