1 Introduction
-
Code samples throughout have been updated to reflect parts of our formalization contributed to mathlib after the previous publication and to incorporate changes in mathlib after contribution.
-
The new Sect. 3 gives a more detailed explanation of Lean as used in mathlib, in particular the use of typeclasses and bundling.
-
We discuss definitional equality in Lean in the context of overlapping typeclass instances in Sect. 4.1.
-
The further evolution of fraction rings in mathlib is discussed at the end of Sect. 4.5.
-
We give more details on the proof of finiteness of the class group and its formalization in Sect. 8.2.
-
We elaborate on future directions in Sect. 9.2, including research relying on the formalization described here.
2 Mathematical Background
3 Lean and Mathlib
e
has a unique type t
, written e: t
. The natural number 0 has type \(\mathbb {N}\), and the rational 0 has type \(\mathbb {Q}\). One can then identify 0:
\(\mathbb {N}\) with 0:
\(\mathbb {Q}\) using a map \(\mathbb {N}\rightarrow \mathbb {Q}\) called a coercion (denoted by the arrow \(\uparrow \) or left implicit), that is, (0:
\(\mathbb {Q}\)) = \(\uparrow \) (0
: \(\mathbb {N}\) )
. Types have types too, for example \(\mathbb {N}\) : Type
. The full hierarchy consists of an impredicative universe Prop
sitting at the bottom of a noncumulative chain Prop
: Type
: Type 1
: Type 2
\(:\,\ldots \) ; “an arbitrary Type u
” is abbreviated as Type*
. Propositions correspond to elements of Prop
, while a (verified) proof of the proposition P: Prop
corresponds to an element p: P
. In addition to these features commonly found in a dependent type theory, Lean provides proof irrelevance, quotient types and classical reasoning. Proof irrelevance means that for any proposition P: Prop
, any two proofs \({\texttt {p}}_{\texttt {1}}\, {\texttt {p}}_{\texttt {2}}: {\texttt {P}}\) are judged equal by the system. These features are all commonly used in mathlib.class
, then one can supply values for the class that Lean will automatically infer, by tagging these with instance
. As an example, consider a ring R with a subring S. The instance subring.to
_ring
says that S is also a ring. Consequently, one can now use lemmas about rings for S without having to invoke subring.to
_ring
. We put the implicit arguments to be inferred by the typeclass system in square brackets. Other implicit arguments remain in curly brackets, while explicit arguments go in round brackets. As an example, consider:
a
, which has type M
, and a natural number n
. As a result, Lean can determine the value of M
through unification and can then use the typeclass system to infer a value for [monoid M]
.simp
(simplifies the main goal target using lemmas tagged with the attribute [simp]
), library
_search
(tries to close the current goal by applying a lemma from the library), and ring
(proves equality of polynomial expressions over commutative (semi)rings). Lean uses these to simplify the statement or to close the goal. These are very efficient when working with proofs that are calculation heavy, or that follow from a small number of easy (or mathematically trivial) steps.3.1 Use of Typeclasses and Bundling
[monoid M]
parameter of pow
_succ a n
, a Prolog-like search is started to automatically synthesize a suitable value for this parameter. Each of the local parameters and the declarations marked as instance
is tested in turn to see if their type matches the expected type of the instance synthesis. All instance parameters of candidate instances are themselves recursively inferred, until either a suitable term is constructed or no more candidates remain; an error is raised in the latter case [2, Sect. 10]. Compared to Haskell’s, Lean’s typeclasses have few structural restrictions: notably, classes and instances can depend on any term, instances may overlap, classes can apply to multiple types, and can have functional dependencies.structure
keyword formally declaring a structure type whose elements are tuples. To confuse matters further, Lean implements typeclasses as structure types, where the typeclass instances are tuples of the typeclass’s fields. Typeclasses provided us a way to treat uniformly situations that are informally considered the same, as we discuss in Sects. 4.1 and 4.2. Our reliance on typeclasses did not cause any noticeable slowness in proof checking: there was no instance that should be found but could not due to timeouts.is
_number
_field
typeclass of Sect. 4 is considered to have unbundled inheritance from the field
class because instances of these classes are passed in separate parameters, while it has bundled inheritance from char
_zero
and finite
_dimensional
since both are included as fields of the structure. Similarly, the formalization of admissible absolute values discussed in Sect. 8.2 features a bundled structure absolute
_value
which includes a map along with proofs stating that this map is an absolute value, and an unbundled structure is
_admissible
which takes the absolute value map as a separate parameter.Prop
-valued and are not involved in long inheritance chains.4 Number Fields, Global Fields, and Rings of Integers
(K: Type*)
, while square brackets mark instance parameters inferred by the typeclass system, such as [field K]
. The condition [to
_char
_zero: char
_zero K]
states that K has characteristic zero, so the unique ring homomorphism \(\mathbb {Z}\rightarrow K\) is an embedding. This implies that there is a \(\mathbb {Q}\)-algebra structure on K (found by typeclass instance synthesis), endowing K with the \(\mathbb {Q}\)-vector space structure used in the hypothesis [to
_finite
_dimensional: finite
_dimensional
\(\mathbb {Q}\) K]
.[to
_algebra: algebra (ratfunc
\(\mathbb {F}_{q}\) ) F]
witnesses that F is a field extension of the field \(\mathbb {F}_{q}(t)\) of rational functions over \(\mathbb {F}_{q}\), where \(\mathbb {F}_{q}\) is any field (although in our applications we will insist that \(\mathbb {F}_{q}\) be actually finite). Again, the condition that this extension is finite is written using the finite
_dimensional
typeclass. We present a more detailed analysis of algebra
in Sect. 4.1 and of fraction fields including ratfunc
in Sect. 4.5. For now, we point out that there are many fields K that are isomorphic to the field of rational functions \(\mathbb {F}_{q}(t)\); we provided a theorem function
_field
_iff
that shows that the choice of K does not matter. Note that there is no requirement that the field Fq
is finite, since this is not needed to state the conditions on F
. We instead add a [fintype Fq]
hypothesis only to those results that require finiteness.4.1 Field Extensions
is
_number
_field
illustrates our treatment of field extensions. A field L containing a subfield K is said to be a field extension L/K. Often we encounter towers of field extensions: we might have that \(\mathbb {Q}\) is contained in K, K is contained in L, L is contained in an algebraic closure \(\overline{K}\) of K, and \(\overline{K}\) is contained in \(\mathbb {C}\). We might formalize this situation by viewing \(\mathbb {Q}\), K, L, and \(\overline{K}\) as sets of complex numbers \(\mathbb {C}\) and defining field extensions as subset relations between these subfields. This way, no coercions need to be inserted in order to map elements of one field into a larger field. Unfortunately, we can only avoid coercions as far as we are able to stay within one largest field. For example, the definition of complex numbers depends on many results for rational numbers, which would need to be proved again, or transported, for the subfield of \(\mathbb {C}\) isomorphic to \(\mathbb {Q}\).[algebra K L]
denoting a K-algebra structure on L. The algebra
structure provides us with a ring homomorphism \(\texttt {algebra} \_\texttt {map\,K\,L}: K \rightarrow L\); this map is injective because K and L are fields. In other words, field extensions are given by their embeddings.2 + 2:
\(\mathbb {N}\) is definitionally equal to 4
. Whenever Lean can infer the definitional equality of two terms (the terms are said to unify), one can be substituted for the other. Thus, ensuring definitional equality for instances means that overlapping instances will not lead to conflicts when one instance is expected and another is found.4.2 Scalar Towers
[algebra F K]
, [algebra K L]
, and [algebra F L]
, along with a parameter [is
_scalar
_tower F K L]
expressing that the maps commute.is
_scalar
_tower
typeclass derives its name from its applicability to any three types among which scalar multiplication operations exist:
[is
_scalar
_tower R A M]
parameter. Since x
\(\cdot \) y
for an R-algebra A is defined as algebra
_map R A x * y
, applying smul
_assoc
for each x : K with \(y = (1: L)\) and \(z = (1: F)\) shows that the algebra
_maps
indeed commute in a tower of field extensions L/K/F.is
_scalar
_tower
instances are declared in mathlib, such as for the maps \(R \rightarrow S \rightarrow B\) when S is a R-subalgebra of A and B is an A-algebra such that is
_scalar
_tower R A B
; this also implies that the maps \(R \rightarrow S \rightarrow A\) form a tower. The effect is that almost all coherence proof obligations are automated through typeclass instance synthesis. Only when defining a new algebra structure were we required to supply the is
_scalar
_tower
instances ourselves.4.3 Rings of Integers
is
_number
_field
), the ring \(\mathcal {O}_{K}\) of integers in K is defined as the integral closure of \(\mathbb {Z}\) in K. This is the subring containing those x : K that are a root of a monic polynomial with coefficients in \(\mathbb {Z}\):
integral
_closure
was already defined in mathlib. When K is a function field over the finite field \(\mathbb {F}_{q}\), we defined \(\mathcal {O}_{K}\) analogously as integral
_closure (
\(\mathbb {F}_{q}\) [X]) K
.is
_integral
_closure A R B
stating that A is the integral closure of R in B, and worked with a generic is
_integral
_closure
instance instead of the specific ring
_of
_integers
construction when possible.4.4 Subobjects
structure
comprising the carrier set and proofs showing the carrier set is closed under the relevant operations. Bundled subobjects provide similar benefits to those of bundled morphisms; the choice for the latter is explained in the mathlib overview paper [31]. Where the algebra
and is
_scalar
_tower
typeclasses provide an interface generalizing over multiple equivalent definitions, subobjects provide a specific implementation of that interface in the form of a subtype.subfield
as well as intermediate
_field
. We defined a subfield of a field K as a subset of K that contains 0 and 1 and is closed under addition, negation, multiplication, and taking inverses. If L is a field extension of K, we defined an intermediate field as a subfield of L that is also a K-subalgebra: in other words, a subfield that contains the image of \(\texttt {algebra} \_\texttt {map\,K\,L} \). Other examples of subobjects available in mathlib are submonoids, subgroups, and submodules (with ideals as a special case of submodules); all of these are provided with an instance of the set
_like
typeclass that supplies notation such as a membership relation “\(x \in S\).”intermediate
_field
to mathlib, the Berkeley Galois theory group used it in a formalization of the primitive element theorem. Soon after the primitive element theorem was merged into mathlib, we used it in our development of the trace form. This anecdote illustrates the decentralized development style of mathlib, with different groups and people building on each other’s results in a collaborative process.set
_like
typeclass, subobjects can be coerced to types, by sending a subobject S to the subtype of all elements of S. By putting typeclass instances on this subtype, we could reason about inductively defined rings such as \(\mathbb {Z}\) and subrings such as integral
_closure
\(\mathbb {Z}\) K
uniformly. If \(S: \texttt {subfield}\ K\), there is a ring embedding, the map that sends x : S to K by “forgetting” that \(x \in S\), and we registered this map as an algebra S K
instance, also allowing us to treat field extensions of the form \(\mathbb {Q}\rightarrow \mathbb {C}\) and subfields uniformly. Similarly, for \(F: \texttt {intermediate} \_\texttt {field\,K\,L} \), we defined the corresponding algebra K F
, algebra F L
, and is
_scalar
_tower K F L
instances.4.5 Fields of Fractions
fraction
_ring R
, and is used to define the field of rational functions \(K(X) = \texttt {ratfunc\,K} \). When \(R=\mathbb {Z}\), this yields the traditional description of \(\mathbb {Q}\) as the set of equivalence classes of fractions, where \(\frac{2}{3}=\frac{-4}{-6}\), etc.[algebra R K]
instance, where the map algebra
_map R K
witnesses that all elements K are “fractions” of elements of R—and to parametrize every result over the choice of K. The conditions on the R-algebra structure on K are encoded as a typeclass is
_fraction
_ring R K
. In the definition used by mathlib, a fraction ring is a special case of a ring localization, which is defined for any commutative ring R. Different localizations restrict the denominators to different multiplicative submonoids of \(R\setminus \{0\}\).algebra
_map R K
imply that K is the smallest field, up to isomorphism, containing R, expressed by the following unique mapping property. If \(g :R \rightarrow A\) is an injective map to a ring A such that g(x) has a multiplicative inverse for all \(x \ne 0: R\), then it can be extended uniquely to a map \(K \rightarrow A\) compatible with algebra
_map R K
and g. In particular, given \({\texttt {is}}\_{\texttt {fraction}}\_{\texttt {ring}}\,{\texttt {R}}\,{\texttt {K}}_{\texttt {1}}\) and \({\texttt {is}}\_{\texttt {fraction}}\_{\texttt {ring}}\,{\texttt {R}}\,{\texttt {K}}_{\texttt {2}}\), we can derive an isomorphism \(K_1 \simeq K_2\). The construction of \({{\,\mathrm{Frac}\,}}R\) then results in a field of fractions (with an instance is
_fraction
_ring R (fraction
_ring R)
) rather than the field of fractions.quotient
_ring R
, constructed similarly to the current definition of fraction
_ring R
. Due to the aforementioned drawback—namely, that this provided no easy way to view \(\mathbb {Q}\) as the field of fractions of \(\mathbb {Z}\), for instance—this was refactored to use a characteristic predicate instead.fraction
_map R K
. Results on fraction fields were parametrized over a choice of fraction map f. This made it possible to view \(\mathbb {Q}\) as the fraction field of \(\mathbb {Z}\), by providing a suitable map called int.fraction
_map
: fraction
_map
\(\mathbb {Z}~\mathbb {Q}\). This came at a price: informally, at any given stage of one’s reasoning, the field K is fixed and the map \(f:R\rightarrow K\) is applied implicitly, just viewing every x : R as x : K. It is now impossible to view \(R \le K\) as an inclusion of R-subalgebras, because the map f is needed explicitly to give the R-algebra structure on K. As a workaround, mathlib used a type synonym codomain f:= K
and instantiated the R-algebra structure given by f on this synonym. Again we encountered a distinction between \(\mathbb {Q}\) “itself” and \({{\,\mathrm{Frac}\,}}(\mathbb {Z}) = \texttt {codomain\, int.fraction} \_\texttt {map} \), still requiring the transfer of results such as typeclass instances.algebra
typeclass to denote inclusions of rings, we unbundled the explicit (f: fraction
_map R K)
parameters into an instance parameter [algebra R K]
that specifies the map, and an instance parameter [is
_fraction
_ring R K]
that specifies the conditions satisfied by the map. Separating out these parameters finally allowed us to painlessly view \(\mathbb {Q}\) as the fraction ring of \(\mathbb {Z}\) while preserving the original \(\mathbb {Z}\)-algebra structure on \(\mathbb {Q}\).4.6 Representing Monogenic Field Extensions
power
_basis
structure, we gained the ability to parametrize our results, being able to choose the F and K in a monogenic field extension K/F, or being able to choose the \(\alpha \) generating \(F(\alpha )\) (by setting the gen
field to \(\alpha \)). To specialize a result from an arbitrary K with a power basis over F to a specific construction of \(K = F(\alpha )\), one can apply the result to the power basis pb
generated by \(\alpha \) and rewrite \(\texttt {power} \_\texttt {basis.gen\,pb} = \alpha \).5 Dedekind Domains
5.1 Definitions
-
is
_dedekind
_domain D
: D is a Noetherian integral domain, integrally closed in its fraction field and has Krull dimension at most 1; -
is
_dedekind
_domain
_inv D
: D is an integral domain and nonzero fractional ideals of D have a multiplicative inverse (we discuss the notion and formalization of fractional ideals in Sect. 5.2); -
is
_dedekind
_domain
_dvr D
: D is a Noetherian integral domain and the localization of D at each nonzero prime ideal is a discrete valuation ring.
is
_dedekind
_domain
as the main definition, since this condition is usually the one checked in practice [28]. The other two equivalent definitions were added to mathlib, but before formalizing the proof that they are indeed equivalent. Having multiple definitions allowed us to do our work in parallel without depending on unformalized results. For example, the proof of unique ideal factorization in a Dedekind domain initially assumed is
_dedekind
_domain
_inv D
, and the proof that the ring of integers \(\mathcal {O}_{K}\) is a Dedekind domain concluded is
_dedekind
_domain (ring
_of
_integers K)
. After the equivalence between is
_dedekind
_domain D
and is
_dedekind
_domain
_inv D
was formalized, we could easily replace usages of is
_dedekind
_domain
_inv
with is
_dedekind
_domain
.is
_dedekind
_domain
and is
_dedekind
_domain
_inv
require a fraction field K, although the truth value of the predicates does not depend on the choice of K. For ease of use, we let the type of is
_dedekind
_domain
depend only on the domain D by instantiating K in the definition as fraction
_ring D
. From now on, we fix a fraction field K of D.
is
_dedekind
_domain
can choose a specific fraction field through the following lemma exposing the alternate definition:
is
_dedekind
_domain
as a typeclass by using the keyword class
rather than structure
, allowing the typeclass system to automatically infer the Dedekind domain structure when an appropriate instance is declared, such as for PIDs or for rings of integers.5.2 Fractional Ideals
is
_fractional
as a predicate on R-submodules J of F, informally as “there is an x : R with \(x J \subseteq R\).” For a Dedekind domain, nonzero fractional ideals form a group under multiplication. As seen in Sect. 4.5, this notion depends on the field F as well as on the embedding f := algebra
_map R F
. A more precise way of stating the above condition is then \(f(x)J\subseteq f(R)\). We formalized the definition of fractional ideals of R contained in F as a type fractional
_ideal R F
, whose elements consist of an R-submodule of F along with a proof of is
_fractional
. The structure of fractional ideals does not depend on the choice of a fraction field, which we formalized as an isomorphism fractional
_ideal.canonical
_equiv
between two types of fractional ideals on R, corresponding to different fields of fractions.group
_with
_zero
in mathlib, consisting of groups endowed with an extra element 0
whose inverse is again 0
.5.3 Equivalence of the Definitions
is
_dedekind
_domain
and is
_dedekind
_domain
_inv
of being a Dedekind domain are equivalent. Let D be a Dedekind domain, and let \(f:D\rightarrow K\) a fraction map to a field of fractions K of D.is
_dedekind
_domain
_inv
implies is
_dedekind
_domain
, we follow the proof given by Fröhlich in [20, Chap. 1, Sect. 2, Proposition 1.2.1]. A constant challenge that was faced while coding this proof was already mentioned in Sect. 4.5, namely the fact that elements of the domain must be traced along the inclusion into the chosen field of fractions. The proofs for being integrally closed and of dimension being less than or equal to 1 are fairly straightforward.b: B,
\(a*b\). However, it is quite challenging to formalize that an element of \(A*B\) must be a finite sum \(\sum _{i} a_i*b_i\), for \(a_i \in A\) and \(b_i \in B\). Instead, we show that, for every element \(x\in A*B\), there are finite sets \(T\subseteq A\), \(T'\subseteq B\) such that x
\(\in \) span (T * T’)
, formalized as submodule.mem
_span
_mul
_finite
_of
_mem
_mul
. Now considering a nonzero integral ideal I of the ring D, by definition of invertibility we can write 1
\(\in \) (1
: fractional
_ideal D K) = I * I
\({}^{-1}\). Hence, we obtain finite sets \(T \subset I\) and \(T' \subset I{}^{-1}\) such that 1 is contained in the D-span of \(T*T'\). We used the norm
_cast
tactic [25] to resolve most coercions but this tactic did not solve coercions coming from the inclusion algebra
_map D K
. With coercions, the actual statement of the latter expression in Lean is \(\uparrow \) T’
\(\subseteq \) \(\uparrow \uparrow \) (
\(\uparrow \) I)
\({}^{-1}\), which reads
fractional
_ideal.mul
_inv
_cancel
proves the converse, namely that is
_dedekind
_domain
implies is
_dedekind
_domain
_inv
. The classical proof consists of three steps: first, every maximal ideal \(M\subseteq D\), seen as a fractional ideal, is invertible; second, every nonzero ideal is invertible, using that it is contained in a maximal ideal; third, the fact that every fractional ideal J satisfies \(xJ\le I\) for a suitable element \(x\in D\) and a suitable ideal \(I\subseteq D\) implies that every fractional ideal is invertible, concluding the proof that nonzero fractional ideals form a group. The third step was easy, building upon the material developed for the general theory of fractional
_ideal
. Concerning the first two, we found that passing from the case where M is maximal to the general case required more code than directly showing invertibility of arbitrary nonzero ideals. The formal statement reads
I
: ideal D
and its coercion \(\uparrow \) I
: fractional
_ideal D K
although these objects, from a mathematical point of view, are identical.exists
_not
_mem
_one
_of
_ne
_bot
, which says that for every nontrivial ideal \(0\subsetneq I\subsetneq D\), there exists an element in the field K which is not integral (so, not in 1: fractional
_ideal D K
) but lies in \(I{}^{-1}\). The proof begins by invoking that every nonzero ideal in the Noetherian ring D contains a product of nonzero prime ideals. This result was not previously available in mathlib. The dimension condition shows its full force when applying this lemma: each prime ideal in the product \(I*I^{-1}\), being nonzero, will be maximal because the Krull dimension of D is at most 1; from this, exists
_not
_mem
_one
_of
_ne
_bot
follows easily. Having the above lemma at our disposal, we were able to prove that every ideal \(I\ne 0\) is invertible by arguing by contradiction: if \(I*I{}^{-1}\ne D\), we can find an element \(x\in K{\setminus } D\) which is in \((I*I{}^{-1}){}^{-1}\) thanks to exists
_not
_mem
_one
_of
_ne
_bot
; some easy algebraic manipulation then implies that x is actually integral over D. Since D is integrally closed, \(x \in D\), contradicting the construction of x. Combining these results gives the equivalence between the two conditions for being a Dedekind domain.5.4 Unique Ideal Factorization
associates
\(\alpha \). With much of the necessary definitions and properties already formalized, the formalization of this unique factorization result has been done in well under 100 lines of Lean code. One of the main mathematical ingredients (interesting in its own right) is that for ideals in a Dedekind domain, to divide is to contain:
6 Principal Ideal Domains are Dedekind
[comm_ring R] [is
_domain R] [is
_principal
_ideal
_ring R]
to denote a PID R, where is
_domain
is a typeclass asserting that the ring is nontrivial and there are no zero divisors, and is
_principal
_ideal
_ring
is a typeclass defined for all commutative rings:
[comm
_ring R] [is
_domain R] [is
_principal
_ideal
_ring R]
imply is
_dedekind
_domain R
was relatively short:
principal
_ideal
_ring.is
_noetherian
_ring
, since, by definition, each ideal in a principal ideal ring is finitely generated (by a single element).dimension
_le
_one.principal
_ideal
_ring
, which is an instantiation of the existing result is
_prime.to
_maximal
_ideal
, showing that a nonzero prime ideal in a PID is maximal. The latter lemma uses the characterization that I is a maximal ideal if and only if any strictly larger ideal \(J\supsetneq I\) is the full ring R. If I is a nonzero prime ideal and \(J \supsetneq I\) in the PID R, we see that a generator j of J is a divisor of any generator i of I. Since I is prime, this implies that either \(j \in I\), contradicting the assumption that \(J \supsetneq I\), or \(i = 0\), contradicting that I is nonzero, or finally that j is a unit, implying \(J = R\) as desired.principal
_ideal
_ring.to
_unique
_factorization
_monoid
to deduce that a PID is a unique factorization monoid (UFM), to instantiate our proof that every UFD is integrally closed. In a PID, the Noetherian property implies that the division relation is well-founded, and principal
_ideal
_ring.irreducible
_iff
_prime
shows that irreducible elements and prime elements coincide. To prove that an irreducible element p is prime, the proof uses that prime elements generate prime ideals and irreducible elements of a PID generate maximal ideals. Since all maximal ideals are prime ideals, the ideal generated by p is maximal, hence prime, thus p is prime. We proved the lemma irreducible
_of
_prime
, which shows the converse holds in any commutative monoid with zero.denom
_dvd
_of
_is
_root
, which states that for a polynomial p : R[X] and an element of the fraction field \(x: {{\,\mathrm{Frac}\,}}R\) such that \(p(x) = 0\), the denominator of x divides the leading coefficient of p. If x is integral with minimal polynomial p, the leading coefficient is 1, therefore the denominator is a unit and x is an element of R. This gave us the required lemma unique
_factorization
_monoid.integrally
_closed
, which states that the integral closure of R in its fraction field is R itself.7 Rings of Integers are Dedekind Domains
is
_fraction
_ring
_of
_finite
_extension D F K: is
_fraction
_ring S K
. The main content of is
_fraction
_ring
_of
_finite
_extension
consisted of showing that all elements x : K can be written as y/z for elements \(y \in S\), \(z \in D \subseteq S\); the standard proof of this fact (see [16, Theorem 15.29]) formalized readily.7.1 The Trace Form
lmul:=
\(\lambda \) x y
: K, x * y
. The trace of the linear map lmul x
is called the algebra trace \({{\,\mathrm{Tr}\,}}_{K / F}(x)\) of x. We defined the algebra trace as a linear map, in this case from K to F:
linear
_map.trace
makes a case distinction on the existence of a finite basis, choosing an arbitrary finite basis if one exists (since the value of linear
_map.trace
does not depend on this choice) and returning 0 otherwise. This latter case did not occur in our development.[algebra F K] [algebra K L] [algebra F L] [is
_scalar
_tower F K L]
, as described in Sect. 4.2.trace
_algebra
_map x
: trace F K (algebra
_map F K x) = finrank F K * x
as well as trace
_trace x
: trace F K (trace (K L x)) = trace F L x
; here finrank F K
is the degree of the field extension K/F. These results followed by direct computation.minpoly F x
, the minimal polynomial of x over F). In formalizing this formula, we first mapped the trace to L using the embedding \(\texttt {algebra} \_\texttt {map\,F\,L} \), which gave the following statement:
roots (map (algebra
_map F L) (minpoly F pb.gen))
are called conjugates of x in L. Each conjugate of x is integral since it is a root of the same monic polynomial, and integer multiples and sums of integral elements are integral. Combining trace
_gen
_eq
_sum
_roots
and trace
_algebra
_map
showed that the trace of x is an integer multiple (namely finrank F(x) L
) of a sum of conjugate roots, hence we concluded that the trace (and trace form) of an integral element is also integral.pb
generated by an element x : K. Letting \(x_k\) denote the k-th conjugate of x in an algebraically closed field L/K/F, the main difficulty was in checking the equality \(\sum _k x_k^{i + j} = {{\,\mathrm{Tr}\,}}_{K / F} (x^{i + j})\). Directly applying trace
_gen
_eq
_sum
_roots
was tempting, since we had a sum over conjugates of powers on both sides. However, the two expressions did not precisely match: the left-hand side is a sum of conjugates of x, where each conjugate is raised to the power \(i + j\), while the conclusion of trace
_gen
_eq
_sum
_roots
resulted in a sum over conjugates of \(x^{i + j}\).trace
_gen
_eq
_sum
_roots
through the equivalence gave \({{\,\mathrm{Tr}\,}}_{K / F}(x) = \sum _{\sigma } \sigma \ x\). Since each \(\sigma \) is a ring homomorphism, \(\sigma \ x^{i + j} = (\sigma \ x)^{i + j}\), so the conjugates of \(x^{i + j}\) are the \((i + j)\)-th powers of conjugates of x, which concluded the proof.8 Class Group and Class Number
8.1 The Class Group
class
_group.mk0
sending nonzero integral ideals of R to the corresponding class in the class group.8.2 Finiteness Results
class
_group.fintype
_of
_admissible
_of
_finite
, that the integral closure S of D in K has a finite class group whenever D has an “admissible” absolute value abs
. This notion originated in our project from the adaptation and generalization of the classical finiteness proof in interaction with the formalization efforts. Very informally, the admissibility conditions require that the remainder operator %
produces values that are not too far apart. More precisely, and in more “ordinary” mathematical notation, writing \({{\,\mathrm{mod}\,}}\) instead of \(\%\) and \(x \mapsto |x |\) for the absolute value function \(D \rightarrow \mathbb {Z}\), the latter is called admissible if both:-
we have a function \({{\,\mathrm{card}\,}}: \mathbb {R}_{>0} \rightarrow \mathbb {N}\);
-
for all \(\epsilon \in \mathbb {R}_{>0},\ b \in D-\{0\}\), and finite subsets \(A \subset D\), we can partition A into at most \({{\,\mathrm{card}\,}}(\epsilon )\) parts, such that all \(x, y \in A\) in the same part satisfy$$\begin{aligned} |x {{\,\mathrm{mod}\,}}b - y {{\,\mathrm{mod}\,}}b |< \epsilon |b |. \end{aligned}$$
abv
:
is
_euclidean abv
predicate asserts that the absolute value abv
: D
\(\rightarrow \) \(\mathbb {Z}\) respects the remainder operator of the Euclidean domain D, in particular abv (a % b)
\(\texttt {<} \) abv b
.x
: S
as the determinant of the linear map lmul x
. We used the admissibility of abs
to find a finite set finset
_approx
of elements of D, such that the following generalization of [23, Theorem 12.2.1] holds.
finset
_approx
, hence M is nonzero. Since the ideals of the Dedekind domain S have unique factorization, the nonzero ideal \(\langle M \rangle \) spanned by M has only finitely many divisors. To contain is to divide in Dedekind domains, so there are only finitely many ideals J with \(M \in J\). Thus, we concluded that \(\mathcal {C}l_{K}\) is finite under the condition of the existence of an admissible absolute value on D.number
_field.class
_number
and function
_field.class
_number
as the cardinality of the respective class groups.[is
_separable F K]
assumption above. For instance, using that any function field K, given as finite extension of \(\mathbb {F}_{q}(t)\), contains an \(s \in K\) such that \(K/\mathbb {F}_{q}(s)\) is a finite and separable extension; see for example [24, Corollary 4.4 in Chap. VIII] (noting that \(\mathbb {F}_{q}\) is perfect and K has transcendence degree 1 over \(\mathbb {F}_{q}\)). One then also needs to show that the finiteness of the class group of the integral closure of \(\mathbb {F}_{q}[s]\) in K is preserved upon replacing \(\mathbb {F}_{q}[s]\) by \(\mathbb {F}_{q}[t]\). A trivial way to get rid of the assumption in the statement above is to simply move it to our definition of function field. While this would be mathematically consistent by the result just cited, we did not opt to do this (for instance showing a finite extension of a function field is a function field would become nontrivial). Alternatively, one could aim at dropping the separability condition in the formalized result mentioned in the first paragraph of Sect. 7. Having a formalization of this generalization would be interesting in its own right. This approach would also still need the adaptation of some of the details in the final steps for the finiteness of the class group in the admissible case.class
_number
_eq
_one
_iff
, stating that the class number of K is 1 if and only if \(\mathcal {O}_{K}\) is a principal ideal domain. After defining the isomorphism rat.ring
_of
_integers
_equiv
showing \(\mathcal {O}_{\mathbb {Q}}\) is \(\mathbb {Z}\), we could use the fact that \(\mathbb {Z}\) is a PID to conclude that the class number of \(\mathbb {Q}\) is equal to 1:
9 Discussion
9.1 Related Work
set.mm
database for MetaMath [27], and the Mizar Mathematical Library [22]. The field of algebraic numbers, or more generally algebraic closures of arbitrary fields, are also available in many provers. For example, Blot [6] formalized algebraic numbers in Coq, Cohen [12] constructed the subfield of real algebraic numbers in Coq, Thiemann et al. [33] formalized algebraic numbers in Isabelle/HOL, Carneiro [9] in MetaMath, and Watase [35] in Mizar. To our knowledge, the Coq Mathematical Components library is the only formal development beside ours specifically dealing with number fields [26, field/algnum.v
].9.2 Future Directions
-
The group of units of the ring of integers \(\mathcal {O}_{K}^{\times }\) in a number field K is finitely generated, or even Dirichlet’s unit theorem [28, Theorem 7.4], stating that \(\mathcal {O}_{K}^{\times }\) has rank \(r+s-1\) and that its torsion subgroup is the cyclic group of roots of unity in K. Here r denotes the number of real embeddings of K and s the number of conjugate pairs of complex nonreal embeddings of K. The finite generation result also holds in function fields, again with a precise description of the rank and of the torsion.
-
Other finiteness results in algebraic number theory, most notably Hermite’s theorem about the existence of finitely many number fields, up to isomorphism, with bounded discriminant [28, Theorem 2.16]. While this could be done without interpreting the primes dividing the discriminant as the primes that ramify in the number field, it would certainly be interesting to set up some basic ramification theory: on the one hand, this would also prove essential for many other developments and, on the other, it would allow to prove a version of Hermite’s theorem stating that, up to isomorphism, there are only finitely many number fields with bounded degree and restricted ramification. As usual, there are analogous results in the function field setting, though they are less straightforward. One reason for this is that the nondegeneracy of the trace form from Sect. 7.1 does not hold any more when the separability condition is dropped.
-
Class number computations, starting with, say, quadratic number fields. This could be a step towards the verification of correctness of number-theoretic software, such as KASH/KANT [29] and PARI/GP [32]. Along the same lines, unit group computations would also be of much interest, most notably the explicit computation of \(r+s-1\) generators for the free part of \(\mathcal {O}_{K}^{\times }\). Restricting to quadratic fields, we see that the rank is positive (and equal to 1) if and only if the field is of the shape \(\mathbb {Q}(\sqrt{d})\) for some positive integer d that is not a square. Finding a generator can be done by using continued fractions, of which the basics are already implemented in Lean by Kevin Kappelmann, though certifying that a given (perhaps externally computed) element is indeed a generator could also be done without continued fractions.
-
Applications of algebraic number theory to solving Diophantine equations, such as determining all pairs of integers (x, y) such that \(y^2=x^3+D\) for some nonzero \(D \in \mathbb {Z}\). It would be interesting to deal with some values of D where no elementary techniques are available and where factorization in the ring of integers of \(\mathbb {Q}(\sqrt{D})\), along with information about the class number, could solve the equation.
9.3 Conclusion
is
_scalar
_tower
, is
_fraction
_ring
or power
_basis
, allows to treat equivalent viewpoints uniformly without the need for transferring results.