Document Open Access Logo

Formalizing Norm Extensions and Applications to Number Theory

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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.13.pdf
  • Filesize: 0.77 MB
  • 18 pages

Document Identifiers

Author Details

María Inés de Frutos-Fernández
  • Imperial College London, UK
  • Universidad Autónoma de Madrid, Spain

Funding

1) EPSRC Grant EP/V048724/1: Digitising the Langlands Program (UK). 2) This work has been supported by the Madrid Government (Comunidad de Madrid – Spain) under the multiannual Agreement with UAM in the line for the Excellence of the University Research Staff in the context of the V PRICIT (Regional Programme of Research and Technological Innovation)

Acknowledgements

I would like to thank Kevin Buzzard for many helpful conversations during the completion of this project, Thomas Browning for formalizing normal closures, and Yaël Dillies for the discussions on how best to integrate seminorms in mathlib. I also thank the mathlib community and maintainers for their support and insightful suggestions during the development of this work.

Cite AsGet BibTex

María Inés de Frutos-Fernández. Formalizing Norm Extensions and Applications to Number Theory. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.13

Abstract

The field ℝ of real numbers is obtained from the rational numbers ℚ by taking the completion with respect to the usual absolute value. We then define the complex numbers ℂ as an algebraic closure of ℝ. The p-adic analogue of the real numbers is the field ℚ_p of p-adic numbers, obtained by completing ℚ with respect to the p-adic norm. In this paper, we formalize in Lean 3 the definition of the p-adic analogue of the complex numbers, which is the field ℂ_p of p-adic complex numbers, a field extension of ℚ_p which is both algebraically closed and complete with respect to the extension of the p-adic norm. More generally, given a field K complete with respect to a nonarchimedean real-valued norm, and an algebraic field extension L/K, we show that there is a unique norm on L extending the given norm on K, with an explicit description. Building on the definition of ℂ_p, we formalize the definition of the Fontaine period ring B_{HT} and discuss some applications to the theory of Galois representations and to p-adic Hodge theory. The results formalized in this paper are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat’s Last Theorem.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • formal mathematics
  • Lean
  • mathlib
  • algebraic number theory
  • p-adic analysis
  • Galois representations
  • p-adic Hodge theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 3-20, Cham, 2020. Springer International Publishing. Google Scholar
  2. Emil Artin and John Tate. Class Field Theory. W. A. Benjamin, New York, 1967. Google Scholar
  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. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:20, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.4.
  5. Anne Baanen, Alex J. Best, Nirvana Coppola, and Sander R. Dahmen. Formalized class group computations and integral points on mordell elliptic curves. In Brigitte Pientka and Steve Zdancewic, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 47-62, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575682.
  6. 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.
  7. Siegfried Bosch, Ulrich Güntzer, and Reinhold Remmert. Non-archimedean analysis : a systematic approach to rigid analytic geometry. Springer-Verlag Berlin Heidelberg, 1984. Google Scholar
  8. Thomas Browning and Patrick Lutz. Formalizing Galois Theory. Experimental Mathematics, 31(2):413-424, 2022. URL: https://doi.org/10.1080/10586458.2021.1986176.
  9. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising Perfectoid Spaces. In Jasmin Blanchette and Cătălin Hriţcu, 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.
  10. José Manuel Rodríguez Caballero and Dominique Unruh. Complex bounded operators. Archive of Formal Proofs, September 2021. Formal proof development. URL: https://isa-afp.org/entries/Complex_Bounded_Operators.html.
  11. Mario Carneiro. The Type Theory of Lean, 2019. Master thesis. URL: https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf.
  12. Xavier Caruso. An introduction to p-adic period rings, volume 54 of Panoramas et Synthèses, pages 19-92. Société Mathématique de France, 2019. Google Scholar
  13. Johan Commelin and Robert Y. Lewis. Formalizing the Ring of Witt Vectors. In Cătălin Hriţcu and Andrei Popescu, editors, Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 264-277, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3437992.3439919.
  14. Aaron Crighton. p-adic fields and p-adic semialgebraic sets. Archive of Formal Proofs, September 2022. Formal proof development. URL: https://isa-afp.org/entries/Padic_Field.html.
  15. María Inés de Frutos-Fernández. Formalizing the Ring of Adèles of a Global Field. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.14.
  16. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378-388, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  17. Paulo Emílio de Vilhena and Lawrence C. Paulson. Algebraically Closed Fields in Isabelle/HOL. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 204-220, Cham, 2020. Springer International Publishing. Google Scholar
  18. Noboru Endou. Complex Linear Space and Complex Normed Space. Formalized Mathematics, 12(2):93-102, 2004. Google Scholar
  19. Jean-Marc Fontaine, editor. Périodes p-adiques - Séminaire de Bures, 1988, number 223 in Astérisque. Société mathématique de France, 1994. Google Scholar
  20. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-Checked Proof of the Odd Order Theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 163-179, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  21. Robert P. Langlands. Problems in the Theory of Automorphic Forms, volume 170 of Lecture Notes in Mathematics, pages 18-61. Springer, Berlin, Heidelberg, 1970. URL: https://doi.org/10.1007/BFb0079065.
  22. Robert Y. Lewis. A Formal Proof of Hensel’s Lemma over the p-Adic Integers. In Assia Mahboubi and Magnus O. Myreen, editors, 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.
  23. Assia Mahboub and Enrico Tassi. The Mathematical Components Libraries, 2017. URL: https://math-comp.github.io/mcb/.
  24. The mathlib Community. The Lean Mathematical Library. In Jasmin Blanchette and Cătălin Hriţcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  25. Sebastian Monnet. Formalising the Krull Topology in Lean, 2022. URL: https://arxiv.org/abs/2207.09486.
  26. Kazuhisa Nakasho, Yuichi Futa, and Yasunari Shidama. Topological Properties of Real Normed Space. Formalized Mathematics, 22(3):209-223, 2014. URL: https://doi.org/10.2478/forma-2014-0024.
  27. Á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.
  28. Christoph Schwarzweller. Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials. Formalized Mathematics, 28(3):251-261, 2020. URL: https://doi.org/10.2478/forma-2020-0022.
  29. Christoph Schwarzweller. Existence and Uniqueness of Algebraic Closures. Formalized Mathematics, 30(4):281-294, 2022. URL: https://doi.org/10.2478/forma-2022-0022.
  30. Christoph Schwarzweller and Agnieszka Rowińska-Schwarzweller. Algebraic Extensions. Formalized Mathematics, 29(1):39-47, 2021. URL: https://doi.org/10.2478/forma-2021-0004.
  31. 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 Imprint Privacy Contact