Algebraic Number Theory

InstanceFiniteness of the class number #

Finiteness of the class number is the theorem that the ideal class group of the ring of integers of a number field is finite. Its order, the class number, measures how far that ring is from being a principal ideal domain, and in particular whether factorization of elements into irreducibles in it is unique. Together with the Dirichlet unit theorem it is one of the two basic finiteness results of algebraic number theory.

Statement

Let $K$ be a number field, that is, a finite extension of the rational numbers, and let $\mathcal{O}_K$ be its ring of integers, the elements of $K$ that are roots of monic polynomials with integer coefficients. The ring $\mathcal{O}_K$ is a Dedekind domain: every nonzero ideal factors uniquely as a product of prime ideals. Its nonzero fractional ideals form an abelian group under multiplication, the principal fractional ideals form a subgroup, and the quotient group is the ideal class group $\mathrm{Cl}(K)$. Two nonzero ideals $I$ and $J$ of $\mathcal{O}_K$ lie in the same class exactly when there are nonzero $x, y \in \mathcal{O}_K$ with $(x)I = (y)J$, and the class of a nonzero ideal is trivial exactly when the ideal is principal.

The theorem states that the class group $\mathrm{Cl}(K)$ is finite. Its order is the class number $h_K$, which is therefore a positive integer.

A quantitative form gives a bound. Write $n = [K : \mathbb{Q}]$, let $r_2$ be the number of pairs of complex conjugate embeddings of $K$ into $\mathbb{C}$, let $d_K$ be the discriminant of $K$, and let the norm $N(I)$ of a nonzero ideal be the number of elements of $\mathcal{O}_K / I$. Then every ideal class contains a nonzero ideal $I$ with $N(I) \le M_K$, where $M_K$ is the Minkowski bound

\[M_K = \left(\frac{4}{\pi}\right)^{r_2} \frac{n!}{n^n} \sqrt{|d_K|}.\]

Examples

The rationals. Here $\mathcal{O}_K = \mathbb{Z}$ is a principal ideal domain, and the class number of $\mathbb{Q}$ is $1$.
The Gaussian integers. For $K = \mathbb{Q}(i)$ one has $\mathcal{O}_K = \mathbb{Z}[i]$, $n = 2$, $r_2 = 1$ and $d_K = -4$, so $M_K = 4/\pi < 2$. Every class then contains an ideal of norm $1$, which is $\mathcal{O}_K$ itself, and $h_K = 1$.
A class number two. For $K = \mathbb{Q}(\sqrt{-5})$ one has $\mathcal{O}_K = \mathbb{Z}[\sqrt{-5}]$ and $d_K = -20$, so $M_K = 4\sqrt{5}/\pi \approx 2.85$. The prime $2$ ramifies: $(2) = \mathfrak{p}^2$ with $\mathfrak{p} = (2, 1 + \sqrt{-5})$, the only ideal of norm $2$. It is not principal, since $a^2 + 5b^2 = 2$ has no integer solutions. Hence $\mathrm{Cl}(K)$ has order $2$. The two factorizations $6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5})$ into irreducibles reflect this.
Cyclotomic fields. The Minkowski bound shows that the ring of integers of the field generated over $\mathbb{Q}$ by a primitive cube root of unity is a principal ideal domain, and that the same holds for a primitive fifth root of unity.

Consequences

Principal ideal domains. The class number $h_K$ equals $1$ exactly when $\mathcal{O}_K$ is a principal ideal domain. A Dedekind domain is a unique factorization domain exactly when it is a principal ideal domain, so $h_K = 1$ also characterizes unique factorization of elements in $\mathcal{O}_K$.
A discriminant criterion. If $|d_K| < \left(2 (\pi/4)^{r_2} n^n / n!\right)^2$, then $\mathcal{O}_K$ is a principal ideal domain. The condition says $M_K < 2$, so every class contains an ideal of norm $1$.
Powers of ideals. By Lagrange's theorem in $\mathrm{Cl}(K)$, the power $I^{h_K}$ of every nonzero ideal $I$ is principal. In the other direction, if $m$ is a positive integer coprime to $h_K$ and $I^m$ is principal, then $I$ is principal.

