Galois equivariance of the semilocal $p$ -adic logarithm

Proved

Leopoldt.log_semilocalGaloisAut

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

galoisleopoldtnumber-theoryp-adic

Let $K$ be a number field, $p$ a prime and $\sigma\in\operatorname{Aut}(K/\mathbb{Q})$ . The automorphism $\sigma$ permutes the primes above $p$ and induces isomorphisms of completed fields $\sigma_w:K_{\sigma^{-1}w}\xrightarrow{\ \sim\ }K_w$ ; the Galois action on the semilocal units $U=\prod_{v\mid p}\mathcal{O}_v^\times$ is $(\sigma\cdot x)_w=\sigma_w(x_{\sigma^{-1}w})$ (Leopoldt.semilocalGaloisAut).

Theorem. Let $x\in U$ and $w\mid p$ , and assume that the component $x_{\sigma^{-1}w}$ is a principal unit, $\|x_{\sigma^{-1}w}-1\|<1$ . Then

\log_p\bigl((\sigma\cdot x)_w\bigr)=\sigma_w\bigl(\log_p x_{\sigma^{-1}w}\bigr).

In other words the componentwise $p$ -adic logarithm $U^{(1)}\to\prod_{v\mid p}K_v$ on principal semilocal units intertwines the Galois action on $U$ with the action $(\sigma\cdot y)_w=\sigma_w(y_{\sigma^{-1}w})$ on $\prod_{v\mid p}K_v=K\otimes_{\mathbb{Q}}\mathbb{Q}_p$ . Consequently the logarithmic image of a Galois-stable group of principal semilocal units is a $\mathbb{Z}_p[G]$ -submodule. The logarithm is $\log_p y=\lim_n (y^{p^n}-1)/p^n$ .

Preamble

import Definitions.Def_LeopoldtGaloisAction
import Definitions.Def_PadicLog

open NumberField

Formal statement

theorem Leopoldt.log_semilocalGaloisAut (p : ℕ) [Fact p.Prime] (K : Type*) [Field K]
    [NumberField K] (σ : K ≃ₐ[ℚ] K) (x : Leopoldt.SemilocalUnits p K)
    (w : Leopoldt.PrimesOver p K)
    (hx : ‖((x ((Leopoldt.primesOverPerm p K σ).symm w) :
        ((Leopoldt.primesOverPerm p K σ).symm w).1.adicCompletionIntegers K) :
        ((Leopoldt.primesOverPerm p K σ).symm w).1.adicCompletion K) - 1‖ < 1) :
    PadicLog.log (p := p)
        ((Leopoldt.semilocalGaloisAut p K σ x w : w.1.adicCompletionIntegers K) :
          w.1.adicCompletion K) =
      Leopoldt.GaloisAction.localRingEquiv σ (Leopoldt.valuation_primesOverPerm_symm p K σ w)
        (PadicLog.log (p := p)
          ((x ((Leopoldt.primesOverPerm p K σ).symm w) :
            ((Leopoldt.primesOverPerm p K σ).symm w).1.adicCompletionIntegers K) :
            ((Leopoldt.primesOverPerm p K σ).symm w).1.adicCompletion K)) := by sorry

Source

L. C. Washington, Introduction to Cyclotomic Fields, 2nd ed., GTM 83, §5.5 (the Galois action on the p-adic logarithms of units, used for the p-adic regulator and Brumer's theorem); J. Neukirch, Algebraic Number Theory, Ch. II §8 (action of automorphisms on completions).

View graph

Galois equivariance of the semilocal ppp-adic logarithm

Galois equivariance of the semilocal $p$ -adic logarithm