Brumer's theorem: Leopoldt's conjecture for abelian extensions of $\mathbb{Q}$

The declaration asserts a single equation between natural numbers, under four blocks of hypotheses. Its data are: a natural number $p$, together with the assumption that $p$ is prime (supplied as an instance, so it is a genuine hypothesis: nothing else is assumed about $p$ — in particular $p = 2$ is allowed); and a type $K$ carrying (i) a field structure, (ii) the assumption that $K$ is a number field, i.e. $K$ has characteristic zero and is finite-dimensional over $\mathbb{Q}$ via the canonical $\mathbb{Q}$-algebra structure, (iii) the assumption that the extension $K/\mathbb{Q}$ is Galois, which in Mathlib's formulation means it is both separable (automatic here, as the characteristic is zero) and normal, and (iv) the assumption that the group $\operatorname{Aut}_{\mathbb{Q}}(K)$ of $\mathbb{Q}$-algebra automorphisms of $K$ is commutative as a multiplicative structure, i.e. $\sigma\tau = \tau\sigma$ for all $\sigma,\tau \colon K \xrightarrow{\ \sim\ } K$ fixing $\mathbb{Q}$. Hypotheses (iii) and (iv) together are the assertion that $K/\mathbb{Q}$ is an abelian extension; they are stated as two separate assumptions, and (iv) alone is a statement about the automorphism group of $K$ over $\mathbb{Q}$ with no normality built in. There is no hypothesis relating $p$ to $K$ in any way (no ramification, splitting, or degree condition), and no hypothesis excluding the case $K = \mathbb{Q}$, which satisfies all four (its automorphism group is trivial).

The conclusion is the equation

$$\mathcal{D}(p, K) \;=\; 0,$$

where $\mathcal{D}(p,K)$ — the quantity named "defect" in the accompanying definitions — is the natural number

$$\mathcal{D}(p,K) \;=\; r(K) \;\dot-\; \rho\bigl(p,\ [K:\mathbb{Q}],\ \bar{E}(p,K)\bigr),$$

with $\dot-$ denoting truncated subtraction of natural numbers (the value is $0$ whenever the subtrahend is at least the minuend, never negative). The three ingredients unfold as follows.

$r(K)$, the global unit rank. This is Mathlib's unit rank of $K$, defined as

$$r(K) \;=\; \#\{\text{infinite places of } K\} \;\dot-\; 1,$$

again with truncated subtraction; since the number of infinite places is $r_1 + r_2$ (real places plus complex places), $r(K) = r_1 + r_2 - 1$, the Dirichlet unit rank of $\mathcal{O}_K^{\times}$.

The semilocal units and the group $\bar{E}(p,K)$. Let

$$P \;=\; \{\,v \text{ a height-one prime of } \mathcal{O}_K \ :\ \text{the image of } p \text{ in } \mathcal{O}_K \text{ lies in } v\,\},$$

i.e. the nonzero prime ideals of the ring of integers of $K$ that contain $p$ — the primes above $p$ (the accompanying definitions also establish that this index set is finite, as a fact, not as a hypothesis). For $v \in P$ write $\mathcal{O}_v = \{x \in K_v : |x|_v \le 1\}$ for the valuation subring of the $v$-adic completion $K_v$ of $K$, and set

$$U \;=\; \prod_{v \in P} \mathcal{O}_v^{\times},$$

the product (formally, the type of dependent functions on $P$) of the local unit groups, with componentwise multiplication and the product topology; each factor $\mathcal{O}_v^{\times}$ carries the topology induced from $\mathcal{O}_v \subseteq K_v$ (with its valuation topology) through the map $u \mapsto (u, u^{-1})$. Let

$$\iota \colon \mathcal{O}_K^{\times} \longrightarrow U, \qquad \iota(u) \;=\; \bigl(\text{image of } u \text{ under } \mathcal{O}_K \to \mathcal{O}_v\bigr)_{v \in P}$$

be the diagonal group homomorphism given componentwise by the canonical algebra map. Then

$$\bar{E}(p,K) \;=\; \bigcap_{n \in \mathbb{N}} \Bigl(\ \iota\bigl(\mathcal{O}_K^{\times}\bigr) \ \vee\ \bigl\{\,u^{\,p^{\,n+1}} : u \in U \,\bigr\}\ \Bigr),$$

an intersection of subgroups of $U$, where $\vee$ is the join of subgroups (the subgroup generated by the union; since $U$ is commutative this join is the setwise product of the two subgroups). The exponents range over $p^1, p^2, p^3, \dots$, so this is $\bigcap_{m \ge 1} \iota(\mathcal{O}_K^{\times})\cdot U^{p^m}$. This is an entirely algebraic definition: no topological closure operator is applied, and $\bar{E}(p,K)$ is not asserted to be closed.

$\rho$, the bounded $\mathbb{Z}_p$-rank. For a commutative topological group $G$, a bound $b \in \mathbb{N}$ and a subgroup $H \le G$, the definition sets

$$\rho(p, b, H) \;=\; \sup\Bigl\{\, n \in \mathbb{N} \ :\ n \le b \ \text{ and } \ \exists\, f \colon \mathbb{Z}_p^{\,n} \to G \ \text{a group homomorphism with } f \text{ injective, } f \text{ continuous, and } f(x) \in H \text{ for every } x \,\Bigr\},$$

where $\mathbb{Z}_p^{\,n}$ means the group of $n$-tuples of $p$-adic integers under componentwise addition, written multiplicatively, carrying the product of the $p$-adic topologies (for $n = 0$ this is the trivial group). The condition on $f$ is: it is a monoid (hence group) homomorphism, injective, continuous for the topology of $G$, and its image is contained in $H$; $H$ is not required to be closed, and $f$ is not required to be a topological embedding or to have closed image. The set in question always contains $n = 0$ (via the trivial homomorphism) and is bounded above by $b$, so the supremum is attained and $\rho(p,b,H)$ is the largest such $n$, a natural number with $0 \le \rho(p,b,H) \le b$. In the defect this is applied with $G = U$, $H = \bar{E}(p,K)$, and $b = [K:\mathbb{Q}] = \dim_{\mathbb{Q}} K$; the bound $[K:\mathbb{Q}]$ is part of the definition and caps the value.

Net content of the conclusion. Because the outer subtraction is truncated, the equation $\mathcal{D}(p,K) = 0$ is equivalent to the inequality

$$r_1 + r_2 - 1 \;\le\; \max\Bigl\{\, n \le [K:\mathbb{Q}] \ :\ \exists \text{ a continuous injective homomorphism } \mathbb{Z}_p^{\,n} \to \textstyle\prod_{v \mid p} \mathcal{O}_v^{\times} \text{ with image inside } \bigcap_{m \ge 1} \iota(\mathcal{O}_K^{\times})\,U^{p^m} \,\Bigr\},$$

rather than to an equality of two independently computed ranks: the conclusion holds whenever the right-hand side is greater than or equal to the Dirichlet rank, and in particular it holds automatically whenever $r_1 + r_2 \le 1$ (e.g. $K = \mathbb{Q}$ or $K$ imaginary quadratic), where $r(K) = 0$ and the equation reads $0 \dot- \rho = 0$ regardless of $\rho$.