Residue characteristic $p$ at the primes above $p$ : $\|p\| < 1$ in $K_{\mathfrak{p}}$ , and the $\mathbb{Z}_p$ -module structure on its principal units

Definition

PrimesOverNorm

by WCoram · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

local-fieldsnumber-theoryp-adicunits

Let $K$ be a number field, $p$ a prime, and $\mathfrak{p} \mid p$ a prime of $\mathcal{O}_K$ , that is, a term of the platform's type Leopoldt.PrimesOver p K of primes above $p$ . The completion $K_\mathfrak{p}$ has residue characteristic $p$ , so in the absolute value of $K_\mathfrak{p}$

\|p\| < 1 .

This file records that fact as a typeclass instance (Fact (‖(p : K_𝔭)‖ < 1)), and makes $K_\mathfrak{p}$ a nontrivially normed field (Mathlib's scoped Valued.toNontriviallyNormedField, extending the existing normed-field structure on the completion). Together with Mathlib's ultrametric and completeness instances for $K_\mathfrak{p}$ , these are exactly the hypotheses of Definitions.Def_OneUnits, so the principal units

U_1(K_\mathfrak{p}) = \{u \in K_\mathfrak{p}^\times : \|u - 1\| < 1\}

of each completion at a prime above $p$ become a topological $\mathbb{Z}_p$ -module, and so does the product $\prod_{\mathfrak{p} \mid p} U_1(K_\mathfrak{p})$ inside the semilocal units $U_p(K) = \prod_{\mathfrak{p} \mid p} \mathcal{O}_\mathfrak{p}^\times$ of the mission's definition file.

Two lemmas restate Mathlib's NumberField.FinitePlace.norm_lt_one_iff_mem, which says that an algebraic integer has norm $< 1$ in $K_\mathfrak{p}$ exactly when it lies in $\mathfrak{p}$ : the natural number $p$ has norm $< 1$ when $\mathfrak{p} \mid p$ , and an algebraic integer $x \equiv 1 \pmod{\mathfrak{p}}$ satisfies $\|x - 1\| < 1$ in $K_\mathfrak{p}$ , i.e. maps to a principal unit. The second is how global units that are $\equiv 1$ modulo every prime above $p$ land in $\prod_{\mathfrak{p} \mid p} U_1(K_\mathfrak{p})$ .

Formalization Note Adapted from FormalConjecturesForMathlib/NumberTheory/NumberField/PrimesAbove.lean of the Formal Conjectures project (Apache 2.0), by Chris Birkbeck, with its PrimesAbove K p replaced by the platform's Leopoldt.PrimesOver p K (the same subtype of the height-one spectrum). The Fact instance is keyed on v : PrimesOver p K and applies to v.1.adicCompletion K.

Definition code

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import Definitions.Def_LeopoldtDefect
import Definitions.Def_OneUnits

/-!
# Residue characteristic of the completions at the primes above `p`

For a number field `K` and a prime `𝔭 ∣ p` of `𝓞 K` (a term of `Leopoldt.PrimesOver p K`), the
completion `K_𝔭` has residue characteristic `p`, so `‖p‖ < 1` there. This is recorded as a `Fact`
instance, which is what gives the principal units `oneUnits (K_𝔭)` of the completion their
`ℤ_[p]`-module structure `OneUnits.instModule` from `Definitions.Def_OneUnits`.

The completion `K_𝔭` is also made a `NontriviallyNormedField` (Mathlib's scoped instance
`Valued.toNontriviallyNormedField`, extending the existing `NormedField` instance), which together
with Mathlib's `IsUltrametricDist` and `CompleteSpace` instances is what `Def_OneUnits` needs.

The norm on `K_𝔭` detects congruences modulo `𝔭`: Mathlib's
`NumberField.FinitePlace.norm_lt_one_iff_mem` says an algebraic integer has norm `< 1` under the
embedding `K → K_𝔭` exactly when it lies in `𝔭`. The two lemmas restate this for `ℕ → K_𝔭` and
`𝓞 K → K_𝔭`; the second says that an integer congruent to `1` modulo `𝔭` maps to a principal unit.

Adapted from `FormalConjecturesForMathlib/NumberTheory/NumberField/PrimesAbove.lean` of the
Formal Conjectures project (Apache 2.0), by Chris Birkbeck, with `PrimesAbove K p` replaced by
the platform's `Leopoldt.PrimesOver p K` (the same subtype).
-/

open IsDedekindDomain NumberField

namespace IsDedekindDomain.HeightOneSpectrum

variable {K : Type*} [Field K] [NumberField K] (v : HeightOneSpectrum (𝓞 K))

theorem norm_natCast_lt_one {p : ℕ} (hv : (p : 𝓞 K) ∈ v.asIdeal) :
    ‖((p : ℕ) : v.adicCompletion K)‖ < 1 := by
  rw [← map_natCast' (algebraMap (𝓞 K) (adicCompletion K v)) rfl _]
  exact (NumberField.FinitePlace.norm_lt_one_iff_mem _ _ _).2 hv

theorem norm_algebraMap_sub_one_lt {x : 𝓞 K} (hx : x - 1 ∈ v.asIdeal) :
    ‖algebraMap (𝓞 K) (v.adicCompletion K) x - 1‖ < 1 := by
  rw [← map_one (algebraMap (𝓞 K) (v.adicCompletion K)), ← map_sub]
  exact (NumberField.FinitePlace.norm_lt_one_iff_mem K v _).2 hx

end IsDedekindDomain.HeightOneSpectrum

/-- The `v`-adic completion is a nontrivially normed field: this is Mathlib's scoped instance
`Valued.toNontriviallyNormedField`, made global, and extends the existing `NormedField`
instance on the completion. -/
noncomputable instance {K : Type*} [Field K] [NumberField K] (v : HeightOneSpectrum (𝓞 K)) :
    NontriviallyNormedField (v.adicCompletion K) :=
  Valued.toNontriviallyNormedField (v.adicCompletion K) (WithZero (Multiplicative ℤ))

namespace Leopoldt

/-- Each `K_𝔭` with `𝔭 ∣ p` has residue characteristic `p`. This instance gives the principal
units of `K_𝔭` their `ℤ_[p]`-module structure. -/
instance (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K] (v : PrimesOver p K) :
    Fact (‖((p : ℕ) : v.1.adicCompletion K)‖ < 1) :=
  ⟨v.1.norm_natCast_lt_one v.2⟩

end Leopoldt

Source

Preda Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544, Section 1.1, p. 3 (the primes P above p and the semilocal units U); standard fact that the completion at a prime above p has residue characteristic p (J. Neukirch, Algebraic Number Theory, Springer 1999, Chapter II, Section 8). Code: FormalConjecturesForMathlib/NumberTheory/NumberField/PrimesAbove.lean, Formal Conjectures project (Apache 2.0), author Chris Birkbeck; Mathlib's NumberField.FinitePlace.norm_lt_one_iff_mem.

View graph

Residue characteristic ppp at the primes above ppp: ∥p∥<1\|p\| < 1∥p∥<1 in KpK_{\mathfrak{p}}Kp​, and the Zp\mathbb{Z}_pZp​-module structure on its principal units

Residue characteristic $p$ at the primes above $p$ : $\|p\| < 1$ in $K_{\mathfrak{p}}$ , and the $\mathbb{Z}_p$ -module structure on its principal units