Proof

The classical argument uses the geometry of numbers. Embed $K$ in $\mathbb{R}^{r_1} \times \mathbb{C}^{r_2}$, where $r_1$ counts the real embeddings; a nonzero ideal becomes a lattice whose covolume is proportional to its norm. Minkowski's theorem applied to a suitable convex body shows that every nonzero ideal $I$ contains a nonzero $a$ with $|N_{K/\mathbb{Q}}(a)| \le M_K\,N(I)$.

Given a class $C$, pick a nonzero ideal $I$ in the inverse class $C^{-1}$ and such an element $a \in I$. In a Dedekind domain an ideal containing $(a)$ divides it, so $(a) = IJ$ for some ideal $J$, which lies in $C$. The norm is multiplicative and $N((a)) = |N_{K/\mathbb{Q}}(a)|$, so $N(J) \le M_K$.

It remains to see that only finitely many ideals have norm at most $M_K$. An ideal of norm $m$ contains $m$, so it divides $(m)$, which has only finitely many ideal divisors. In general, a Dedekind domain whose quotients by nonzero ideals are all finite has only finitely many ideals of norm at most a given integer, and $\mathcal{O}_K$ is such a ring. Every class contains one of these finitely many ideals, so there are finitely many classes.

The Dirichlet class number formula expresses the residue at $s = 1$ of the Dedekind zeta function of $K$ in terms of $h_K$, the regulator, the number of roots of unity, $r_1$, $r_2$ and $d_K$.
Function fields. The same finiteness holds for the integral closure of $\mathbb{F}_q[t]$ in a finite separable extension $F$ of the rational function field $\mathbb{F}_q(t)$, and Mathlib defines the class number of such a function field as the order of that class group. This number depends on the choice of $t$, and in general differs from the class number of $F$ defined through divisor classes of degree zero.

In Mathlib

Mathlib defines the class group of any integral domain as the group of invertible fractional ideals of the domain (inside its field of fractions) modulo the principal ones. In a Dedekind domain every nonzero fractional ideal is invertible, so this is the usual group. Finiteness is recorded as a noncomputable finiteness structure on the class group, a finite set that contains every class, and the class number is defined as the cardinality of that set. The proof does not go through the Minkowski bound. It applies a general theorem: the integral closure of a Euclidean domain in a finite separable extension of its fraction field has finite class group, provided the domain is infinite and carries an integer-valued absolute value, compatible with the Euclidean division, with a suitable approximation property (called admissible). The integers with the usual absolute value give the number field case, and polynomials over a finite field with an absolute value based on the degree give the function field case. The Minkowski bound is proved separately, through the geometry of numbers, and serves as a tool for showing that particular rings of integers are principal ideal domains.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibNumberField.RingOfIntegers.instFintypeClassGroup

Uses 5 · Used by 1

Statement usesIdeal of a commutative ring · Fractional ideal · Quotient group · Prime ideal

Proof usesMinkowski’s Fundamental Theorem

Used byDirichlet class number formula

TheoremDirichlet unit theorem #

The Dirichlet unit theorem describes the group of units of the ring of integers of a number field: it is the product of the finite cyclic group of roots of unity in the field and a free abelian group whose rank is determined by how the field embeds into the complex numbers. It is one of the two basic finiteness results of algebraic number theory, alongside the finiteness of the class number, and the size of the units, measured by the regulator, enters the class number formula.

Statement

Let $K$ be a number field, a field of finite degree $n$ over $\mathbb{Q}$, and let $\mathcal{O}_K$ be its ring of integers, the elements of $K$ that are roots of monic polynomials with integer coefficients. Of the $n$ field embeddings $K \to \mathbb{C}$, say $r_1$ land in $\mathbb{R}$ and the remaining $2r_2$ come in complex-conjugate pairs, so that $r_1 + 2r_2 = n$. Each real embedding, and each conjugate pair, gives an absolute value $|\cdot|_w$ on $K$, called an infinite place; there are $r_1 + r_2$ of them. Put

