Profinite completion of the Hurwitz quaternions

We define \(\widehat{\mathcal{O}}\) to be \(\mathcal{O}\otimes\widehat{\mathbb{Z}}\), so it's elements \(a+bi+cj+d\omega\) with \(a,b,c,d\in\widehat{\mathbb{Z}}\).

We define \(D:=\mathbb{Q}\otimes\mathcal{O}=\mathbb{Q}\oplus\mathbb{Q} i\oplus\mathbb{Q} j\oplus\mathbb{Q}\omega=\mathbb{Q}\oplus\mathbb{Q} i\oplus\mathbb{Q} j\oplus\mathbb{Q} k\). Finally, we define \(\widehat{D}:=D\otimes\widehat{\mathbb{Z}}\). Just as with \(\widehat{\mathbb{Q}}\) we have

LemmaHurwitzRatHat.canonicalForm#

Every element of \(\widehat{D}\) can be written as \(z/N\) with \(z\in\widehat{\mathcal{O}}\) and \(N\in\mathbb{N}^+\).

Proof

Same as the proof for \(\widehat{\mathbb{Q}}\).

Lean

Stated as HurwitzRatHat.canonicalForm; the blueprint marks no proof of it as formalized.

Sources
LeanHurwitzRatHat.canonicalForm
Uses 3 · Used by 1
Statement usesQHat · ZHat · Hurwitz
Used byHurwitzRatHat.completed_units

It is not hard to check that \(\widehat{D}\) contains \(\widehat{\mathcal{O}}\) and \(D\) as subrings, and that as additive abelian groups we have \(\widehat{\mathcal{O}}\cap D=\mathcal{O}\) and \(\widehat{\mathcal{O}}+D=\widehat{D}\). This is because \(\mathcal{O}\) is just four copies of \(\mathbb{Z}\) and we've proved the analogous result for \(\mathbb{Z}\).

However the multiplicative structure is more interesting, especially as \(D\) is not commutative. For a general quaternion algebra it is not true that \((\widehat{D})^\times=D^\times(\widehat{\mathcal{O}})^\times\), because there are "class group obstructions". The double coset space is some kind of non-commutative analogue of a class group. However for our particular choice of \(D\) and \(\mathcal{O}\) the result is true.

TheoremHurwitzRatHat.completed_units#

The group of units of \(\widehat{D}\) is \(D^\times\widehat{\mathcal{O}}^\times\). More precisely, every element of \(\widehat{D}^\times\) can be written as a product \(\delta u\) with \(\delta\in D^\times\) and \(u\in\widehat{\mathcal{O}}^\times\).

Proof

Given an element \(x\) of \(\widehat{D}^\times\), we can use lemma HurwitzRatHat.canonicalForm to write it as \(z/N\) with \(N\) a positive integer and \(z\in\widehat{\mathcal{O}}\). Note that \(N\) is central and in \(D^\times\). Similarly, we can write \(x^{-1}\) as \(y/M\) with \(M\) a positive integer and \(y\in\widehat{\mathcal{O}}\). Then \(1=xx^{-1}=zy/NM\) and so \(zy=NM=MN\), and \(1=x^{-1}x=yz/MN\) so \(yz=MN\) too. In particular \(y\) both left and right divides a positive integer.

Now consider the left ideal \(\widehat{\mathcal{O}}y\) generated by \(y\). We've just seen that this ideal has nontrivial intersection with \(\mathcal{O}\), because it contains \(MN>0\). Hence its intersection with \(\mathcal{O}\) is a nonzero left ideal of \(\mathcal{O}\), which is hence principal by corollary Hurwitz.left_ideal_princ. Write it as \(\mathcal{O}\alpha\) with \(0\not=\alpha\in\mathcal{O}\).

It suffices to show that \(\widehat{\mathcal{O}}\alpha=\widehat{\mathcal{O}} y\). For this would imply that \(u\alpha=y\) and \(vy=\alpha\) for some \(u,v\in\widehat{\mathcal{O}}\) and thus \((vu-1)\alpha=0\) and \((uv-1)y=0\), and both \(\alpha\) and \(y\) are left divisors of positive integers (the norm of \(\alpha\), and \(MN\) respectively), so now using the fact that \(\widehat{\mathcal{O}}\) is \(\mathbb{Z}\)-torsion-free (is the tensor product of torsion-free abelian groups torsion-free? That would be a cheap way of doing it. Otherwise use \(\mathcal{O}=\mathbb{Z}^4\)) we deduce that \(u\) and \(v\) are units, and thus \(x^{-1}=\frac{1}{M}u\alpha\) so \(x=(M\alpha^{-1})v\in D^\times\widehat{\mathcal{O}}^\times\).

What remains is this. We have \(y\in\widehat{\mathcal{O}}\) which left and right divides some positive integer. We've defined \(0\not=\alpha\in\mathcal{O}\) such that \(\mathcal{O}\alpha\) is the pullback of the abelian group \(\widehat{\mathcal{O}} y\) along the map \(\mathcal{O}\to\widehat{\mathcal{O}}\). We need to show that when we push this ideal \(\mathcal{O}\alpha\) forwards to \(\widehat{\mathcal{O}}\) we get \(\widehat{\mathcal{O}} y\) again. The fact that \(\widehat{\mathcal{O}}\alpha\subseteq\widehat{\mathcal{O}} y\) is easy, because \(\alpha\in\widehat{\mathcal{O}} y\) by definition. So it remains to show that \(y\in\widehat{\mathcal{O}}\alpha\).

Let's define \(T\) to be a positive integer which is both a left and right multiple of both \(y\) and \(\alpha\) (for example \(T=MN\alpha\overline{\alpha}\) will do). Now note that we have an isomorphism \(\mathcal{O}/T\mathcal{O}=\widehat{\mathcal{O}}/T\widehat{\mathcal{O}}\), so we can choose some \(\beta\in\mathcal{O}\) such that \(\beta-y\in T\widehat{\mathcal{O}}\) is a multiple of \(T\). Next note that \(\beta\in y+\widehat{\mathcal{O}} T\subset \widehat{\mathcal{O}} y\) is in \(\widehat{\mathcal{O}} y\cap\mathcal{O}=\mathcal{O}\alpha\), meaning \(\beta=\gamma\alpha\) for some \(\gamma\in\mathcal{O}\). Hence \(y\in\beta+\widehat{\mathcal{O}} T\subseteq\widehat{\mathcal{O}}\alpha\).

Lean

Stated as HurwitzRatHat.completed_units; the blueprint marks no proof of it as formalized.

Sources
LeanHurwitzRatHat.completed_units
Uses 1
Statement usesHurwitzRatHat.canonicalForm

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.