LIPIcs.ITP.2022.14.pdf
- Filesize: 0.79 MB
- 18 pages
Document
Formalizing the Ring of Adèles of a Global Field
Author
María Inés de Frutos-Fernández 
-
Part of:
Volume:
13th International Conference on Interactive Theorem Proving (ITP 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-08-03
File
Document Identifiers
Author Details
Acknowledgements
I would like to thank Kevin Buzzard for his constant support and for many helpful conversations during the completion of this project, and Ashvni Narayanan for pointing out that the finite adèle ring can be defined for any Dedekind domain. I am also grateful to Patrick Massot for making some of the topological prerequisites available in mathlib, and to Sebastian Monnet for formalizing the topology on the infinite Galois group. Finally, I thank the mathlib community for their helpful advice, and the mathlib maintainers for the insightful reviews of the parts of this project already submitted to the library.
Cite AsGet BibTex
María Inés de Frutos-Fernández. Formalizing the Ring of Adèles of a Global Field. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.14
https://doi.org/10.4230/LIPIcs.ITP.2022.14
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
- Theory of computation → Type theory
Keywords
- formal math
- algebraic number theory
- class field theory
- Lean
- mathlib
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Emil Artin and John Tate. Class Field Theory. W. A. Benjamin, New York, 1967.
- Emil Artin and George Whaples. Axiomatic Characterization of Fields by the Product Formula for Valuations. Bulletin of the American Mathematical Society, 51(7):469-492, 1945. URL: https://mathscinet.ams.org/mathscinet-getitem?mr=MR0013145.
- Jeremy Avigad, Leonardo de Moura, and Soonho Kong. Theorem Proving in Lean. Carnegie Mellon University, 2021. Release 3.23.0. URL: https://leanprover.github.io/theorem_proving_in_lean/.
- Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.5.
- Daniel Bump. Automorphic Forms and Representations. Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1997. URL: https://doi.org/10.1017/CBO9780511609572.
- Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising Perfectoid Spaces. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 299-312. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373830.
- Mario Carneiro. The Type Theory of Lean. Springer, Berlin, Heidelberg, 2019. Master thesis. URL: https://github.com/digama0/lean-type-theory/releases.
-
J. W. S. Cassels and A. Fröhlich (eds.). Algebraic Number Theory. Academic Press, London; Thompson Book Co., Inc., Washington, D.C., 1967.
- L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean Theorem Prover (System Description). In Felty A. and Middeldorp A., editors, Automated Deduction - CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, Cham, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
-
Gerald J. Janusz. Algebraic Number Fields, volume 55 of Pure and Applied Mathematics. Academic Press, London, 2nd edition, 1996.
- R. P. Langlands. Problems in the Theory of Automorphic Forms. In Lectures in Modern Analysis and Applications III, volume 170 of Lecture Notes in Mathematics, pages 18-61. Springer, Berlin, Heidelberg, 1970. URL: https://doi.org/10.1007/BFb0079065.
- Robert Y. Lewis. A Formal Proof of Hensel’s Lemma over the p-Adic Integers. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 15-26, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294089.
- J. S. Milne. Class Field Theory (v4.03), 2020. URL: https://www.jmilne.org/math/CourseNotes/CFT.pdf.
- Jürgen Neukirch. Algebraic Number Theory. Springer, Berlin, Heidelberg, 1999. URL: https://doi.org/10.1007/978-3-662-03983-0.
- Álvaro Pelayo, Vladimir Voevodsky, and Michael A. Warren. A univalent formalization of the p-adic numbers. Mathematical Structures in Computer Science, 25(5):1147-1171, 2015. URL: https://doi.org/10.1017/S0960129514000541.
- Henning Stichtenoth. Algebraic Function Fields and Codes. Universitext. Springer, 1993. URL: https://dblp.org/rec/books/daglib/0084861.
- Floris van Doorn. Formalized Haar Measure. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:17, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.18.