Formalising the local compactness of the adele ring

TL;DR

This paper formalizes the proof of the local compactness of the adele ring of a number field within the Lean 4 theorem prover, including new formalizations of related types and properties.

Contribution

It introduces formal definitions and proofs of local compactness for the adele ring and its components in Lean 4, advancing formal number theory.

Findings

Formal proof of local compactness of the adele ring

Formalizations of completions at infinite and finite places

Proofs that rings of integers at finite places are compact

Abstract

The adele ring of a number field is a central object in modern number theory. Its status as a locally compact topological ring is one of the key reasons why. We describe a formal proof that the adele ring of a number field is locally compact implemented in the Lean 4 theorem prover. Our work includes the formalisations of new types, including the completion of a number field at an infinite place, the infinite adele ring and the finite $S$-adele ring, as well as formal proofs that completions of a number field are locally compact and that their rings of integers at finite places are compact.