Dual quaternions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Similar to the way that rotations in 3D space can be represented by quaternions of unit length, rigid motions in 3D space can be represented by dual quaternions of unit length.

Main results #

quaternion.dual_number_equiv: quaternions over dual numbers or dual numbers over quaternions are equivalent constructions.

References #

https://en.wikipedia.org/wiki/Dual_quaternion

source

def quaternion.dual_number_equiv {R : Type u_1} [comm_ring R] :

quaternion (dual_number R) ≃ₐ[R] dual_number (quaternion R)

The dual quaternions can be equivalently represented as a quaternion with dual coefficients, or as a dual number with quaternion coefficients.

See also matrix.dual_number_equiv for a similar result.

Equations

quaternion.dual_number_equiv = {to_fun := λ (q : quaternion (dual_number R)), ({re := triv_sq_zero_ext.fst q.re, im_i := triv_sq_zero_ext.fst q.im_i, im_j := triv_sq_zero_ext.fst q.im_j, im_k := triv_sq_zero_ext.fst q.im_k}, {re := triv_sq_zero_ext.snd q.re, im_i := triv_sq_zero_ext.snd q.im_i, im_j := triv_sq_zero_ext.snd q.im_j, im_k := triv_sq_zero_ext.snd q.im_k}), inv_fun := λ (d : dual_number (quaternion R)), {re := ((triv_sq_zero_ext.fst d).re, (triv_sq_zero_ext.snd d).re), im_i := ((triv_sq_zero_ext.fst d).im_i, (triv_sq_zero_ext.snd d).im_i), im_j := ((triv_sq_zero_ext.fst d).im_j, (triv_sq_zero_ext.snd d).im_j), im_k := ((triv_sq_zero_ext.fst d).im_k, (triv_sq_zero_ext.snd d).im_k)}, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

Lemmas characterizing quaternion.dual_number_equiv.

source

@[simp]

theorem quaternion.re_fst_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.fst (⇑quaternion.dual_number_equiv q)).re = triv_sq_zero_ext.fst q.re

source

@[simp]

theorem quaternion.im_i_fst_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.fst (⇑quaternion.dual_number_equiv q)).im_i = triv_sq_zero_ext.fst q.im_i

source

@[simp]

theorem quaternion.im_j_fst_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.fst (⇑quaternion.dual_number_equiv q)).im_j = triv_sq_zero_ext.fst q.im_j

source

@[simp]

theorem quaternion.im_k_fst_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.fst (⇑quaternion.dual_number_equiv q)).im_k = triv_sq_zero_ext.fst q.im_k

source

@[simp]

theorem quaternion.re_snd_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.snd (⇑quaternion.dual_number_equiv q)).re = triv_sq_zero_ext.snd q.re

source

@[simp]

theorem quaternion.im_i_snd_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.snd (⇑quaternion.dual_number_equiv q)).im_i = triv_sq_zero_ext.snd q.im_i

source

@[simp]

theorem quaternion.im_j_snd_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.snd (⇑quaternion.dual_number_equiv q)).im_j = triv_sq_zero_ext.snd q.im_j

source

@[simp]

theorem quaternion.im_k_snd_dual_number_equiv {R : Type u_1} [comm_ring R] (q : quaternion (dual_number R)) :

(triv_sq_zero_ext.snd (⇑quaternion.dual_number_equiv q)).im_k = triv_sq_zero_ext.snd q.im_k

source

@[simp]

theorem quaternion.fst_re_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.fst (⇑(quaternion.dual_number_equiv.symm) d).re = (triv_sq_zero_ext.fst d).re

source

@[simp]

theorem quaternion.fst_im_i_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.fst (⇑(quaternion.dual_number_equiv.symm) d).im_i = (triv_sq_zero_ext.fst d).im_i

source

@[simp]

theorem quaternion.fst_im_j_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.fst (⇑(quaternion.dual_number_equiv.symm) d).im_j = (triv_sq_zero_ext.fst d).im_j

source

@[simp]

theorem quaternion.fst_im_k_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.fst (⇑(quaternion.dual_number_equiv.symm) d).im_k = (triv_sq_zero_ext.fst d).im_k

source

@[simp]

theorem quaternion.snd_re_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.snd (⇑(quaternion.dual_number_equiv.symm) d).re = (triv_sq_zero_ext.snd d).re

source

@[simp]

theorem quaternion.snd_im_i_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.snd (⇑(quaternion.dual_number_equiv.symm) d).im_i = (triv_sq_zero_ext.snd d).im_i

source

@[simp]

theorem quaternion.snd_im_j_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.snd (⇑(quaternion.dual_number_equiv.symm) d).im_j = (triv_sq_zero_ext.snd d).im_j

source

@[simp]

theorem quaternion.snd_im_k_dual_number_equiv_symm {R : Type u_1} [comm_ring R] (d : dual_number (quaternion R)) :

triv_sq_zero_ext.snd (⇑(quaternion.dual_number_equiv.symm) d).im_k = (triv_sq_zero_ext.snd d).im_k