Galois conjugation preserves vanishing of all semilocal unit logarithms

Proved

Leopoldt.log_diagonalUnits_zero_of_galois

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

leopoldtnumber-theory

Let $K$ be a number field, $p$ a prime, and $\varepsilon$ a global unit sufficiently close to $1$ at every place above $p$ for the local logarithm. If every component of the semilocal logarithm of $\varepsilon$ vanishes, then the same is true of each Galois conjugate $\sigma(\varepsilon)$ . The conjugation also permutes the places above $p$ , so vanishing at all places is essential.

Preamble

import Theorems.Thm_Leopoldt_log_diagonalUnits_conj

open NumberField

Formal statement

namespace Leopoldt
theorem log_diagonalUnits_zero_of_galois (p : ℕ) [Fact p.Prime] (K : Type*) [Field K]
    [NumberField K] (σ : K ≃ₐ[ℚ] K) (ε : (𝓞 K)ˣ)
    (hsmall : ∀ v : PrimesOver p K,
      ‖((diagonalUnits p K ε v : v.1.adicCompletionIntegers K) :
          v.1.adicCompletion K) - 1‖ < 1)
    (hzero : ∀ v : PrimesOver p K,
      PadicLog.log (p := p)
        ((diagonalUnits p K ε v : v.1.adicCompletionIntegers K) :
          v.1.adicCompletion K) = 0) (w : PrimesOver p K) :
    PadicLog.log (p := p)
      ((diagonalUnits p K
          (_root_.Units.map (RingOfIntegers.mapRingHom (σ : K →+* K)).toMonoidHom ε) w :
          w.1.adicCompletionIntegers K) : w.1.adicCompletion K) = 0 := by sorry
end Leopoldt

Source

Direct corollary of the already proved theorem Leopoldt.log_diagonalUnits_conj (Galois covariance of the p-adic logarithm), Prove2Me theorem cbcb4eb2-8be3-41aa-925c-8b472dbcf0f4.

View graph