This repository contains the source code for the extended version of the paper "A formalization of Dedekind domains and class groups of global fields", submitted to the Journal of Automated Reasoning.
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.
The formalization has been developed for the community fork of Lean 3.
To install a full Lean development environment, please follow the "Regular install" instructions at https://leanprover-community.github.io/get_started.html.
After installation, you can run the command leanproject get lean-forward/class-number to obtain copies of the relevant source files and all dependencies.
Our results have been merged into the Lean mathematical library mathlib; this repository hosts copies of the files that are relevant to our project.
When opening a Lean project in VS Code, you must use the "Open Folder" menu option to open the project's root directory.
On the command line, you can run code path/to/class-number.
The following files contain major contributions from our project:
src/field_theory/intermediate_field.leansrc/field_theory/subfield.leansrc/number_theory/class_number/admissible_absolute_value.leansrc/number_theory/class_number/admissible_abs.leansrc/number_theory/class_number/admissible_card_pow_degree.leansrc/number_theory/class_number/finite.leansrc/number_theory/class_number/function_field.leansrc/number_theory/class_number/number_field.leansrc/number_theory/function_field.leansrc/number_theory/number_field.leansrc/ring_theory/class_group.leansrc/ring_theory/dedekind_domain/basic.leansrc/ring_theory/dedekind_domain/ideal.leansrc/ring_theory/dedekind_domain/integral_closure.leansrc/ring_theory/fractional_ideal.leansrc/ring_theory/integrally_closed.leansrc/ring_theory/power_basis.leansrc/ring_theory/trace.lean
The following files contain declarations mentioned in the paper or otherwise important to understanding our formalization:
src/group_theory/group_action/defs.leansrc/field_theory/adjoin.leansrc/field_theory/primitive_element.leansrc/ring_theory/integral_closure.leansrc/ring_theory/localization/fraction_ring.leansrc/ring_theory/noetherian.leansrc/ring_theory/principal_ideal_domain.leansrc/ring_theory/unique_factorization_domain.lean
We will now provide an overview of the source code files containing results mentioned in the paper.
- number fields:
src/algebraic_number_theory/number_field.lean - function fields:
src/algebraic_number_theory/function_field.lean - algebras:
src/algebra/algebra/basic.lean - scalar towers:
src/group_theory/group_action/defs.lean - ring of integers (of a number field):
src/number_theory/number_field.lean - ring of integers (of a function field):
src/number_theory/function_field.lean - integral closure:
src/ring_theory/integral_closure.lean - subfield:
src/field_theory/subfield.lean set_like:src/data/set_like/basic.lean- intermediate field:
src/field_theory/intermediate_field.lean - fraction field:
src/ring_theory/localization/fraction_ring.lean - power basis:
src/ring_theory/power_basis.lean
- Dedekind domain:
src/ring_theory/dedekind_domain/basic.lean - Krull dimension:
src/ring_theory/dedekind_domain/basic.lean - integrally closed:
src/ring_theory/integrally_closed.lean - integral closure:
src/ring_theory/integral_closure.lean - Noetherian ring:
src/ring_theory/noetherian.lean - fractional ideal:
src/ring_theory/fractional_ideal.lean - inverses of fractional ideals:
src/ring_theory/dedekind_domain/ideal.lean - group with zero:
src/algebra/group_with_zero/basic.lean - unique factorization monoid:
src/ring_theory/unique_factorization_domain.lean
- principal ideal domain:
src/ring_theory/principal_ideal_domain.lean - unique factorization monoid:
src/ring_theory/unique_factorization_domain.lean
- going up theory:
src/ring_theory/ideal/over.lean - trace form:
src/ring_theory/trace.lean - minimal polynomial:
src/field_theory/minpoly.lean - conjugate element:
src/ring_theory/trace.lean
- class group:
src/ring_theory/class_group.lean - admissible absolute value:
src/number_theory/class_number/admissible_absolute_value.lean - finiteness of the class group:
src/number_theory/class_number/finite.lean - class number of a number field:
src/number_theory/class_number/number_field.lean - class number of a function field:
src/number_theory/class_number/function_field.lean