A formalization of Dedekind domains and class groups of global fields. (English) Zbl 1524.68428
Summary: 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.
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 11R29 | Class numbers, class groups, discriminants |
| 13C20 | Class groups |
| 13F05 | Dedekind, Prüfer, Krull and Mori rings and their generalizations |
Software:
PARI/GP; Archive Formal Proofs; Metamath; Isabelle; KANT/KASH; Lean; Isabelle/HOL; mathlib; Minkowskis_Theorem; Gaussian_Integers; Algebraic NumbersReferences:
| [1] | Artin, E.; Whaples, G., Axiomatic characterization of fields by the product formula for valuations, Bull. Am. Math. Soc., 51, 7, 469-492 (1945) · Zbl 0060.08302 · doi:10.1090/S0002-9904-1945-08383-9 |
| [2] | Avigad, J., de Moura, L., Kong, S.: Theorem Proving in Lean. Carnegie Mellon University, Pittsburgh, PA, USA (2021). Release 3.23.0, https://leanprover.github.io/theorem_proving_in_lean/ |
| [3] | Baanen, T., Dahmen, S.R., Ashvni N., Nuccio Mortarino Majno di Capriglio, F.A.E.: A Formalization of Dedekind Domains and Class Groups of Global Fields. In: Cohen, L., Kaliszyk, C. (eds.) ITP 2021. LIPIcs, vol. 193, pp. 5-1519. Schloss Dagstuhl—Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021). doi:10.4230/LIPIcs.ITP.2021.5. https://drops.dagstuhl.de/opus/volltexte/2021/13900 · Zbl 1523.68167 |
| [4] | Baanen, T.: Use and abuse of instance parameters in the Lean mathematical library. CoRR abs/2202.01629 (2022) arxiv:2202.01629. Accepted for publication at ITP 2022, Haifa, Israel · Zbl 07881117 |
| [5] | Ballarin, C., Aransay, J., Baillon, M., de Vilhena, P.E., Hohe, S., Kammüller, F., Paulson, L.C.: The Isabelle/HOL Algebra Library. http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html |
| [6] | Blot, V.: Basics for algebraic numbers and a proof of Liouville’s theorem in C-CoRN. MSc internship report (2009) |
| [7] | Brasca, R., et al.: The ring of integers of a cyclotomic field. https://leanprover-community.github.io/blog/posts/the-ring-of-integers-of-a-cyclotomic-field/. Accessed 20 June 2022 |
| [8] | Cano, G., Cohen, C., Dénès, M., Mörtberg, A., Siles, V.: Formalized linear algebra over elementary divisor rings in Coq. Logical Methods in Computer Science 12(2) (2016). doi:10.2168/LMCS-12(2:7)2016 · Zbl 1448.68461 |
| [9] | Carneiro, M.: Definition df-aa. http://us.metamath.org/mpeuni/df-aa.html |
| [10] | Carneiro, M.: Definition df-gz. http://us.metamath.org/mpeuni/df-gz.html |
| [11] | Claborn, L., Every abelian group is a class group, Pac. J. Math., 18, 2, 219-222 (1966) · Zbl 0166.30602 · doi:10.2140/pjm.1966.18.219 |
| [12] | Cohen, C.: Construction of real algebraic numbers in Coq. In: Beringer, L., Felty, A.P. (eds.) ITP 2012. Lecture Notes in Computer Science, vol. 7406, pp. 67-82. Springer, Cham (2012). doi:10.1007/978-3-642-32347-8_6 · Zbl 1360.68744 |
| [13] | de Frutos-Fernández, M.I.: Formalizing the Ring of Adèles of a Global Field. arXiv (2022). doi:10.48550/ARXIV.2203.16344. arxiv:2203.16344 |
| [14] | de Lima, TA; Galdino, AL; Avelar, AB; Ayala-Rincón, M., Formalization of ring theory in PVS: isomorphism theorems, principal, prime and maximal ideals. Chinese remainder theorem, J. Automat. Reason., 65, 8, 1231-1263 (2021) · Zbl 1493.68389 · doi:10.1007/s10817-021-09593-0 |
| [15] | de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25. LNCS, vol. 9195, pp. 378-388. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_26 · Zbl 1465.68279 |
| [16] | Dummit, DS; Foote, RM, Abstract Algebra, 932 (2004), Hoboken: Wiley, Hoboken · Zbl 1037.00003 |
| [17] | Eberl, M.: Gaussian integers. Archive of Formal Proofs (2020). https://isa-afp.org/entries/Gaussian_Integers.html, Formal proof development |
| [18] | Eberl, M.: Minkowski’s theorem. Archive of Formal Proofs (2017). https://isa-afp.org/entries/Minkowskis_Theorem.html, Formal proof development |
| [19] | Eberl, M.: Nine chapters of analytic number theory in Isabelle/HOL. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) ITP 2019. LIPIcs, vol. 141, pp. 16-11619. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2019). doi:10.4230/LIPIcs.ITP.2019.16 · Zbl 07649965 |
| [20] | Fröhlich, A.: Local fields. In: Algebraic Number Theory (Proc. Instructional Conf., Brighton, 1965), pp. 1-41. Thompson, Washington, D.C. (1967) · Zbl 1492.11160 |
| [21] | Futa, Y., Mizushima, D., Okazaki, H.: Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. In: 2012 International Symposium on Information Theory and Its Applications, pp. 591-595 (2012) |
| [22] | Grabowski, A., Kornilowicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: Ganzha, M., Maciaszek, L., Paprzycki, M. (eds.) Proceedings of the 2016 Federated Conference on Computer Science and Information Systems. ACSIS, vol. 8, pp. 363-371 (2016) |
| [23] | Ireland, K.; Roosen, M., A Classical Introduction to Modern Number Theory (1990), Cham: Springer, Cham · Zbl 0712.11001 · doi:10.1007/978-1-4757-2103-4 |
| [24] | Lang, S.: Algebra, 3rd edn. Graduate Texts in Mathematics, vol. 211, p. 914. Springer, Cham (2002). doi:10.1007/978-1-4613-0041-0 · Zbl 0984.00001 |
| [25] | Lewis, R.Y., Madelaine, P.: Simplifying casts and coercions (extended abstract). In: Fontaine, P., Korovin, K., Kotsireas, I.S., Rümmer, P., Tourret, S. (eds.) Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol. 2752, pp. 53-62. CEUR-WS.org, Aachen, Germany (2020). http://ceur-ws.org/Vol-2752/paper4.pdf |
| [26] | Mahboubi, A.; Tassi, E., The Mathematical Components Libraries (2017), Genève: Zenodo, Genève · Zbl 1317.68221 · doi:10.5281/zenodo.4457887 |
| [27] | Megill, N.D., Wheeler, D.A.: Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, NC, USA (2019). http://us.metamath.org/downloads/metamath.pdf |
| [28] | Neukirch, J.: Algebraic Number Theory. Fundamental Principles of Mathematical Sciences, vol. 322, p. 571. Springer, Cham: Translated from the 1992 German original and with a note by Norbert Schappacher. With a foreword by G. Harder (1999). doi:10.1007/978-3-662-03983-0 |
| [29] | Pohst, M.E., et al.: The Computer Algebra System KASH/KANT. http://www.math.tu-berlin.de/ kant |
| [30] | Stasinski, A., A uniform proof of the finiteness of the class group of a global field, Am. Math. Monthly, 128, 3, 239-249 (2021) · Zbl 1469.11444 · doi:10.1080/00029890.2021.1855036 |
| [31] | The mathlib Community: the Lean mathematical library. In: Blanchette, J., Hriţcu, C. (eds.) CPP 2020, pp. 367-381. ACM, New York, USA (2020). doi:10.1145/3372885.3373824 |
| [32] | The PARI Group: PARI/GP Version 2.11.2. Univ. Bordeaux (2019). The PARI Group. http://pari.math.u-bordeaux.fr/ |
| [33] | Thiemann, R., Yamada, A., Joosten, S.: Algebraic numbers in Isabelle/HOL. Archive of Formal Proofs (2015). https://isa-afp.org/entries/Algebraic_Numbers.html, Formal proof development |
| [34] | Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Principles of Programming Languages. POPL ’89, pp. 60-76. ACM, Austin, TX, USA (1989). doi:10.1145/75277.75283 |
| [35] | Watase, Y., Algebraic numbers, Formaliz. Math., 24, 4, 291-299 (2016) · Zbl 1357.11107 · doi:10.1515/forma-2016-0025 |
| [36] | Zariski, O., Samuel, P.: Commutative Algebra, Volume I. The University Series in Higher Mathematics, p. 329. D. Van Nostrand Company, Inc., Princeton, NJ, USA (1958) · Zbl 0081.26501 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
