A Formalization of Dedekind Domains and Class Groups of Global Fields

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

doi:10.1007/s10817-022-09644-0

A Formalization of Dedekind Domains and Class Groups of Global Fields

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

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

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.

Original language	English
Pages (from-to)	611-637
Number of pages	27
Journal	Journal of Automated Reasoning
Volume	66
Issue number	4
Early online date	8 Sept 2022
DOIs	https://doi.org/10.1007/s10817-022-09644-0
Publication status	Published - Nov 2022

Bibliographical note

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

Publisher Copyright:
© 2022, The Author(s).

Funding

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

Keywords

Algebraic number theory
Commutative algebra
Formal math
Lean
Mathlib

Access to Document

10.1007/s10817-022-09644-0

Persistent URL (handle)

Persistent link

Cite this

@article{9ae5eb4683864b7592278b08386e3d10,

title = "A Formalization of Dedekind Domains and Class Groups of Global Fields",

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{\textquoteright}s decentralized collaboration processes involved in this project.",

keywords = "Algebraic number theory, Commutative algebra, Formal math, Lean, Mathlib",

author = "Anne Baanen and Dahmen, {Sander R.} and Ashvni Narayanan and {Nuccio Mortarino Majno di Capriglio}, {Filippo A.E.}",

note = "Funding Information: Anne Baanen was funded by NWO Vidi Grant No. 016.Vidi.189.037, Lean Forward. Sander R. Dahmen was funded by NWO Vidi Grant No. 639.032.613, New Diophantine Directions. Ashvni Narayanan was funded by EPSRC Grant EP/S021590/1 (UK). Publisher Copyright: {\textcopyright} 2022, The Author(s).",

year = "2022",

month = nov,

doi = "10.1007/s10817-022-09644-0",

language = "English",

volume = "66",

pages = "611--637",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "4",

}

TY - JOUR

T1 - A Formalization of Dedekind Domains and Class Groups of Global Fields

AU - Baanen, Anne

AU - Dahmen, Sander R.

AU - Narayanan, Ashvni

AU - Nuccio Mortarino Majno di Capriglio, Filippo A.E.

N1 - Funding Information: Anne Baanen was funded by NWO Vidi Grant No. 016.Vidi.189.037, Lean Forward. Sander R. Dahmen was funded by NWO Vidi Grant No. 639.032.613, New Diophantine Directions. Ashvni Narayanan was funded by EPSRC Grant EP/S021590/1 (UK). Publisher Copyright: © 2022, The Author(s).

PY - 2022/11

Y1 - 2022/11

N2 - 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.

AB - 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.

KW - Algebraic number theory

KW - Commutative algebra

KW - Formal math

KW - Lean

KW - Mathlib

UR - http://www.scopus.com/inward/record.url?scp=85137570845&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85137570845&partnerID=8YFLogxK

U2 - 10.1007/s10817-022-09644-0

DO - 10.1007/s10817-022-09644-0

M3 - Article

AN - SCOPUS:85137570845

SN - 0168-7433

VL - 66

SP - 611

EP - 637

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 4

ER -

A Formalization of Dedekind Domains and Class Groups of Global Fields

Abstract

Bibliographical note

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this