A norm-compatible ring homomorphism commutes with the $p$ -adic logarithm

Proved

PadicLog.map_log

by ebayuser · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnumber-theoryp-adic

Let $p$ be a prime and let $K$ and $K'$ be complete non-archimedean (ultrametric) nontrivially normed fields of characteristic zero in which $\|p\| < 1$ . On the ball $\|x - 1\| \le \|p\|^2$ the $p$ -adic logarithm is defined by Iwasawa's limit

\log_p x = \lim_{n \to \infty} \frac{x^{p^n} - 1}{p^n}.

Let $\iota : K \to K'$ be a ring homomorphism and suppose there is a real $c > 0$ with

\|\iota(y)\|_{K'} = \|y\|_K^{\,c} \quad \text{for all } y \in K.

Then for every $x$ in the ball $\|x - 1\|_K \le \|p\|_K^2$ ,

\iota\bigl(\log_p x\bigr) = \log_p\bigl(\iota(x)\bigr).

The proof is formal: $\iota$ is continuous because of the norm relation, it carries each approximant $(x^{p^n} - 1)/p^n$ to the corresponding approximant of $\iota(x)$ because it is a ring homomorphism fixing $p$ , and $\iota(x)$ lies in the ball of $K'$ because $\|\iota(x) - 1\| = \|x - 1\|^c \le (\|p\|_K^2)^c = \|p\|_{K'}^2$ ; so both sides are the limit of the same sequence.

Use. Together with Leopoldt.exists_primesOver_ringHom_adicCompletion this lets one compute the $p$ -adic logarithm of an element of a completion $K_v$ inside a larger completion $L_w$ ; it is the lemma that a proof of Leopoldt.charSum_log_ne_zero_of_brumer needs to pass from $\iota(\log_p \sigma\varepsilon)$ to $\log_p$ taken in $L_w$ , where Brumer's theorem for $L$ applies.

Formalization Note. PadicLog.log is the limUnder of the sequence PadicLog.logSeq; the hypotheses on $K$ and $K'$ are those of Definitions.Def_PadicLog (NontriviallyNormedField, IsUltrametricDist, CompleteSpace, Fact (‖(p : K)‖ < 1), CharZero). The exponent is ‖x‖ ^ c with real c (real power). The relevant platform lemmas are PadicLog.tendsto_logSeq and PadicLog.norm_p_pos.

Preamble

import Definitions.Def_PadicLog

Formal statement

theorem PadicLog.map_log {p : ℕ} [Fact p.Prime]
    {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    [Fact (‖((p : ℕ) : K)‖ < 1)] [CharZero K]
    {K' : Type*} [NontriviallyNormedField K'] [IsUltrametricDist K'] [CompleteSpace K']
    [Fact (‖((p : ℕ) : K')‖ < 1)] [CharZero K']
    (ι : K →+* K') {c : ℝ} (hc : 0 < c) (hι : ∀ x, ‖ι x‖ = ‖x‖ ^ c)
    {x : K} (hx : ‖x - 1‖ ≤ ‖((p : ℕ) : K)‖ ^ 2) :
    ι (PadicLog.log (p := p) x) = PadicLog.log (p := p) (ι x) := by sorry

Source

Elementary consequence of the definition

\log_p x = \lim_n (x^{p^n} - 1)/p^n

(Iwasawa's limit formula for the

p

-adic logarithm on principal units), as formalized in `Definitions.Def_PadicLog` (`PadicLog.log`, `PadicLog.tendsto_logSeq`). A continuous ring homomorphism fixing

p

preserves the approximants and hence the limit.

View graph

A norm-compatible ring homomorphism commutes with the ppp-adic logarithm

A norm-compatible ring homomorphism commutes with the $p$ -adic logarithm