License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.14
URN: urn:nbn:de:0030-drops-167232
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16723/
de Frutos-Fernández, María Inés
Formalizing the Ring of Adèles of a Global Field
Abstract
The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalize adic valuations on Dedekind domains. We present some 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 idèle class group.
BibTeX - Entry
@InProceedings{defrutosfernandez:LIPIcs.ITP.2022.14,
author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16723},
URN = {urn:nbn:de:0030-drops-167232},
doi = {10.4230/LIPIcs.ITP.2022.14},
annote = {Keywords: formal math, algebraic number theory, class field theory, Lean, mathlib}
}