\[r = r_1 + r_2 - 1.\]

The roots of unity in $K$ all lie in $\mathcal{O}_K$ and form a finite cyclic group $\mu_K$. The theorem says that there are units $\varepsilon_1, \dots, \varepsilon_r$ of $\mathcal{O}_K$, a fundamental system of units, such that every unit $u$ can be written in exactly one way as

\[u = \zeta\, \varepsilon_1^{a_1} \cdots \varepsilon_r^{a_r}, \qquad \zeta \in \mu_K,\ a_1, \dots, a_r \in \mathbb{Z}.\]

Mathlib chooses a particular fundamental system and proves that every unit is uniquely a root of unity times a product of integer powers of its members. In group-theoretic terms, $\mathcal{O}_K^\times \cong \mu_K \times \mathbb{Z}^r$: the unit group is finitely generated, its torsion subgroup is $\mu_K$, and the quotient by $\mu_K$ has rank $r$, in line with the structure theorem for finitely generated abelian groups.

Examples

The rationals. For $K = \mathbb{Q}$ we have $r_1 = 1$, $r_2 = 0$ and $r = 0$, and indeed the only units of its ring of integers $\mathbb{Z}$ are $1$ and $-1$.
Imaginary quadratic fields. Here $r_1 = 0$, $r_2 = 1$ and $r = 0$, so there are only finitely many units: $\pm 1, \pm i$ in the Gaussian integers, the six sixth roots of unity in $\mathbb{Z}[\tfrac{1 + \sqrt{-3}}{2}]$, and just $\pm 1$ in every other case.
Real quadratic fields. Here $r_1 = 2$ and $r = 1$. For $K = \mathbb{Q}(\sqrt 2)$ the ring of integers is $\mathbb{Z}[\sqrt 2]$, and the units are exactly the numbers $\pm(1 + \sqrt 2)^k$ with $k \in \mathbb{Z}$. An element $a + b\sqrt 2$ is a unit exactly when its norm $a^2 - 2b^2$ is $\pm 1$, an instance of the general criterion that an algebraic integer is a unit if and only if its norm has absolute value $1$.
A cubic field. For $K = \mathbb{Q}(\sqrt[3]{2})$, with $r_1 = 1$ and $r_2 = 1$, the rank is again $1$; the identity $(\sqrt[3]{2} - 1)(\sqrt[3]{4} + \sqrt[3]{2} + 1) = 1$ exhibits a unit of infinite order. Since the degree is odd, the only roots of unity in $K$ are $1$ and $-1$.
Cyclotomic fields. For a prime $p \ge 3$, the field $\mathbb{Q}(\zeta_p)$ has no real embeddings and degree $p - 1$, so $r = \tfrac{p-1}{2} - 1 = \tfrac{p-3}{2}$.

Proof

Write $d_w$ for $1$ when $w$ is real and $2$ when it is complex, and send a unit $u$ to its logarithm vector $\ell(u) = \big(d_w \log |u|_w\big)_w$ in $\mathbb{R}^{r_1 + r_2}$. This is a group homomorphism from multiplication to addition. A unit has norm $\pm 1$, so the coordinates of $\ell(u)$ sum to zero, and the image lies in a hyperplane of dimension $r$.

The kernel is finite: a unit is a root of unity exactly when $|u|_w = 1$ at every infinite place, and since the minimal polynomial of an element of $\mathcal{O}_K$ has integer coefficients, degree at most $n$, and coefficients bounded in terms of the absolute values $|\cdot|_w$ of the element, only finitely many elements of $\mathcal{O}_K$ have all $|\cdot|_w$ bounded. The same bound shows that every ball meets the image in finitely many points, so the image is a discrete subgroup of the hyperplane, hence a free abelian group of rank at most $r$.

