The Hurwitz quaternions
DefinitionHurwitz#
The Hurwitz quaternions are the set \(\mathcal{O} := \mathbb{Z}\oplus\mathbb{Z} \omega\oplus\mathbb{Z} i\oplus \mathbb{Z} i\omega\) (as an abstract abelian group or as a subgroup of the usual quaternions). Here \(\omega=\frac{-1+(i+j+k)}{2}\) and note that \((i+j+k)^2=-3\). We have \(\overline{\omega}=\omega^2=-(\omega+1)\). A general quaternion \(a+bi+cj+dk\) is a Hurwitz quaternion if either \(a,b,c,d\in\mathbb{Z}\) or \(a,b,c,d\in\mathbb{Z}+\frac{1}{2}\).
Used by 3
LemmaHurwitz.ring#
The Hurwitz quaternions form a ring.
Uses 1 · Used by 1
This ring is isomorphic to \(\mathbb{Z}^4\) as an additive group, and \(\mathcal{O}\otimes_{\mathbb{Z}}\mathbb{R}=\mathbb{R}\oplus \mathbb{R} i\oplus \mathbb{R} j\oplus\mathbb{R} \omega\) is the usual Hamilton quaternions.
DefinitionHurwitz.starRing#
There's a conjugation map (which we'll call "star") from the Hurwitz quaternions to themselves, sending integers to themselves and purely imaginary elements like \(2\omega+1\) to minus themselves. It satisfies \((x^*)^*=x\), \((xy)^*=y^*x^*\) and \((x+y)^*=x^*+y^*\). In particular, the Hurwitz quaternions are a "star ring" in the sense of mathlib.
Uses 1 · Used by 1
DefinitionHurwitz.norm#
The Hurwitz quaternions come equipped with an integer-valued norm, which is \(a^2+b^2+c^2+d^2\) on \(a+bi+cj+dk\) but needs to be modified a bit to deal with \(\omega\).
Uses 1 · Used by 9
LemmaHurwitz.norm_eq_mul_conj#
We have \(N(x)=x\overline{x}\).
Uses 2
LemmaHurwitz.norm_zero#
The norm of \(0\) is \(0\).
Uses 1
LemmaHurwitz.norm_one#
The norm of \(1\) is \(1\).
Uses 1
LemmaHurwitz.norm_mul#
The norm of a product is the product of the norms.
Uses 1
LemmaHurwitz.norm_nonneg#
The norm of an element is nonnegative.
Proof
It's a sum of rational squares.
Lean
Formalized as Hurwitz.norm_nonneg.
Sources
Uses 1
LemmaHurwitz.norm_eq_zero#
The norm of an element is zero if and only if the element is zero.
Proof
It's a sum of rational squares.
Lean
Formalized as Hurwitz.norm_eq_zero.
Sources
Uses 1
LemmaHurwitz.exists_near#
Given a “usual” quaternion \(a=x+yi+zj+wk\) with \(x,y,z,w\in\mathbb{R}\), there exists a Hurwitz quaternion \(q\) such that \(N(a-q)<1\).
Proof
If \([r]\) denotes the nearest integer to the real number \(r\), then \(|r-[r]|\leq \frac{1}{2}\). Hence if \(q=[x]+[y]i+[z]j+[w]k\) then \(N(a-q)=|x-[x]|^2+\cdots \leq \frac{1}{4}+\frac{1}{4}+\frac{1}{4}+\frac{1}{4}\leq 1\), with strict inequality unless \(|x-[x]|=|y-[y]|=|z-[z]|=|w-[w]|=\frac{1}{2}\), in which case \(a\in\mathcal{O}\) because \(a-\omega\) has integer coordinates.
Lean
Formalized as Hurwitz.exists_near.
Sources
Uses 1 · Used by 1
LemmaHurwitz.quot_rem#
Given two Hurwitz quaternions \(a\) and \(b\) with \(b\) nonzero, there exists \(q\) and \(r\) such that \(a=qb+r\) and \(N(r)\lt N(b)\).
Proof
Let \(q\) be the Hurwitz quaternion obtained by applying Lemma Hurwitz.exists_near to \(a/b := ab^{-1}\); then \(N(a/b-q)<1\) and now everything follows after multiplying up.
Lean
Formalized as Hurwitz.quot_rem.
Sources
Uses 2 · Used by 1
CorollaryHurwitz.left_ideal_princ#
All left ideals of \(\mathcal{O}\) are principal.
Proof
If the ideal is 0, use 0. Otherwise, choose a nonzero element of smallest norm.
Lean
Formalized as Hurwitz.left_ideal_princ.
Sources
Uses 2
Remark. All right ideals are principal too, because there's another version of Euclid saying \(a=bq+r\).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.