Papers With

← All papers
First page of Formalising the local compactness of the adele ring

Formalising the local compactness of the adele ring

Salvatore Mercuri

cs.LO May 29, 2024 · v2
formalization mathlib number-theory algebra
Read PDF arXiv abstract
TL;DR
Formalizes in Lean 4 that the adele ring of a number field is locally 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 for its importance. We describe a formal proof implemented in Lean 4 that the adele ring of a number field is locally compact. This includes 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, along with formal proofs that completions of number fields are locally compact and that their rings of integers at finite places are compact.
Problem

The adele ring of a number field is central in modern number theory, and its local compactness is one of the key reasons for its importance, but this property had not been formally verified.

Approach

The authors implement a formal proof in Lean 4 that the adele ring of a number field is locally compact. This includes formalizations of new types (completions of number fields at infinite places, the infinite adele ring, the finite S-adele ring) along with formal proofs that completions of number fields are locally compact and that their rings of integers at finite places are compact.

Results

A machine-checked proof in Lean 4 establishes that the adele ring of a number field is locally compact. The formalization introduces new types into the Lean ecosystem and verifies the necessary topological properties of completions and rings of integers.