Quaternions #
In this file we define quaternions ℍ[R]
over a commutative ring R
, and define some
algebraic structures on ℍ[R]
.
Main definitions #
quaternion_algebra R a b
,ℍ[R, a, b]
: quaternion algebra with coefficientsa
,b
quaternion R
,ℍ[R]
: the space of quaternions, a.k.a.quaternion_algebra R (-1) (-1)
;quaternion.norm_sq
: square of the norm of a quaternion;quaternion.conj
: conjugate of a quaternion;
We also define the following algebraic structures on ℍ[R]
:
ring ℍ[R, a, b]
andalgebra R ℍ[R, a, b]
: for any commutative ringR
;ring ℍ[R]
andalgebra R ℍ[R]
: for any commutative ringR
;domain ℍ[R]
: for a linear ordered commutative ringR
;division_algebra ℍ[R]
: for a linear ordered fieldR
.
Notation #
The following notation is available with open_locale quaternion
.
ℍ[R, c₁, c₂]
:quaternion_algebra R c₁ c₂
ℍ[R]
: quaternions overR
.
Implementation notes #
We define quaternions over any ring R
, not just ℝ
to be able to deal with, e.g., integer
or rational quaternions without using real numbers. In particular, all definitions in this file
are computable.
Tags #
quaternion
- re : R
- im_i : R
- im_j : R
- im_k : R
Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$.
Implemented as a structure with four fields: re
, im_i
, im_j
, and im_k
.
Multiplication is given by
1 * x = x * 1 = x
;i * i = c₁
;j * j = c₂
;i * j = k
,j * i = -k
;k * k = -c₁ * c₂
;i * k = c₁ * j
,k * i =
-c₁ * j`;j * k = -c₂ * i
, `k * j = c₂ * i`.
Equations
- quaternion_algebra.has_mul = {mul := λ (a b : ℍ[R,c₁,c₂]), {re := (a.re) * b.re + (c₁ * a.im_i) * b.im_i + (c₂ * a.im_j) * b.im_j - ((c₁ * c₂) * a.im_k) * b.im_k, im_i := (a.re) * b.im_i + (a.im_i) * b.re - (c₂ * a.im_j) * b.im_k + (c₂ * a.im_k) * b.im_j, im_j := (a.re) * b.im_j + (c₁ * a.im_i) * b.im_k + (a.im_j) * b.re - (c₁ * a.im_k) * b.im_i, im_k := (a.re) * b.im_k + (a.im_i) * b.im_j - (a.im_j) * b.im_i + (a.im_k) * b.re}}
Equations
- quaternion_algebra.ring = {add := has_add.add quaternion_algebra.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec {add := has_add.add quaternion_algebra.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg quaternion_algebra.has_neg, sub := has_sub.sub quaternion_algebra.has_sub, sub_eq_add_neg := _, gsmul := gsmul_rec {neg := has_neg.neg quaternion_algebra.has_neg}, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul quaternion_algebra.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul quaternion_algebra.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
Equations
Quaternion conjugate.
Equations
- quaternion_algebra.star_ring = {to_star_monoid := {to_has_involutive_star := {to_has_star := {star := ⇑quaternion_algebra.conj}, star_involutive := _}, star_mul := _}, star_add := _}
Quaternion conjugate as an alg_equiv
to the opposite ring.
Equations
- quaternion_algebra.conj_alg_equiv = {to_fun := opposite.op ∘ ⇑quaternion_algebra.conj, inv_fun := ⇑quaternion_algebra.conj ∘ opposite.unop, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
Equations
Equations
Quaternion conjugate.
Equations
Alias of commute_conj_conj
.
Quaternion conjugate as an alg_equiv
to the opposite ring.
Square of the norm.
Equations
- quaternion.domain = {add := ring.add quaternion.ring, add_assoc := _, zero := ring.zero quaternion.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul quaternion.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg quaternion.ring, sub := ring.sub quaternion.ring, sub_eq_add_neg := _, gsmul := ring.gsmul quaternion.ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul quaternion.ring, mul_assoc := _, one := ring.one quaternion.ring, one_mul := _, mul_one := _, npow := ring.npow quaternion.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
Equations
- quaternion.has_inv = {inv := λ (a : ℍ[R]), (⇑quaternion.norm_sq a)⁻¹ • ⇑quaternion.conj a}
Equations
- quaternion.division_ring = {add := domain.add quaternion.domain, add_assoc := _, zero := domain.zero quaternion.domain, zero_add := _, add_zero := _, nsmul := domain.nsmul quaternion.domain, nsmul_zero' := _, nsmul_succ' := _, neg := domain.neg quaternion.domain, sub := domain.sub quaternion.domain, sub_eq_add_neg := _, gsmul := domain.gsmul quaternion.domain, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := domain.mul quaternion.domain, mul_assoc := _, one := domain.one quaternion.domain, one_mul := _, mul_one := _, npow := domain.npow quaternion.domain, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := has_inv.inv quaternion.has_inv, div := div_inv_monoid.div._default domain.mul quaternion.division_ring._proof_19 domain.one quaternion.division_ring._proof_20 quaternion.division_ring._proof_21 domain.npow quaternion.division_ring._proof_22 quaternion.division_ring._proof_23 has_inv.inv, div_eq_mul_inv := _, gpow := div_inv_monoid.gpow._default domain.mul quaternion.division_ring._proof_25 domain.one quaternion.division_ring._proof_26 quaternion.division_ring._proof_27 domain.npow quaternion.division_ring._proof_28 quaternion.division_ring._proof_29 has_inv.inv, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}