smmercuriadele-ring_locally-compact

The proof that the adele ring of a number field is locally compact, formalised in Lean 4.

Local Compactness of the Adele Ring of a Number Field

This repository contains the proof that the adele ring of a number field is locally compact, formalised in Lean 4.10.0 using Mathlib's version caac5b1.

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.

Overview of the proof

Introduction

Let be an algebraic number field over and let be its ring of integers, which is a Dedekind domain of Krull dimension . By the extension of Ostrowski's theorem to number fields any valuation on is equivalent to some -adic valuation on or an absolute value arising from the real and complex embeddings of . Equivalence classes of valuations on are known as places. Thus places of are indexed by the real/complex embeddings of and by the primes of ; the former are called the infinite places and the latter the finite places.

Let be a place of , then we denote by the completion of with respect to some representative valuation of the place . The place extends naturally to a place on , which we denote by . The integral closure of inside is called the (-adic) ring of integers and is denoted ; this corresponds to the ring of all such that .

The direct product of completions of at finite places is denoted

This product is not locally compact, given the product topology. On the other hand, we define the finite adele ring as the restricted direct product

with basis of open sets

Missing \left or extra \right\left\\{ \prod\_{v\ \text{finite}} V\_v \mathrel{\bigg|} V\_v \subseteq K\_v\ \text{open and}\ V\_v = \mathcal{O}\_v\ \text{for all but finitely many}\ v\right\\}.

We will prove below that is locally compact.

The infinite adele ring is given as the (finite) direct product of the real/complex completions of at the real/complex places

The adele ring of is then given as the product of the infinite and finite adele rings:

Compactness of

Suppose now that is a finite place. A crucial result that will play a role later is that the -adic ring of integers is compact. It suffices to show that is complete and totally bounded. For completeness, we show that it is closed, which can be proven in a similar way to the proof that it is open. Indeed, since the valuation is discrete, any open set is also closed. Since is a closed set in a complete space, it is also complete.

For to be totally bounded means that for some fixed radius > 0, we can cover with finitely many open balls of radius . It suffices to check this for . Each such corresponds to some integer in the sense that the ball of radius is equal to the ball of radius , where generates the unique maximal ideal of . We note also that the residue field is finite. For any , is therefore also finite as it can be viewed as copies of . Hence, for a fixed , we take the finitely-many representatives from and it can be checked that the balls centred at these representatives of radius form a finite cover of . This completes the proof that is compact.

Local compactness of

It is enough to show that has a compact neighbourhood, because we can translate and dilate/shrink this neighbourhood to be contained in a neighbourhood of any other point. The maximal ideal is a clopen subset of the compact space , so it is a compact neighbourhood of .

Local compactness of

The local compactness of the finite adele ring is difficult to show directly. Instead, we note that it suffices to cover with open and locally compact subsets. Then any neighbourhood of contains a compact neighbourhood by intersecting with the compact neighbourhood containing obtained from one of the locally compact subsets. To achieve this we use the finite -adele ring , where is some finite set of finite places, defined by

This clearly belongs to the basis of open sets for , hence it is open. Moreover, through the map , it is homeomorphic to

which is locally compact as is a finite product of locally compact spaces and is an infinite product of compact spaces. Therefore is locally compact as well. Finally, the finite -adele rings cover since , where is the (finitely-many) places such that .

Local compactness of

The infinite adele ring is locally compact because it is a finite product of the completions , where is an infinite place, each of which are locally compact.

Local compactness of

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.

Overview of the code

The high-level code structure is modelled after the structure of Mathlib version caac5b1. In line with the above proof overview, we break down the specific location of results in the various files.

Compactness of

The proofs that is totally bounded, complete, and therefore compact can be found in RingTheory.DedekindDomain.AdicValuation.

Local compactness of

Local compactness of

Local compactness of

Local compactness of

Implementation notes

We collect some implementation notes and describe the Lean proof of the local compactness of the finite -adele ring here.

  • FromLocalClassFieldTheory.LocalClassFieldTheory 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 in our work is the finiteness of the residue field of . This also appears in (M.I. de Frutos-Fernández, F.A.E. Nuccio, A Formalization of Complete Discrete Valuation Rings and Local Fields).
  • The finite -adele ring is formalised as a subtype of , in an analogous way to the formalisation of . This gets the subspace topology of .
  • The equivalence and homeomorphism between and are given, respectively, by Mathlib's Equiv.piEquivPiSubtypeProd and Homeomorph.piEquivPiSubtypeProd. This homeomorphism then descends to a homeomorphism , when the right-hand side is seen as a subtype of .
  • There is a homeomorphism between when viewed as a subtype of 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 .
  • Lean always expects a single instance of a class on a type. A number field, however, has multiple distinct uniform structures coming from infinite places. To handle this ambiguity, we use a dependent type synonym WithAbs, which simply renames a semiring and makes it depend on absolute values. When v is an infinite place on K, we can instead view K as WithAbs v.1. This allows the type class inference system to automatically infer any assigned instances that depend on absolute values.

TODOs

  • Incorporate the proof that v.adicCompletionIntegers K has finite residue field.
  • v2.0 : Show that is a discrete and cocompact subgroup of the additive group of .
    • Define the adelic norm.
    • Prove the product formula for global adeles: if then .
    • This is enough to show that is a discrete subgroup.
    • Prove base change for adele rings : if then .
    • Helper result: for all finite places , if then there exists such that and for all .
    • This is enough to show that is compact, since it's the continuous image of the compact set . Then use base change for general .
  • 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 that U 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 where U v = (v.adicCompletionIntegers K)^*, therefore locally compact.