Dirichlet's unit theorem

Remarks

The proof uses the logarithmic embedding $u \mapsto \big(N_j \log \abs{\sigma_j(u)}\big)_j$ into $\R^{r_1 + r_2}$, where $\sigma_j$ runs over the real embeddings and one embedding from each complex pair, and $N_j$ is $1$ or $2$. Its kernel on $\mathcal{O}_K^\times$ is the finite group $\mu(K)$, and its image lies in the hyperplane where the coordinates sum to $0$. The hard part is that the image is a full lattice in that hyperplane; this uses Minkowski's theorem to produce enough units.

A set of $r = r_1 + r_2 - 1$ units that generate $\mathcal{O}_K^\times$ modulo $\mu(K)$ is a system of fundamental units.

Example: for $K = \Q(\sqrt{2})$, $r_1 = 2$ and $r_2 = 0$, so the rank is $1$. The units of $\Z[\sqrt{2}]$ are exactly $\pm (1 + \sqrt{2})^k$ with $k \in \Z$. For an imaginary quadratic field, $r_1 = 0$ and $r_2 = 1$, so the rank is $0$ and every unit is a root of unity; for $\Q(i)$ the units are $\pm 1, \pm i$.

Going deeper

For a student

The theorem is one of the two finiteness results at the start of algebraic number theory, with the finiteness of the class number. In terms of free abelian groups, $\mathcal{O}_K^\times / \mu(K)$ is free of rank $r_1 + r_2 - 1$. The covolume of the unit lattice is the regulator, which enters the class number formula. For real quadratic fields, the fundamental unit gives the solutions of Pell's equation.