The main step is that the image spans the hyperplane. Using Minkowski's theorem on lattice points in convex bodies, one builds a sequence of nonzero algebraic integers of bounded norm that shrink at every place except a chosen one; since only finitely many ideals of $\mathcal{O}_K$ have norm below a given bound, two of them generate the same principal ideal, and their quotient is a unit. Thus, for each infinite place $w_1$ there is a unit $u$ with $\log |u|_w < 0$ at every place $w \neq w_1$. A determinant estimate shows that $r$ of these vectors are linearly independent. The image is therefore a lattice of rank exactly $r$, and lifting a basis of it to units gives a fundamental system.

Consequences

Generation. The fundamental units together with the roots of unity generate the whole unit group.
The regulator. Delete one coordinate from the logarithm vectors of a fundamental system; the absolute value of the determinant of the resulting $r \times r$ matrix is the regulator of $K$. It depends neither on the fundamental system nor on the deleted coordinate, and it is strictly positive.
Pell's equation. For a positive integer $d$ that is not a square, the solutions of $x^2 - dy^2 = 1$ are the units of norm $1$ in $\mathbb{Z}[\sqrt d]$, and the same rank-one phenomenon appears: every solution is, up to sign, an integer power of the fundamental solution, the one with $x > 1$, $y > 0$ and $x$ least.

In Mathlib

Mathlib works with the unit group of the ring of integers of any field that is a number field. The roots of unity are its torsion subgroup, the units of finite order. The rank is defined as the number of infinite places minus one, and a separate result shows that the number of infinite places is $r_1 + r_2$, while $r_1 + 2r_2$ is the degree. The logarithmic embedding in the proof drops one distinguished place, so it lands in $\mathbb{R}^r$ rather than in a hyperplane of $\mathbb{R}^{r_1 + r_2}$. The quotient of the units by the roots of unity is treated as a module over the integers; Mathlib picks a basis of it, and its fundamental system consists of arbitrary lifts of the basis elements. The uniqueness statement refers to that chosen system, not to every fundamental system.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibNumberField.Units.exist_unique_eq_mul_prod

Uses 11 · Used by 1

Statement usesField · Complex number · Group · Cyclic group · Polynomial in one indeterminate

Proof usesLogarithm · Minkowski’s Fundamental Theorem · Basis · Minimal polynomial · Ideal of a commutative ring · Determinant

Used byDirichlet class number formula

TheoremDirichlet class number formula #

The Dirichlet class number formula, also called the analytic class number formula, expresses the behaviour of the Dedekind zeta function of a number field near $s = 1$ in terms of the field's basic arithmetic invariants: its class number, regulator, number of roots of unity, discriminant and numbers of real and complex places. It ties an analytic quantity to algebraic ones, and is the main route by which the class number, which is defined algebraically, can be computed or estimated with analysis. Through it, the positivity of these invariants yields the nonvanishing of Dirichlet $L$-functions at $s = 1$, the key input to Dirichlet's theorem on primes in arithmetic progressions.

Statement

Let $K$ be a number field of degree $n$ over $\mathbb{Q}$ with ring of integers $\mathcal{O}_K$. The norm of a nonzero ideal $I$ of $\mathcal{O}_K$ is the size of the finite quotient ring $\mathcal{O}_K / I$. The Dedekind zeta function of $K$ is the Dirichlet series $\zeta_K(s) = \sum_{m \ge 1} a_m m^{-s}$, where $a_m$ is the number of ideals of $\mathcal{O}_K$ of norm $m$. It converges for complex $s$ with real part greater than $1$; for $K = \mathbb{Q}$ it agrees there with the Riemann zeta function.

The formula involves the following invariants of $K$.

