The diagonal embedding $\iota : E \to U$ is injective

Proved

Leopoldt.diagonalUnits_injective

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

leopoldtnumber-theory

Let $K$ be a number field and $p$ a prime. The diagonal map

\iota : \mathcal{O}_K^\times \longrightarrow U = \prod_{\wp \mid p} \mathcal{O}_\wp^\times

from the global units into the semilocal units at $p$ is injective.

This holds because there is at least one prime $\wp$ above $p$ and the completion map $K \to K_\wp$ is an injective field homomorphism.

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem diagonalUnits_injective (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K] :
    Function.Injective (diagonalUnits p K) := by sorry
end Leopoldt

Source

P. Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, Section 1.1 (the diagonal embedding iota : K -> K_p); mission definition file Def_LeopoldtDefect (diagonalUnits)

View graph

The diagonal embedding ι:E→U\iota : E \to Uι:E→U is injective

The diagonal embedding $\iota : E \to U$ is injective