Papers With

← All papers
First page of Formalizing the Ring of Adeles of a Global Field

Formalizing the Ring of Adeles of a Global Field

María Inés de Frutos-Fernández

cs.LO Mar 6, 2022 · v1
formalization mathlib number-theory algebra
Read PDF arXiv abstract
TL;DR
Formalizes adeles, ideles, and adic valuations on Dedekind domains in Lean 3.
Abstract
The ring of adeles of a global field and its group of units, the group of ideles, are fundamental objects in modern number theory. We formalize their definitions in the Lean 3 theorem prover. As a prerequisite, we formalize adic valuations on Dedekind domains. We present applications including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idele class group.
Problem

The ring of adeles and the group of ideles are fundamental objects in algebraic number theory, but they had not been formalized in a theorem prover, limiting the ability to formally state and verify results in global class field theory.

Approach

The paper formalizes the ring of adeles of a global field and the group of ideles in Lean 3. As a prerequisite, it formalizes adic valuations on Dedekind domains. The development builds on mathlib's algebraic infrastructure for number fields, valuations, and completions.

Results

The formalization enables stating the main theorem of global class field theory in Lean. It includes a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idele class group. The prerequisite formalization of adic valuations on Dedekind domains is contributed to the library.