$r_1$ is the number of real places and $r_2$ the number of complex places of $K$. Each field embedding $\sigma : K \to \mathbb{C}$ defines an absolute value $|x|_v = |\sigma(x)|$ on $K$, and an infinite place $v$ is an absolute value arising in this way. An embedding and its complex conjugate give the same place; the place is real when $\sigma$ maps $K$ into $\mathbb{R}$ and complex otherwise, so complex places correspond to pairs of conjugate non-real embeddings and $r_1 + 2r_2 = n$.
$h_K$ is the class number, the order of the ideal class group, which is finite; $h_K = 1$ exactly when $\mathcal{O}_K$ is a principal ideal domain.
$R_K$ is the regulator. By the Dirichlet unit theorem, there are units $\varepsilon_1, \dots, \varepsilon_r$ of $\mathcal{O}_K$, where $r = r_1 + r_2 - 1$, such that every unit is uniquely a root of unity times a product $\varepsilon_1^{k_1} \cdots \varepsilon_r^{k_r}$ with integer exponents; these form a system of fundamental units. Fix one infinite place $v_0$. Then $R_K$ is the absolute value of the determinant of the $r \times r$ matrix with entries $n_v \log |\varepsilon_i|_v$, where $v$ runs over the infinite places other than $v_0$, and $n_v$ is $1$ for a real place and $2$ for a complex place. The value depends neither on the system of fundamental units nor on the choice of $v_0$.
$w_K$ is the number of roots of unity in $K$, that is, the order of the torsion subgroup of the unit group of $\mathcal{O}_K$.
$d_K$ is the discriminant of $K$, the discriminant of an integral basis of $\mathcal{O}_K$.

With these, $(s - 1)\zeta_K(s)$ tends to the following constant as the real number $s$ decreases to $1$:

\[\lim_{s \to 1^+} (s - 1)\,\zeta_K(s) = \frac{2^{r_1} (2\pi)^{r_2}\, h_K\, R_K}{w_K \sqrt{|d_K|}}.\]

The constant on the right-hand side is strictly positive, so $\zeta_K(s)$ tends to infinity as $s \to 1^+$.

Examples

The rational numbers. Here $r_1 = 1$, $r_2 = 0$, $h_K = 1$, $R_K = 1$, $w_K = 2$ and $d_K = 1$, so the right-hand side is $1$. This matches the fact that the Riemann zeta function satisfies $(s - 1)\zeta(s) \to 1$ as $s \to 1$ in the complex plane.
Quadratic fields. If $K$ is quadratic with discriminant $d = d_K$, then $\zeta_K(s) = \zeta(s)\,L(s, \chi_d)$. Here, for a Dirichlet character $\chi$, the Dirichlet $L$-function is $L(s, \chi) = \sum_{m \ge 1} \chi(m) m^{-s}$, and $\chi_d(m)$ is the Kronecker symbol $(d/m)$, a character modulo $|d|$. Comparing limits at $s = 1$ gives, for $d < 0$ (where $r_2 = 1$ and $R_K = 1$), $$h_K = \frac{w_K \sqrt{|d|}}{2\pi}\, L(1, \chi_d),$$ and, for $d > 0$ (where $r_1 = 2$ and $R_K = \log \varepsilon$ for the fundamental unit $\varepsilon > 1$), $$h_K = \frac{\sqrt{d}}{2 \log \varepsilon}\, L(1, \chi_d).$$
Gaussian rationals. For $K = \mathbb{Q}(i)$ one has $d_K = -4$, $w_K = 4$ and $h_K = 1$, so $L(1, \chi_{-4}) = 1 - \tfrac13 + \tfrac15 - \tfrac17 + \cdots = \pi/4$, the Leibniz series.
The field $\mathbb{Q}(\sqrt2)$. Here $d_K = 8$, $h_K = 1$ and $\varepsilon = 1 + \sqrt2$, which gives $1 - \tfrac13 - \tfrac15 + \tfrac17 + \tfrac19 - \cdots = \log(1 + \sqrt2)/\sqrt2$.

Proof

The argument has a counting part and an analytic part.

