A local completion embeds linearly into an ef-fold product of Q_p

Proved

Leopoldt.exists_adicCompletion_linearEmbedding_to_padicProduct

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

local-fieldsnumber-theoryp-adic

Let p be a prime, F a number field, and v a prime of F above p. If e and f are the ramification index and inertia degree of v over p, then the completed field F_v admits an injective linear map over the p-adic integers into a product of e f copies of the p-adic field Q_p. This is the local coordinate statement underlying the degree formula: choose a Q_p-basis of the completion and record its coordinates.

Preamble

import Definitions.Def_PadicLog

open NumberField IsDedekindDomain

Formal statement

namespace Leopoldt
theorem exists_adicCompletion_linearEmbedding_to_padicProduct (p : ℕ) [Fact p.Prime]
    (F : Type*) [Field F] [NumberField F] (v : PrimesOver p F) :
    ∃ g : v.1.adicCompletion F →ₗ[ℤ_[p]]
        (Fin (v.1.asIdeal.ramificationIdx ℤ * v.1.asIdeal.inertiaDeg ℤ) → ℚ_[p]),
      Function.Injective g := by sorry
end Leopoldt

Source

J.-P. Serre, Local Fields, Springer GTM 67 (1979), Chapter II, Section 3, Proposition 10; J. Neukirch, Algebraic Number Theory, Springer Grundlehren 322 (1999), Chapter II, Section 6, Proposition 6.8. These identify the completion at v as an ef-dimensional Q_p-vector space.

View graph