An injective map into n copies of Q_p bounds the Z_p-rank by n

Proved

Leopoldt.rank_le_of_injective_linearMap_to_padicProduct

by mysticflounder · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebralocal-fieldsp-adic

Let p be a prime and let F_v be the completion of a number field at a prime above p. Any injective linear map over the p-adic integers from F_v into a product of n copies of Q_p forces the Z_p-module rank of F_v to be at most n. This is the rank-monotonicity step that turns finite local coordinates into the local degree bound.

Preamble

import Definitions.Def_PadicLog

open NumberField IsDedekindDomain

Formal statement

namespace Leopoldt
theorem rank_le_of_injective_linearMap_to_padicProduct (p : ℕ) [Fact p.Prime]
    (F : Type*) [Field F] [NumberField F] (v : PrimesOver p F) {n : ℕ}
    (g : v.1.adicCompletion F →ₗ[ℤ_[p]] (Fin n → ℚ_[p]))
    (hg : Function.Injective g) :
    Module.rank ℤ_[p] (v.1.adicCompletion F) ≤ (n : Cardinal) := by sorry
end Leopoldt

Source

Mathlib linear algebra dimension theory, in particular Module.Basis.mk_eq_rank and rank monotonicity under injective linear maps, together with the standard rank-one computation for Q_p over Z_p; see Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean and Mathlib/NumberTheory/Padics/PadicNumbers.lean.

View graph