Full-rank finite family in the local product contains an independent subfamily

Proved

Leopoldt.exists_linearlyIndependent_subfamily_localProduct

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

linear-algebranumber-theoryp-adic

Let $p$ be prime, $K$ a number field, and $M=\prod_{v\mid p}K_v$ , regarded as a $\mathbb Z_p$ -module. Suppose a finite family $(w_i)_{i\in I}$ spans a submodule of rank $r$ . Then one can choose $r$ indices $s(1),\dots,s(r)$ such that

w_{s(1)},\dots,w_{s(r)}

are linearly independent over $\mathbb Z_p$ .

The torsion-free local product allows clearing the denominators in a maximal independent family without losing rank. This selection result converts a full-rank span of semilocal logarithms into a choice of independent conjugates in the logarithmic criterion for Leopoldt's conjecture.

Preamble

import Definitions.Def_PadicLog

open NumberField

Formal statement

namespace Leopoldt
theorem exists_linearlyIndependent_subfamily_localProduct
    (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K]
    {ι : Type*} [Finite ι]
    (w : ι → ∀ v : PrimesOver p K, v.1.adicCompletion K) {r : ℕ}
    (hr : Module.finrank ℤ_[p] (Submodule.span ℤ_[p] (Set.range w)) = r) :
    ∃ s : Fin r → ι, LinearIndependent ℤ_[p] (w ∘ s) := by sorry
end Leopoldt

Source

Extraction of the independent-subfamily argument from the verified proof of Leopoldt.leopoldtConjecture_iff_exists_linearIndependent_log_conj (submission 48251889-2ea0-4f5b-804c-e937ba97f5d3); maximal independent family and torsion-free rank comparison.

View graph