The Hurwitz ring is generated by the quaternion units and omega

Proved

HurwitzQ.hurwitzIntegersQ_eq_closure

by jawneeboy · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebrahurwitz-integersnumber-theoryquaternions

Let $\mathcal{H}$ be the Hurwitz subring of the rational quaternions: the four coordinates of an element are either all in $\mathbb{Z}$ or all in $\mathbb{Z}+\frac12$ . Put $\omega=(1+i+j+k)/2$ , where $i,j,k$ are the standard quaternion units.

\mathcal{H}=\mathbb{Z}[i,j,k,\omega].

This identifies the coordinate-defined subring with the smallest subring containing the four displayed generators.

Preamble

import Definitions.Def_HurwitzQ_hurwitzIntegersQ
import Definitions.Def_HurwitzQ_omega
import Mathlib.Algebra.Quaternion
import Mathlib.Algebra.QuaternionBasis
import Mathlib.Algebra.Ring.Subring.Basic
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring

open Quaternion QuaternionAlgebra HurwitzQ

Formal statement

theorem HurwitzQ.hurwitzIntegersQ_eq_closure :
    hurwitzIntegersQ =
      Subring.closure {((Basis.self ℚ).i : ℍ[ℚ]), (Basis.self ℚ).j, (Basis.self ℚ).k, omega} := by sorry

Source

Standard definition: John H. Conway and Derek A. Smith, On Quaternions and Octonions: Their Geometry, Arithmetic, and Symmetry, A K Peters, 2003, §5.1, The Hurwitz Integral Quaternions. https://www.routledge.com/On-Quaternions-and-Octonions/Conway-Smith/p/book/9781568811345 The displayed assertion is an elementary consequence of this definition; no numbered theorem attribution is claimed.

View graph