Prove2Me

The pp-adic logarithm of a Galois conjugate of a global unit

Proved
Leopoldt.log_diagonalUnits_conj

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

galoisleopoldtnumber-theoryp-adic

Let KK be a number field, pp a prime, σ∈Aut⁡(K/Q)\sigma\in\operatorname{Aut}(K/\mathbb{Q}) and ε∈OK×\varepsilon\in\mathcal{O}_K^\times. For a prime w∣pw\mid p let σw:Kσ−1w→∼Kw\sigma_w:K_{\sigma^{-1}w}\xrightarrow{\sim}K_w be the isomorphism of completions induced by σ\sigma, and assume ε\varepsilon is a principal unit at σ−1w\sigma^{-1}w, i.e. ∥ισ−1w(ε)−1∥<1\|\iota_{\sigma^{-1}w}(\varepsilon)-1\|<1. Then

log⁡pιw(σε)=σw(log⁡pισ−1w(ε)).\log_p\iota_w(\sigma\varepsilon)=\sigma_w\bigl(\log_p\iota_{\sigma^{-1}w}(\varepsilon)\bigr).

Thus the semilocal logarithm vector of a Galois conjugate is obtained from that of ε\varepsilon by the Galois action on ∏v∣pKv\prod_{v\mid p}K_v: Λ(σε)=σ⋅Λ(ε)\Lambda(\sigma\varepsilon)=\sigma\cdot\Lambda(\varepsilon), and the Zp\mathbb{Z}_p-span of the logarithms of the (principal) units is a Zp[G]\mathbb{Z}_p[G]-module. Here σε\sigma\varepsilon is the image of ε\varepsilon under the ring automorphism of OK\mathcal{O}_K induced by σ\sigma.

Preamble
import Definitions.Def_LeopoldtGaloisAction
import Definitions.Def_PadicLog

open NumberField
Formal statement
theorem Leopoldt.log_diagonalUnits_conj (p : ℕ) [Fact p.Prime] (K : Type*) [Field K]
    [NumberField K] (σ : K ≃ₐ[ℚ] K) (ε : (𝓞 K)ˣ) (w : Leopoldt.PrimesOver p K)
    (hε : ‖((Leopoldt.diagonalUnits p K ε ((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.diagonalUnits p K
            (_root_.Units.map (RingOfIntegers.mapRingHom (σ : K →+* K)).toMonoidHom ε) w :
          w.1.adicCompletionIntegers K) : w.1.adicCompletion K) =
      Leopoldt.GaloisAction.localRingEquiv σ (Leopoldt.valuation_primesOverPerm_symm p K σ w)
        (PadicLog.log (p := p)
          ((Leopoldt.diagonalUnits p K ε ((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 (Galois action on log_p of units in the proof of Brumer's theorem); J. Ax, On the units of an algebraic number field, Illinois J. Math. 9 (1965), 584–589.

View graph