Document Open Access Logo

Formalizing the Ring of Adèles of a Global Field

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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.14.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Author Details

María Inés de Frutos-Fernández
  • Imperial College London, UK

Funding

EPSRC Grant EP/V048724/1: Digitising the Langlands Program (UK).

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 As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Emil Artin and John Tate. Class Field Theory. W. A. Benjamin, New York, 1967. Google Scholar
  2. 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.
  3. 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/.
  4. 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.
  5. Daniel Bump. Automorphic Forms and Representations. Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1997. URL: https://doi.org/10.1017/CBO9780511609572.
  6. 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.
  7. Mario Carneiro. The Type Theory of Lean. Springer, Berlin, Heidelberg, 2019. Master thesis. URL: https://github.com/digama0/lean-type-theory/releases.
  8. J. W. S. Cassels and A. Fröhlich (eds.). Algebraic Number Theory. Academic Press, London; Thompson Book Co., Inc., Washington, D.C., 1967. Google Scholar
  9. 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.
  10. Gerald J. Janusz. Algebraic Number Fields, volume 55 of Pure and Applied Mathematics. Academic Press, London, 2nd edition, 1996. Google Scholar
  11. 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.
  12. 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.
  13. J. S. Milne. Class Field Theory (v4.03), 2020. URL: https://www.jmilne.org/math/CourseNotes/CFT.pdf.
  14. Jürgen Neukirch. Algebraic Number Theory. Springer, Berlin, Heidelberg, 1999. URL: https://doi.org/10.1007/978-3-662-03983-0.
  15. Á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.
  16. Henning Stichtenoth. Algebraic Function Fields and Codes. Universitext. Springer, 1993. URL: https://dblp.org/rec/books/daglib/0084861.
  17. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact