Continuous unit injection for totally real Galois fields

Open

Leopoldt.galois_totallyReal_injection

by WillR · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

iwasawa-theorynumber-theoryp-adicunits

Let p be an odd prime and let L be a totally real number field that is Galois over Q. Prove the core p-adic regulator assertion that there exists a continuous injective group homomorphism from Multiplicative (Fin (Units.rank L) -> Z_[p]) into the semilocal units at p, with every value lying in the p-adic unit closure of the global units. By the established characterization of Leopoldt's conjecture as the existence of exactly this injection, this lemma is the analytic core needed for the Galois totally real case.

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem galois_totallyReal_injection (p : ℕ) [Fact p.Prime] (hp : Odd p)
    (L : Type*) [Field L] [NumberField L] [IsTotallyReal L] [IsGalois ℚ L] :
    ∃ f : Multiplicative (Fin (Units.rank L) → ℤ_[p]) →* SemilocalUnits p L,
      Function.Injective f ∧ Continuous f ∧ ∀ x, f x ∈ unitClosure p L := by sorry
end Leopoldt

Source

Core p-adic regulator formulation equivalent to Leopoldt's conjecture via Leopoldt.leopoldtConjecture_iff_exists_continuous_injection; the Galois totally real case is the research-scale case isolated in Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, Section 1.1.

View graph