Rational Hurwitz integers map into the real model

Proved

HurwitzQ.lift_mem_hurwitzIntegers

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$ . Let $\iota$ apply the canonical inclusion $\mathbb{Q}\hookrightarrow\mathbb{R}$ to each quaternion coordinate, and let $\mathcal{H}_{\mathbb{R}}$ be the real-quaternion subring defined by the same coordinate condition. Let $q$ be a rational quaternion.

q\in\mathcal{H}\implies\iota(q)\in\mathcal{H}_{\mathbb{R}}.

This connects the rational and real realizations of the Hurwitz integers.

Preamble

import Definitions.Def_HurwitzQ_hurwitzIntegersQ
import Definitions.Def_Quaternion_hurwitzIntegers
import Definitions.Def_Quaternion_lipschitzIntegers
import Mathlib.Algebra.Quaternion
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring

open Quaternion QuaternionAlgebra HurwitzQ

Formal statement

theorem HurwitzQ.lift_mem_hurwitzIntegers {q : ℍ[ℚ]} (hq : q ∈ hurwitzIntegersQ) :
    (⟨(q.re : ℝ), (q.imI : ℝ), (q.imJ : ℝ), (q.imK : ℝ)⟩ : ℍ[ℝ]) ∈ hurwitzIntegers := 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