p-adic coordinates on integer-ring ideals

For a finite compatible extension K/ℚ_[p], any nonzero ideal of 𝒪[K] is a free ℤ_[p]-module of rank [K : ℚ_[p]]. Its basis coordinates are homeomorphisms for the subspace topology on the ideal and the product topology on the coordinates. These coordinates identify the additive lattices that occur as logarithms of deep units.

The scalar structure is a named definition: it transports the existing action of 𝒪[ℚ_[p]] through Padic.integerRingEquiv, without adding global module instances.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §§5–6.

@[reducible, inline]

noncomputable abbrev TauCeti.integerIdealPadicIntModule (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] (I : Ideal ↥(ValuativeRel.valuation K).integer) : Module ℤ_[p] ↥I

The ℤ_[p]-module structure on an ideal of 𝒪[K], obtained from its 𝒪[ℚ_[p]]-module structure via the canonical identification of these scalar rings.

@[simp]

theorem TauCeti.coe_padicInt_smul_integerIdeal {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] (I : Ideal ↥(ValuativeRel.valuation K).integer) (c : ℤ_[p]) (x : ↥I) : ↑↑(c • x) = (algebraMap ℚ_[p] K) ↑c * ↑↑x

Scalar multiplication by a p-adic integer on an integer-ring ideal agrees with multiplication by its image in the local field.

theorem TauCeti.continuousSMul_integerIdealPadicInt {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] (I : Ideal ↥(ValuativeRel.valuation K).integer) : ContinuousSMul ℤ_[p] ↥I

P-adic scalar multiplication is continuous on an integer-ring ideal with its subspace topology.

noncomputable def TauCeti.integerIdealEquivPiPadicInt {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {ι : Type u_2} [Fintype ι] (I : Ideal ↥(ValuativeRel.valuation K).integer) (b : Module.Basis ι ↥(ValuativeRel.valuation ℚ_[p]).integer ↥I) : ↥I ≃L[ℤ_[p]] ι → ℤ_[p]

The p-adic basis coordinates of an ideal of the integer ring. A basis over 𝒪[ℚ_[p]] becomes a basis over ℤ_[p] through Padic.integerRingEquiv.

@[simp]

theorem TauCeti.integerIdealEquivPiPadicInt_symm_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {ι : Type u_2} [Fintype ι] (I : Ideal ↥(ValuativeRel.valuation K).integer) (b : Module.Basis ι ↥(ValuativeRel.valuation ℚ_[p]).integer ↥I) (c : ι → ℤ_[p]) : (integerIdealEquivPiPadicInt I b).symm c = ∑ j : ι, c j • b j

The inverse coordinate map is the linear combination of the chosen basis vectors with p-adic integer coefficients.

@[simp]

theorem TauCeti.integerIdealEquivPiPadicInt_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {ι : Type u_2} [Fintype ι] (I : Ideal ↥(ValuativeRel.valuation K).integer) (b : Module.Basis ι ↥(ValuativeRel.valuation ℚ_[p]).integer ↥I) (x : ↥I) : (integerIdealEquivPiPadicInt I b) x = fun (j : ι) => (Padic.integerRingEquiv p) (b.equivFun x j)

The coordinates are the chosen integral basis coordinates, with each scalar identified with a p-adic integer.

theorem TauCeti.nonempty_integerIdealEquivPiPadicInt (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] (I : Ideal ↥(ValuativeRel.valuation K).integer) (hI : I ≠ ⊥) : Nonempty (↥I ≃L[ℤ_[p]] Fin (Module.finrank ℚ_[p] K) → ℤ_[p])

Every nonzero integer-ring ideal in a finite extension of ℚ_[p] has p-adic coordinates with exactly [K : ℚ_[p]] entries, continuously and linearly.