The algebra of real quaternions is the 4-dimensional real vector space \[ \mathbb {H} =\mathbb {R}1\oplus \mathbb {R}i\oplus \mathbb {R}j\oplus \mathbb {R}k. \] Thus every quaternion can be written uniquely as \[ q=a+bi+cj+dk,\qquad a,b,c,d\in \mathbb {R}. \] Addition and real scalar multiplication are coordinatewise. Multiplication is extended bilinearly from \(1\) as the multiplicative identity and the table \[ \begin {gathered} i^2=j^2=k^2=ijk=-1,\\ ij=k,\quad jk=i,\quad ki=j,\\ ji=-k,\quad kj=-i,\quad ik=-j. \end {gathered} \] This makes \(\mathbb {H}\) an associative, noncommutative real algebra. In Voight's notation, \(\mathbb {H}=(-1,-1\mid \mathbb {R})\); see [voight2021quaternion, def. 2.2.1 and ex. 2.2.3].

More generally, when \(F\) is a field of characteristic different from \(2\) and \(a,b\in F^\times \), the symbol \[ (a,b\mid F) \] denotes the quaternion algebra over \(F\) generated by elements \(i,j\) with \[ i^2=a,\qquad j^2=b,\qquad ji=-ij. \] The two slots record the scalars assigned to the squares of the two generators. With \(k=ij\), the elements \(1,i,j,k\) form an \(F\)-basis. Thus the two entries \(-1,-1\) in \((-1,-1\mid \mathbb {R})\) say precisely that \(i^2=-1\) and \(j^2=-1\); the anticommutation relation then gives \(k^2=-1\).

For \(q=a+bi+cj+dk\), its quaternion conjugate and reduced norm are \[ \overline {q}=a-bi-cj-dk,\qquad \operatorname {nrd}(q)=q\overline {q} =a^2+b^2+c^2+d^2. \] We also have \(\overline {q}q=\operatorname {nrd}(q)\). If \(q\ne 0\), then \(\operatorname {nrd}(q)>0\) and \[ q^{-1}=\frac {\overline {q}}{\operatorname {nrd}(q)}. \] So every nonzero quaternion is invertible. This is the standard involution and reduced norm specialized to Hamilton's Quaternions; see [voight2021quaternion, secs. 3.1--3.3].

The corresponding Mathlib type is Quaternion.

Inside the rational quaternion algebra \(B=(-1,-1\mid \mathbb {Q})\), let \(k=ij\) and \[ \omega =\frac {-1+i+j+k}{2}. \] The Lipschitz order and Hurwitz order are the \(\mathbb {Z}\)-lattices \[ \begin {aligned} L&=\mathbb {Z}+\mathbb {Z}i+\mathbb {Z}j+\mathbb {Z}k,\\ \mathcal {O} &=\mathbb {Z}+\mathbb {Z}i+\mathbb {Z}j+\mathbb {Z}\omega . \end {aligned} \] Both are subrings containing \(1\). The order \(\mathcal {O}\) contains \(L\) with index \(2\); it is the unique order properly containing \(L\), and it is maximal. See [voight2021quaternion, sec. 11.1, esp. lem. 11.1.2].

A Hurwitz unit is a unit of \(\mathcal {O}\). Equivalently, it is an element \(q\in \mathcal {O}\) whose reduced norm is \(1\). Voight calculates that \(\mathcal {O}^{\times }\) has \(24\) elements in [voight2021quaternion, sec. 11.2, pp. 166--168]. The particular unit \(\omega \) will give the cyclic factor used below.

Hurwitz developed integral quaternions in 1919. Starting from the Lipschitz order \(L\), the question is not merely which quaternions have integral coordinates, but which order has the better arithmetic structure. The Lipschitz order is not maximal. Voight compares this with enlarging \(\mathbb {Z}[\sqrt {-3}]\) to the Eisenstein integers. Since \(a=i+j+k\) satisfies \(a^2=-3\), the analogous element \[ \omega =\frac {-1+a}{2} \] satisfies \(\omega ^2+\omega +1=0\). Adjoining it enlarges \(L\) to the maximal Hurwitz order \(\mathcal {O}\). See [voight2021quaternion, sec. 11.1, pp. 165--166].

This enlargement supplies more than a convenient lattice. Its \(24\) units form the binary tetrahedral group, and conjugation by \(\omega \) cyclically permutes the quaternion units \(i,j,k\). The same order also supports a norm-Euclidean algorithm. These features make the Hurwitz order a small meeting point of quaternion arithmetic, finite-group structure, and explicit calculation; see [voight2021quaternion, secs. 11.2--11.3, pp. 166--169].

Let \[ a=i+j+k,\qquad \omega =\frac {-1+i+j+k}{2}=\frac {-1+a}{2}. \] Then \(\omega \) is a Hurwitz unit of order \(3\). This choice appears in [voight2021quaternion, p. 165].

The mixed terms in \(a^2\) cancel in pairs: \[ \begin {aligned} a^2 &=i^2+j^2+k^2+(ij+ji)+(jk+kj)+(ki+ik)\\ &=-3. \end {aligned} \] It follows that \[ \begin {aligned} \omega ^2 &=\frac {(-1+a)^2}{4}\\ &=\frac {1-2a+a^2}{4}\\ &=\frac {-1-a}{2}. \end {aligned} \] Hence \(\omega ^2+\omega +1=0\), and multiplication by \(\omega -1\) gives \[ \omega ^3=1. \] Thus \(\omega \) is invertible, has inverse \(\omega ^{-1}=\omega ^2=(-1-i-j-k)/2\), and has order \(3\) because \(\omega \ne 1\).

For a nonzero quaternion \(q\), we use left conjugation to mean \[ q\mathbin {\triangleright }x=qxq^{-1}. \] See the remark on the conjugation calculation for why the direction is recorded explicitly.

Quaternions can also be obtained from suitable Clifford Algebras; see Notes on Clifford Algebras. Here we use the multiplication in Hamilton's Quaternions directly.

Consider left conjugation by the Hurwitz unit \(\omega =(-1+i+j+k)/2\). We have \[ \omega i\omega ^{-1}=k,\qquad \omega j\omega ^{-1}=i,\qquad \omega k\omega ^{-1}=j. \] Thus the cycle is \(i\mapsto k\mapsto j\mapsto i\). Voight says that conjugation cyclically rotates these units in [voight2021quaternion, sec. 11.2.4, p. 168]; the calculation here fixes the direction. Wilson discusses an abstract order-3 automorphism cycling the quaternion generators in [wilson2021finite, sec. 4.3, pp. 12--13, v5]. That discussion does not select the exact quaternion or fix the oriented cycle calculated here.

It is enough to calculate \[ \omega i=k\omega ,\qquad \omega j=i\omega ,\qquad \omega k=j\omega . \] For example, \[ \omega i =\frac {-1-i+j-k}{2} =k\omega . \] Right multiplication by \(\omega ^{-1}\) proves the three conjugation equations.

Saying that conjugation cyclically permutes \(i,j,k\) does not by itself tell us which cycle is meant. Left conjugation by \(\omega \) gives the cycle in the conjugation example. Conjugation by \(\omega ^{-1}\) gives the inverse cycle. This is why we record the three equations instead of only saying "cyclically permutes."

The calculation supplies the first concrete group action used for the binary tetrahedral group. The next notes restrict this action to the quaternion subgroup and then use it in the semidirect-product construction. The three equations alone do not identify the complete set of \(24\) Hurwitz units with that group.

In Lean, the three equations give the computational interface to Mathlib's Quaternion type. The abstract action is then recovered from this concrete calculation.