Counting ideals. The ideal class group is the group of nonzero fractional ideals of $\mathcal{O}_K$ modulo the principal ones, so each class contains integral ideals. Fix an ideal class $C$ and an integral ideal $J$ in the inverse class. Multiplication by $J$ matches the integral ideals $I$ in $C$ with the principal ideals $(\alpha)$ divisible by $J$, and $|N(\alpha)| = N(I)\,N(J)$. Principal ideals correspond to nonzero elements of $J$ up to multiplication by units. Embedding $K$ into $\mathbb{R}^{r_1} \times \mathbb{C}^{r_2}$ turns $J$ into a lattice, and the unit theorem provides a cone that is a fundamental domain for the action of the units modulo roots of unity, so that each principal ideal has exactly $w_K$ generators in the cone. Counting lattice points in the part of this cone where the norm is at most $t$, a region that scales with $t$, and comparing with its volume shows that the number of nonzero ideals in $C$ of norm at most $t$, divided by $t$, tends to $2^{r_1}(2\pi)^{r_2} R_K / (w_K \sqrt{|d_K|})$ as $t \to \infty$. The limit does not depend on $C$, so ideals are equidistributed among the classes. Summing over the $h_K$ classes, the number of nonzero ideals of norm at most $t$, divided by $t$, tends to the right-hand side of the formula.

From counting to the zeta function. Partial summation writes a Dirichlet series with partial sums $A(t) = \sum_{m \le t} a_m$ as $\sum a_m m^{-s} = s \int_1^\infty A(t)\, t^{-s-1}\, dt$ for real $s > 1$. If $A(t)$ is close to $\ell t$, the integral is close to $\ell s / (s - 1)$. This gives the general fact that if the coefficients are nonnegative real numbers and $(a_1 + \cdots + a_m)/m \to \ell$ as $m \to \infty$, then $(s - 1)\sum a_m m^{-s} \to \ell$ as the real number $s$ decreases to $1$. Applied to the ideal counts, it yields the formula.

Consequences and generalizations

Nonvanishing of $L(1, \chi)$. The Dedekind zeta function of the cyclotomic field $\mathbb{Q}(\zeta_m)$ is, up to finitely many Euler factors, the product of the Dirichlet $L$-functions of the characters modulo $m$. The factor of the trivial character has a simple pole at $s = 1$, and the left-hand side has a finite positive limit after multiplying by $s - 1$. Since the other factors are analytic at $s = 1$, none of them can vanish there. This is the analytic heart of Dirichlet's theorem.
Class number computations. The quadratic formulas above, combined with evaluations of $L(1, \chi_d)$ as finite sums, give a finite formula for the class number of an imaginary quadratic field, and for the product $h_K \log \varepsilon$ for a real quadratic field.
The point $s = 0$. Through the functional equation of $\zeta_K$, the formula is equivalent to the statement that $\zeta_K$ has a zero of order $r_1 + r_2 - 1$ at $s = 0$ with leading coefficient $-h_K R_K / w_K$.

In Mathlib

Mathlib states the formula for an arbitrary number field. It defines the Dedekind zeta function only by its Dirichlet series, as a function of a complex variable, following the library's convention that an $L$-series takes the value $0$ where it does not converge absolutely; it does not construct the analytic continuation. For this reason the formula is phrased as a one-sided limit of $(s - 1)\zeta_K(s)$ as the real number $s$ decreases to $1$, rather than as the residue of a meromorphic function. The limiting value is a separate definition written out in the six invariants above. The regulator is defined as the covolume of the lattice of logarithms of units. Mathlib fixes one system of fundamental units, and for that system and any choice of the omitted place $v_0$, the regulator is the absolute value of the determinant described above. The class number is the cardinality of the class group, and $r_1$ and $r_2$ are defined as numbers of infinite places.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibNumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT

Uses 8

Statement usesIdeal of a commutative ring · Finiteness of the class number · Dirichlet unit theorem · Determinant · Logarithm · Limit of a map with respect to filters

Proof usesFractional ideal · Lebesgue measure (Measures and integral calculus)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Algebraic Number Theory

InstanceFiniteness of the class number#

Statement

Examples

Consequences

Proof

Related concepts

In Mathlib

Sources

TheoremDirichlet unit theorem#

Statement

Examples

Proof

Consequences

In Mathlib

Sources

TheoremDirichlet class number formula#

Statement

Examples

Proof

Consequences and generalizations

In Mathlib

Sources

InstanceFiniteness of the class number #

TheoremDirichlet unit theorem #

TheoremDirichlet class number formula #