Additive structure of \(\widehat{\mathbb{Q}}\).

Here we forget the ring structure on everything, and analyse \(\widehat{\mathbb{Q}}\) as an additive abelian group, and in particular how the subgroups \(\mathbb{Z}\), \(\mathbb{Q}\) and \(\widehat{\mathbb{Z}}\) sit within it.

The two results we prove in this section are that \(\mathbb{Q}\cap\widehat{\mathbb{Z}}=\mathbb{Z}\) and that \(\mathbb{Q}+\widehat{\mathbb{Z}}=\widehat{\mathbb{Q}}\). Using lattice-theoretic notation we could write these results as \(\mathbb{Q}\sqcap\widehat{\mathbb{Z}}=\mathbb{Z}\) and \(\mathbb{Q}\sqcup\widehat{\mathbb{Z}}=\widehat{\mathbb{Q}}\).

LemmaQHat.rat_meet_zHat #

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

Proof

Clearly \(\mathbb{Z}\subseteq\mathbb{Q}\cap\widehat{\mathbb{Z}}\). Now suppose that \(x\in\mathbb{Q}\cap\widehat{\mathbb{Z}}\). Because \(x\) is rational we can write it as \(\frac{A}{B}\otimes_t1\) for some fraction \(A/B\) in lowest terms, and hence \(x=A/B\) where now we regard \(A\in\widehat{\mathbb{Z}}\) and note that \(A/B\) is still in lowest terms. However \(x\in\widehat{\mathbb{Z}}\) implies that \(x=x/1\) is in lowest terms, so we deduce that \(B=1\) and thus \(x=A\in\mathbb{Z}\).

Lean

Formalized as QHat.rat_meet_zHat.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/ch05automorphicformexample.tex, line 448

LeanQHat.rat_meet_zHat

Uses 3 · Used by 1

Statement usesQHat · ZHat.commRing

Proof usesQHat.lowestTerms

Used byQhat.unitsrat_meet_unitszHat

LemmaQHat.rat_join_zHat #

The sum of \(\mathbb{Q}\) and \(\widehat{\mathbb{Z}}\) in \(\widehat{\mathbb{Q}}\) is \(\widehat{\mathbb{Q}}\). More precisely, every element of \(\widehat{\mathbb{Q}}\) can be written as \(q+z\) with \(q\in\mathbb{Q}\) and \(z\in\widehat{\mathbb{Z}}\), or more precisely as \(q\otimes_t 1+1\otimes_t z\).

Proof

Write \(x\in\widehat{\mathbb{Q}}\) as \(x=z/N\) in lowest terms. Lift \(z_N\) to an integer \(t\) and observe that \((z-t)_N=0\), hence \(z-t=Ny\) for some \(y\in\widehat{\mathbb{Z}}\). Now \(x=t/N+y\in\mathbb{Q}+\widehat{\mathbb{Z}}\).