8 Miniproject: Adeles

8.1 Status

This is an active miniproject.

8.2 The goal

At the time of writing, mathlib does not have a definition of the adeles of a number field. There are several goals to this miniproject.

• Define the adeles \(\mathbb {A}_K\) of a number field \(K\) and give them the structure of a \(K\)-algebra;

• Prove that \(\mathbb {A}_K\) is a locally compact topological ring;

• Show that if \(L/K\) is a finite extension of number fields then the natural map \(L\otimes _K\mathbb {A}_K\to \mathbb {A}_L\) is an isomorphism;

• Prove that \(K \subseteq \mathbb {A}_K\) is a discrete subgoup and the quotient is compact.

We briefly go through the basic definitions. A cheap definition of the finite adeles \(\mathbb {A}_K^\infty \) of \(K\) is \(K\otimes _{\mathbb {Z}}\widehat{\mathbb {Z}}\), where \(\widehat{\mathbb {Z}}\) is the profinite completion of the integers. A cheap definition of the infinite adeles \(K_\infty \) of \(K\) is \(K\otimes _{\mathbb {Q}}\mathbb {R}\), and a cheap definition of the adeles of \(K\) is \(\mathbb {A}_K^\infty \times K_\infty \). However in the literature different definitions are often given. The finite adeles of \(K\) are usually defined as the so-called restricted product \(\prod '_{\mathfrak {p}}K_{\mathfrak {p}}\) over the completions \(K_{\mathfrak {p}}\) of \(K\) at all maximal ideals \(\mathfrak {p}\subseteq \mathcal{O}_K\) of the integers of \(K\). Here the restricted product is the subset of \(\prod _{\mathfrak {p}}K_{\mathfrak {p}}\) consisting of elements which are in \(\mathcal{O}_{K,\mathfrak {p}}\) for all but finitely many \(\mathfrak {p}\). Mathlib already has the finite adeles and the proof that they’re a topological ring; in fact the construction in mathlib works for any Dedekind domain.

Similarly the infinite adeles of a number field are usually defined as \(\prod _v K_v\), the product running over the archimedean completions of \(K\).

8.3 Current status

Salvatore Mercuri has made great progress with the definition of \(\mathbb {A}_K\) and he even has a complete formalisation of the proof that the adele ring is locally compact. His work is in his own repo which I don’t want to have as a dependency of FLT, because this work should all be in mathlib. We quote some of it here.

8.4 Results about adeles of a number field that we await

Let \(K\) be a number field. Right now mathlib has the finite adeles \(\mathbb {A}_K^\infty \) of \(K\), with its topological ring structure. It does not however have the infinite adeles \(K_\infty \). There are PRs by Salvatore Mercuri currently in progress for defining this topological ring. Once we have it, the full ring of adeles \(\mathbb {A}_K\) is defined as \(\mathbb {A}_K:=\mathbb {A}_K^\infty \times K_\infty \); it is a topological ring and also a \(K\)-algebra. Once Mercuri’s mathlib PR 16485 is merged, we will have all this available to us; until then, we sorry the definitions and these facts.

Mercuri’s work isn’t however enough for us; we also need several theorems about this topological \(K\)-algebra. These lemmas are essentially impossible to work on until we have the definition in mathlib. We state them here without proof.

Mercuri has already proved local compactness in his repo. As far as I know, the other two theorems remain unformalised (but as I’ve mentioned, we cannot start on them until we have a definition of the adele ring in this project, and I would prefer that this were achieved by upstreaming Mercuri’s work to mathlib).

However, there is something that we can do here even before Mercuri’s work is upstreamed: one proof I know that of discreteness and cocompactness of \(K\) in \(\mathbb {A}_K\) reduces to the case \(K=\mathbb {Q}\), using the “canonical” isomorphism \(\mathbb {A}_K\cong \mathbb {A}_{\mathbb {Q}}\otimes _{\mathbb {Q}}K\). This can be proved by checking it for finite and infinite adeles separately, so one thing which we can work on now is the finite case. We explain this in the next section.

8.5 Results about finite adeles which we can work on now

Adeles are arithmetic objects, attached to global fields like number fields. However (as I learnt from Maria Ines de Frutos Fernandez) finite adeles are algebraic objects, as they can be attached to any Dedekind domain. The “theorem” that we need is the following:

Of course, this isn’t a theorem; this is actually a definition (the map) and a theorem about the definition (that it’s an isomorphism). Before we can prove the theorem, we need to make the definition.

If \(A\) is a Dedekind domain then the height one spectrum of \(A\) is the nonzero prime ideals of \(A\). Note that because we stick to the literature, rather than to common sense, fields are Dedekind domains in mathlib, and the height one spectrum of a field is empty. The reason I don’t like allowing fields to be Dedekind domain is that geometrically the standard definition of Dedekind domain is “smooth affine curve, or a point”. But many theorems in algebraic geometry begin “let \(C\) be a smooth curve”.

There are two steps to the definition of the map; the first is to define it locally on the individual completions and the second is to glue everything together. Let’s start with the local construction.

Say we’re in the AKLB setup above, with \(L/K\) a finite separable extension. Let \(w\) be a finite place of \(L\) lying above a finite place \(v\) of \(K\). We put the \(w\)-adic topology on \(L\) and the \(v\)-adic topology on \(K\). We now claim that inclusion \(i:K\to L\) is continuous with respect to these topologies. This claim follows from

Note: the formalization right now only claims that the map is a \(K\)-algebra homomorphism, not the continuity. Do we have continuous \(K\)-algebra maps?

We can take the product of all of these maps.

One then has to check that for good primes everything works on an integral level,

Note that the finite adeles do not have the subspace topology, so one has to be slightly careful here.