This repository contains the proof that the adele ring of a number field is locally compact, formalised in Lean 4.7.0 using Mathlib's version eaede86.
That the adele ring of a number field is locally compact is one of the motivators for defining the adele ring using the restricted direct product over all completions, rather than just the usual direct product. Moreover, this allows one to do harmonic analysis over the subgroup of units of the adele ring which was done in Tate's landmark thesis, a precursor to the Langlands program.
This work follows on from prior work of Maria Inés de Frutos-Fernández, who first formalised the definition of the adele ring of a global field here, some of which has been ported to Mathlib's version eaede86, and we also use some results from their recent work with Filippo A. E. Nuccio here, namely we port some foundational results on discrete valuations.
Let
Let
The direct product of completions of
The infinite adele ring is given as the (finite) direct product of the real/complex completions of
The adele ring of
Suppose now that
For
Let
The local compactness of the finite adele ring is difficult to show directly. Instead, we note that it suffices to cover
The infinite adele ring
The adele ring is locally compact because it is the direct product of the infinite and finite adele rings, each of which have been shown to be locally compact.
The high-level code structure is modelled after the structure of Mathlib version eaede86. In line with the above proof overview, we break down the specific location of results in the various files.
The proofs that
- The result that
$O_v$ is compact is here.
- The result that
$K_v$ is locally compact for finite places$v$ is given in AdeleRingLocallyCompact/RingTheory/DedekindDomain/AdicValuation.lean, specifically here.
- The topology of the finite adele ring and other related definitions are found in AdeleRingLocallyCompact/RingTheory/DedekindDomain/FiniteAdeleRing.lean.
- The definition of the finite
$S$ -adele ring and the proof that it is locally compact can be found in AdeleRingLocallyCompact/RingTheory/DedekindDomain/FiniteSAdeleRing.lean, respectively here and here. - The proof that the finite adele ring is locally compact can also be found in AdeleRingLocallyCompact/RingTheory/DedekindDomain/FiniteSAdeleRing.lean, specifically here.
- The completion of a number field at the infinite places is formalised in AdeleRingLocallyCompact/NumberTheory/NumberField/Embeddings.lean. The definition is here and the proof it is locally compact is here.
- The definition, topology and local compactness of the infinite adele ring are found in AdeleRingLocallyCompact/NumberTheory/NumberField/InfiniteAdeleRing.lean.
- The definition and local compactness of the adele ring are found in AdeleRingLocallyCompact/NumberTheory/NumberField/AdeleRing.lean.
We collect some implementation notes and describe the Lean proof of the local compactness of the finite
-
AdeleRingLocallyCompact/RingTheory/DedekindDomain/AdicValuation.lean currently contains some results that have been adapted from prior work (M.I. de Frutos-Fernández, F.A.E. Nuccio, A Formalization of Complete Discrete Valuation Rings and Local Fields) into Lean 4. One result remains unproven, which is the finiteness of the residue field of
$O_v$ . This also appears in (M.I. de Frutos-Fernández, F.A.E. Nuccio, A Formalization of Complete Discrete Valuation Rings and Local Fields). Once these results are available in Mathlib these will be updated accordingly. - The finite
$S$ -adele ring is formalised as a subring of$\widehat{K}$ , in an analogous way to the formalisation of$\mathbb{A}_{K, f}$ . It is given the subspace topology of$\mathbb{A}_{K, f}$ by inducing along the open embedding$\mathbb{A}_{S, K, f} \hookrightarrow \mathbb{A}_{K, f}$ . This is the same as the topology obtained as a subtype of$\widehat{K}$ . - The equivalence and homeomorphism between
$\widehat{K}$ and$\widehat{K}_S$ are given, respectively, by Mathlib'sEquiv.piEquivPiSubtypeProd
andHomeomorph.piEquivPiSubtypeProd
. - The above homeomorphism then descends to a homeomorphism
$\mathbb{A}_{S, K, f}\cong \prod_{v\in S} K_v \times \prod_{v\notin S} O_v$ , when the right-hand side is seen as a subtype of$\widehat{K}_S$ . - There is a homeomorphism between
$\prod_{v\in S} K_v \times \prod_{v\notin S} O_v$ when viewed as a subtype of$\widehat{K}_S$ vs. when it is defined as a topological space in its own right (i.e., with product topology). It is easy to show that the latter is locally compact using standard locally compact product results. - This chain of homeomorphisms gives the proof of the local compactness of
$\mathbb{A}_{S, K, f}$ .
- Incorporate the proof that
v.adicCompletionIntegers K
has finite residue field. - v2.0 : Show that
$K$ is a discrete and cocompact subgroup of the additive group of$\mathbb{A}_K$ .- Define the adelic norm.
- Prove the product formula for global adeles: if
$x \in K \subseteq \mathbb{A}_K$ then$|x| = 1$ . - This is enough to show that
$K$ is a discrete subgroup. - Prove base change for adele rings : if
$K/L$ then$\mathbb{A}_L = \mathbb{A}_K\otimes_K L$ . - Helper result: for all finite places
$v$ , if$y \in K_v$ then there exists$x \in K$ such that$|y - x|_v\le 1$ and$|x|_w \le 1$ for all$w \ne v$ . - This is enough to show that
$\mathbb{A}_{\mathbb{Q}}/\mathbb{Q}$ is compact, since it's the continuous image of the compact set$\{x \in \mathbb{A}_{\mathbb{Q}}\mid \forall v, |x|_v \le 1\}$ . Then use base change for general$K$ .
- v3.0 : Show the idele group is locally compact. Probably requires refactoring the current code as follows.
- Define
ProdAdicCompletions.IsRestrictedProduct (X : Subring (ProdAdicCompletions R K) (U : v \\to (Subring (v.adicCompletion K))))
- Refactor the current proof of local compactness of adele ring to show that
ProdAdicCompletions.IsRestrictedProduct
is locally compact (requires the assumption thatU v
are all compact). - Then local compactness of finite adele ring follows immediateley with
U v = v.adicCompletionIntegers K
- Define idele ring as group of units with unit topology.
- Show this is
IsRestrictedProduct
whereU v = (v.adicCompletionIntegers K)^*
, therefore locally compact.
- Define