Independent local $p$ -adic logarithms of Galois conjugates in the non-involution case

Open

Leopoldt.exists_independent_log_conj_of_galois_not_exponent_two

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

number-theoryp-adicunits

Let $L/\mathbb Q$ be a totally real Galois number field of degree at least three whose Galois group contains an element of order greater than two, and let $p$ be an odd prime. There is a global unit $\varepsilon$ whose Galois conjugates generate a finite-index subgroup of the unit group and all lie in the small logarithm ball at every place above $p$ . Among their semilocal $p$ -adic logarithms, one can select $r=\operatorname{rank} \mathcal O_L^\times$ vectors that are linearly independent over $\mathbb Z_p$ .

The finite-index condition is the Minkowski-unit condition. The asserted independence is the unresolved analytic step: by Leopoldt.leopoldtConjecture_iff_exists_linearIndependent_log_conj, it yields Leopoldt's conjecture for these Galois fields. The small-ball clause makes that established criterion applicable without a hidden local hypothesis.

Preamble

import Definitions.Def_PadicLog

open NumberField

Formal statement

namespace Leopoldt
theorem exists_independent_log_conj_of_galois_not_exponent_two (p : ℕ) [Fact p.Prime] (hp : Odd p)
    (L : Type*) [Field L] [NumberField L] [IsTotallyReal L] [IsGalois ℚ L]
    (hL : 3 ≤ Module.finrank ℚ L) (hG : ∃ σ : L ≃ₐ[ℚ] L, σ * σ ≠ 1) :
    ∃ ε : (𝓞 L)ˣ,
      (Subgroup.closure (Set.range fun σ : L ≃ₐ[ℚ] L =>
        _root_.Units.map (RingOfIntegers.mapRingEquiv σ.toRingEquiv).toMonoidHom ε)).FiniteIndex ∧
      (∀ (σ : L ≃ₐ[ℚ] L) (v : PrimesOver p L),
        ‖((diagonalUnits p L
          (_root_.Units.map (RingOfIntegers.mapRingEquiv σ.toRingEquiv).toMonoidHom ε) v :
            v.1.adicCompletionIntegers L) : v.1.adicCompletion L) - 1‖ ≤
          ‖((p : ℕ) : v.1.adicCompletion L)‖ ^ 2) ∧
      ∃ s : Fin (NumberField.Units.rank L) → (L ≃ₐ[ℚ] L),
        LinearIndependent ℤ_[p] fun (i : Fin (NumberField.Units.rank L))
          (v : PrimesOver p L) =>
          PadicLog.log (p := p)
            ((diagonalUnits p L
              (_root_.Units.map (RingOfIntegers.mapRingEquiv (s i).toRingEquiv).toMonoidHom ε) v :
                v.1.adicCompletionIntegers L) : v.1.adicCompletion L) := by sorry
end Leopoldt

Source

Formulation of the unresolved logarithmic independence step in the Galois totally real case; compare Preda Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544, Section 1.1, and Leopoldt.leopoldtConjecture_iff_exists_linearIndependent_log_conj.

View graph

Independent local ppp-adic logarithms of Galois conjugates in the non-involution case

Independent local $p$ -adic logarithms of Galois conjugates in the non-involution case