Document Open Access Logo

A Formalization of Dedekind Domains and Class Groups of Global Fields

Authors Anne Baanen , Sander R. Dahmen , Ashvni Narayanan , Filippo A. E. Nuccio Mortarino Majno di Capriglio

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.5.pdf
  • Filesize: 0.75 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Mathematical software
  • Security and privacy → Logic and verification
Keywords
  • formal math
  • algebraic number theory
  • commutative algebra
  • Lean
  • mathlib

Metrics

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

Abstract

Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and mathlib’s decentralized collaboration processes involved in this project.

Cite As Get BibTex

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 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.5

Author Details

Anne Baanen
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
Sander R. Dahmen
  • Department of Mathematics, Vrije Universiteit Amsterdam, The Netherlands
Ashvni Narayanan
  • London School of Geometry and Number Theory, UK
Filippo A. E. Nuccio Mortarino Majno di Capriglio
  • Univ Lyon, Université Jean Monnet Saint-Étienne, CNRS UMR 5208, Institut Camille Jordan, F-42023 Saint-Étienne, France

Funding

  • Baanen, Anne: NWO Vidi grant No. 016.Vidi.189.037, Lean Forward
  • Dahmen, Sander R.: NWO Vidi grant No. 639.032.613, New Diophantine Directions
  • Narayanan, Ashvni: EPSRC Grant EP/S021590/1 (UK)

Acknowledgements

We would like to thank Jasmin Blanchette and the anonymous reviewers for useful comments on previous versions of the manuscript, which found their way into this paper. A. N. would like to thank Prof. Kevin Buzzard for his constant support and encouragement, and for introducing her to the other co-authors. A. N. and F. N. wish to express their deepest gratitude to Anne Baanen for the generosity shown along all stages of the project. Without Anne’s never-ending patience, it would have been impossible for them to contribute to this project, and to overcome several difficulties. Finally, we would like to thank the whole mathlib community for invaluable advice all along the project.

Supplementary Materials

References

  1. E. Artin and G. Whaples. Axiomatic characterization of fields by the product formula for valuations. Bull. Amer. Math. Soc., 51(7):469-492, July 1945. URL: https://projecteuclid.org:443/euclid.bams/1183507128.
  2. 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/.
  3. C. Ballarin (editor), J. Aransay, M. Baillon, P. E. de Vilhena, S. Hohe, F. Kammüller, and L. C. Paulson. The Isabelle/HOL algebra library. URL: http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html.
  4. Valentin Blot. Basics for algebraic numbers and a proof of Liouville’s theorem in C-CoRN, 2009. MSc internship report. Google Scholar
  5. Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, and Vincent Siles. Formalized linear algebra over elementary divisor rings in Coq. Logical Methods in Computer Science, 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:7)2016.
  6. M. Carneiro. Definition df-aa. URL: http://us.metamath.org/mpeuni/df-aa.html.
  7. M. Carneiro. Definition df-gz. URL: http://us.metamath.org/mpeuni/df-gz.html.
  8. C. Cohen. Construction of real algebraic numbers in Coq. In L. Beringer and A. P. Felty, editors, ITP 2012, volume 7406 of Lecture Notes in Computer Science, pages 67-82. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_6.
  9. L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean theorem prover (system description). In A. P. Felty and A. Middeldorp, editors, Automated Deduction - CADE-25, volume 9195 of LNCS, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  10. D. S. Dummit and R. M. Foote. Abstract algebra. John Wiley & Sons, Inc., Hoboken, NJ, third edition, 2004. Google Scholar
  11. M. Eberl. Minkowski’s theorem. Archive of Formal Proofs, 2017. , Formal proof development. URL: https://isa-afp.org/entries/Minkowskis_Theorem.html.
  12. M. Eberl. Nine chapters of analytic number theory in Isabelle/HOL. In J. Harrison, J. O'Leary, and A. Tolmach, editors, ITP 2019, volume 141 of LIPIcs, pages 16:1-16:19. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.16.
  13. M. Eberl. Gaussian integers. Archive of Formal Proofs, 2020. , Formal proof development. URL: https://isa-afp.org/entries/Gaussian_Integers.html.
  14. A. Fröhlich. Local fields. In Algebraic Number Theory (Proc. Instructional Conf., Brighton, 1965), pages 1-41. Thompson, Washington, D.C., 1967. Google Scholar
  15. Y. Futa, D. Mizushima, and H. Okazaki. Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. In 2012 International Symposium on Information Theory and its Applications, pages 591-595, 2012. Google Scholar
  16. A. Grabowski, A. Kornilowicz, and C. Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, volume 8 of ACSIS, pages 363-371, 2016. Google Scholar
  17. K. Ireland and M. Roosen. A Classical Introduction to Modern Number Theory. Springer-Verlag New York, second edition, 1990. Google Scholar
  18. Serge Lang. Algebra, volume 211 of Graduate Texts in Mathematics. Springer-Verlag, New York, third edition, 2002. URL: https://doi.org/10.1007/978-1-4613-0041-0.
  19. Robert Y. Lewis and Paul-Nicolas Madelaine. Simplifying casts and coercions (extended abstract). In Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, and Sophie Tourret, editors, Practical Aspects of Automated Reasoning, volume 2752 of CEUR Workshop Proceedings, pages 53-62. CEUR-WS.org, 2020. URL: http://ceur-ws.org/Vol-2752/paper4.pdf.
  20. A. Mahboubi and E. Tassi. The Mathematical Components Libraries. https://math-comp.github.io/mcb/, 2017.
  21. N. D. Megill and D. A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf. Google Scholar
  22. J. Neukirch. Algebraic number theory, volume 322 of Fundamental Principles of Mathematical Sciences. Springer-Verlag, Berlin, 1999. Translated from the 1992 German original and with a note by Norbert Schappacher, With a foreword by G. Harder. URL: https://doi.org/10.1007/978-3-662-03983-0.
  23. M. E. et al Pohst. The computer algebra system KASH/KANT. http://www.math.tu-berlin.de/~ kant. Google Scholar
  24. A. Stasinski. A uniform proof of the finiteness of the class group of a global field. to appear in Amer. Math. Monthly, 2020. URL: https://arxiv.org/abs/1909.07121.
  25. The mathlib Community. The Lean mathematical library. In J. Blanchette and C. Hrițcu, editors, CPP 2020, page 367–381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  26. The PARI Group, Univ. Bordeaux. PARI/GP version 2.11.2, 2019. available from URL: http://pari.math.u-bordeaux.fr/.
  27. R. Thiemann, A. Yamada, and S. Joosten. Algebraic numbers in Isabelle/HOL. Archive of Formal Proofs, 2015. , Formal proof development. URL: https://isa-afp.org/entries/Algebraic_Numbers.html.
  28. P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In Principles of Programming Languages, POPL '89, page 60–76. ACM, 1989. URL: https://doi.org/10.1145/75277.75283.
  29. Y. Watase. Algebraic numbers. Formalized Mathematics, 24(4):291-299, 2016. URL: https://doi.org/10.1515/forma-2016-0025.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact