Quaternions #
In this file we define quaternions ℍ[R]
over a commutative ring R
, and define some
algebraic structures on ℍ[R]
.
Main definitions #
QuaternionAlgebra R a b
,ℍ[R, a, b]
: quaternion algebra with coefficientsa
,b
Quaternion R
,ℍ[R]
: the space of quaternions, a.k.a.QuaternionAlgebra R (-1) (-1)
;Quaternion.normSq
: square of the norm of a quaternion;
We also define the following algebraic structures on ℍ[R]
:
Ring ℍ[R, a, b]
,StarRing ℍ[R, a, b]
, andAlgebra R ℍ[R, a, b]
: for any commutative ringR
;Ring ℍ[R]
,StarRing ℍ[R]
, andAlgebra R ℍ[R]
: for any commutative ringR
;IsDomain ℍ[R]
: for a linear ordered commutative ringR
;DivisionRing ℍ[R]
: for a linear ordered fieldR
.
Notation #
The following notation is available with open Quaternion
or open scoped Quaternion
.
ℍ[R, c₁, c₂]
:QuaternionAlgebra 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
The equivalence between a quaternion algebra over R
and R × R × R × R
.
Instances For
The equivalence between a quaternion algebra over R
and Fin 4 → R
.
Instances For
The imaginary part of a quaternion.
Instances For
Coercion R → ℍ[R,c₁,c₂]
.
Instances For
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
.
QuaternionAlgebra.re
as a LinearMap
Instances For
QuaternionAlgebra.imI
as a LinearMap
Instances For
QuaternionAlgebra.imJ
as a LinearMap
Instances For
QuaternionAlgebra.imK
as a LinearMap
Instances For
QuaternionAlgebra.equivTuple
as a linear equivalence.
Instances For
ℍ[R, c₁, c₂]
has a basis over R
given by 1
, i
, j
, and k
.
Instances For
Quaternion conjugate.
Quaternion conjugate as an AlgEquiv
to the opposite ring.
Instances For
The equivalence between the quaternions over R
and R × R × R × R
.
Instances For
The equivalence between the quaternions over R
and Fin 4 → R
.
Instances For
Coercion R → ℍ[R]
.
Instances For
The imaginary part of a quaternion.
Instances For
Quaternion conjugate as an AlgEquiv
to the opposite ring.
Instances For
Square of the norm.
Instances For
The cardinality of a quaternion algebra, as a type.
The cardinality of a quaternion algebra, as a set.
The cardinality of the quaternions, as a type.
The cardinality of the quaternions, as a set.