ℚ⊗ O is a quaternion division algebra with centre ℚ

Let $O$ be a ring which is a domain (no zero divisors, and nontrivial), free and finite as a $\mathbb{Z}$-module, with $\operatorname{finrank}_{\mathbb{Z}} O = 4$, and let $\ell$ be a prime such that there exists an isomorphism of $\mathbb{Z}_{\ell}$-algebras $\mathbb{Z}_{\ell}\otimes_{\mathbb{Z}} O \cong M_2(\mathbb{Z}_{\ell})$ (the hypothesis is the nonemptiness of the type of such AlgEquivs, so no particular isomorphism is named). Then the $\mathbb{Q}$-algebra $D := \mathbb{Q}\otimes_{\mathbb{Z}} O$ satisfies three assertions simultaneously: first, $\operatorname{finrank}_{\mathbb{Q}} D = 4$; second, every nonzero $x \in D$ is a unit of $D$, i.e. $D$ is a division ring; and third, every $z \in D$ commuting with all $x \in D$ (that is, $z x = x z$ for all $x$) lies in the range of the structure map $\mathbb{Q} \to D$, so the centre of $D$ is no larger than the image of $\mathbb{Q}$. Non-commutativity of $D$ is not part of the conclusion; the third clause is the one-sided inclusion $Z(D) \subseteq \mathbb{Q}\cdot 1$.

This is the recognition step saying that a rank-four $\mathbb{Z}$-order without zero divisors having one matrix completion rationalises to a quaternion algebra over $\mathbb{Q}$: a four-dimensional central division algebra over $\mathbb{Q}$. It feeds the construction of definite quaternion algebras ramified exactly at a prescribed set of places together with a maximal order, used further on in the argument.