Multiplicative structure of the units of \(\widehat{\mathbb{Q}}\).

We now forget the additive structure on the commutative ring \(\widehat{\mathbb{Q}}\) and consider the multiplicative structure of its group of units \(\widehat{\mathbb{Q}}^\times\) (which I couldn't get into the section title). We have the obvious subgroups \(\mathbb{Q}^\times\), \(\mathbb{Z}^\times\) and \(\widehat{\mathbb{Z}}^\times\).

LemmaQhat.unitsrat_meet_unitszHat#

The intersection of \(\mathbb{Q}^\times\) and \(\widehat{\mathbb{Z}}^\times\) in \(\widehat{\mathbb{Q}}^\times\) is \(\mathbb{Z}^\times\).

Proof

Clearly the intersection is contained within \(\mathbb{Q}\cap\widehat{\mathbb{Z}}=\mathbb{Z}\). If \(n\in\mathbb{Z}\) is in \(\widehat{\mathbb{Z}}^\times\) then \(n\not=0\) and its inverse \(1/n=\pm1/|n|\) is in lowest terms but also in \(\widehat{\mathbb{Z}}\), and hence \(|n|=1\) by uniqueness of lowest term representation.

Lean

Formalized as QHat.unitsrat_meet_unitszHat.

Sources
LeanQHat.unitsrat_meet_unitszHat
Uses 4
Statement usesQHat · ZHat.commRing
Proof usesQHat.lowestTerms · QHat.rat_meet_zHat

LemmaQHat.unitsrat_join_unitszHat#

The product of \(\mathbb{Q}^\times\) and \(\widehat{\mathbb{Z}}^\times\) in \(\widehat{\mathbb{Q}}^\times\) is all of \(\widehat{\mathbb{Q}}^\times\). More precisely, every element of \(\widehat{\mathbb{Q}}^\times\) can be written as \(qz\) with \(q\in\mathbb{Q}^\times\) and \(z\in\widehat{\mathbb{Z}}^\times\).

Proof

We already know that a general element of \(\widehat{\mathbb{Q}}^\times\) can be written as \(x/N\) with \(N\) positive, so this reduces us to proving that a general element \(x\in\widehat{\mathbb{Z}}\) which is invertible in \(\widehat{\mathbb{Q}}^\times\) can be written as \(qz\) with \(q\in\mathbb{Q}^\times\) and \(z\in\widehat{\mathbb{Z}}^\times\).

We know \(1/x\) can be written in lowest terms as \(y/M\), and multiplying up we deduce that \(xy=M\), and hence \(x\) divides a positive integer. If \(i:\mathbb{Z}\to\widehat{\mathbb{Z}}\) denotes the inclusion, then we've just seen that the preimage of the principal ideal \((x)\), namely, \(J:=i^{-1}(x\widehat{\mathbb{Z}})\) is nonzero, as it contains \(M\). Let \(g\in J\) be the smallest positive integer; it's well-known that \(J=(g)\).

I claim that it suffices to show that \(x\widehat{\mathbb{Z}}=g\widehat{\mathbb{Z}}\). Because knowing \(g=yx\) and \(x=gz\) for some \(y,z\in\widehat{\mathbb{Z}}\) tells us that \(g(1-yz)=0\), and we know that multiplication by \(g\) is injective, hence \(yz=1\), so \(z\) is a unit and we have written \(x=gz\) with \(g\in\mathbb{Q}^\times\) and \(z\in\widehat{\mathbb{Z}}^\times\).

It remains to prove the claim. By definition \(g\in J\subseteq x\widehat{\mathbb{Z}}\) so this is one inclusion. For the other, it suffices to prove that \(x_g=0\). However if \(0\lt x_g\lt g\) lifts \(x_g\) to the naturals then I claim that \(x_g\in J\), for \(x_g-x\) is a multiple of \(g\) and hence of \(x\), and this contradicts minimality of \(g\).

Lean

Formalized as QHat.unitsrat_join_unitszHat.

Sources
LeanQHat.unitsrat_join_unitszHat
Uses 4
Statement usesQHat · ZHat.commRing
Proof usesZHat.multiples · QHat.canonicalForm

Note that by the previous lemma, this representation will be unique up to sign.

The proof of Lemma QHat.unitsrat_join_unitszHat is shown with its statement.

We are nearly ready to embark upon the multiplicative adelic theory for quaternion algebras. However before we do this, we need to develop the theory of the Hurwitz quaternions a bit more formally.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.