Four-dimensional central division ℚ-algebras are quaternion algebras

Let $D$ be a ring equipped with a $\mathbb{Q}$-algebra structure, subject to three hypotheses: $D$ has dimension $4$ as a $\mathbb{Q}$-vector space; every nonzero element of $D$ is a unit; and every element $z$ of $D$ that commutes with all elements of $D$ lies in the image of the structure map $\mathbb{Q} \to D$, i.e. the centre of $D$ is no larger than $\mathbb{Q}$. The conclusion is that there exist rational numbers $a$ and $b$, both nonzero, together with an isomorphism of $\mathbb{Q}$-algebras between $D$ and the quaternion algebra $\mathbb{H}[\mathbb{Q}, a, b]$, that is, the $\mathbb{Q}$-algebra with basis $1, i, j, ij$ and relations $i^2 = a$, $j^2 = b$, $ji = -ij$. The existence of the isomorphism is recorded as the nonemptiness of the type of $\mathbb{Q}$-algebra equivalences $D \simeq_{\mathbb{Q}} \mathbb{H}[\mathbb{Q}, a, b]$, so the statement asserts that some such pair $(a,b)$ of nonzero rationals and some isomorphism exist, without producing them as data.

This is the standard recognition theorem for quaternion algebras: a central division algebra of degree $4$ over a field of characteristic zero is of the form $(a,b)$. It is used in the construction of definite quaternion algebras over $\mathbb{Q}$ ramified exactly at a prescribed set of places, via QuaternionAlgebra.exists_isDefiniteRamifiedExactlyAt_isMaximalOrder_range_eq_of_forall_prime_ne.