Upper bound for the Leopoldt defect in a finite extension

Proved

Leopoldt.defect_le_defect_add_rank_sub

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

leopoldtnumber-theory

Let $p$ be a prime and $K/F$ a finite extension of number fields, with unit ranks $r_F = \mathbb{Z}\text{-rk}(E_F)$ and $r_K$ . Then

\mathcal{D}_L(K) \le \mathcal{D}_L(F) + (r_K - r_F).

This follows because the $\mathbb{Z}_p$ -rank of the $p$ -adic closure $\overline{E}$ of the units can only increase from $F$ to $K$ (the map of semilocal units $U_F \to U_K$ is continuous and injective and carries $\overline{E}_F$ into $\overline{E}_K$ ), and $r_F \le r_K$ . (Here the subtraction $r_K - r_F$ is honest since $r_F \le r_K$ .)

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem defect_le_defect_add_rank_sub (p : ℕ) [Fact p.Prime]
    (F K : Type*) [Field F] [NumberField F] [Field K] [NumberField K]
    [Algebra F K] [FiniteDimensional F K] :
    defect p K ≤ defect p F + (Units.rank K - Units.rank F) := by sorry
end Leopoldt

Source

P. Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, §1, Remark 1.A (Leopoldt defect does not decrease in finite extensions); M. Laurent, Rang p-adique d'unités et action de groupes, J. reine angew. Math. 399 (1989), 81–108, Introduction. Complementary to Remark 1.A: the defect grows by at most the growth of the unit rank.

View graph