The valuation topology of a discretely valued field is adic

Let K be a field whose topology is induced by its valuative relation, and whose ring of integers 𝒪[K] is a discrete valuation ring; a nonarchimedean local field is the motivating example. This file proves that the subspace topology of 𝒪[K] is its 𝓂[K]-adic topology, and reads the consequence back in K: the powers 𝓂[K] ^ n form a neighbourhood basis of 0 in K consisting of open additive subgroups, which are moreover compact when 𝒪[K] is.

So near 0 the topology of K is described by the ideals of 𝒪[K] alone, with no reference to the value group. For a local field this is the additive counterpart of the statement that the unit filtration U(K,n) is a neighbourhood basis of 1 in Kˣ (TauCeti.hasBasis_nhds_one_unitFiltration).

Main results

• Irreducible.exists_valuation_pow_lt: the valuations of the powers of a uniformizer eventually drop below any nonzero value.
• TauCeti.isAdic_maximalIdeal: the topology of 𝒪[K] is the 𝓂[K]-adic topology.
• TauCeti.hasBasis_nhds_zero_maximalIdeal_pow: the images in K of the powers 𝓂[K] ^ n form a neighbourhood basis of 0 in K.
• TauCeti.isOpen_image_maximalIdeal_pow and TauCeti.isCompact_image_maximalIdeal_pow: each of these images is open in K, and compact when 𝒪[K] is.

For a nonarchimedean local field the remaining point-set facts are Mathlib's: 𝒪[K] is open (Valuation.isOpen_integer) and compact (CompactSpace 𝒪[K]), it is 𝓂[K]-adically complete (IsAdicComplete 𝓂[K] 𝒪[K]), and Kˣ is locally compact.

The proof outline for isAdic_maximalIdeal follows IsDedekindDomain.HeightOneSpectrum.isAdic_maximalIdeal_adicCompletionIntegers, adapted from the Valued setting of an adic completion to the ValuativeRel setting of K.

References

• J.-P. Serre, Corps Locaux, Chapter II, §1.
• J. Neukirch, Algebraic Number Theory, Chapter II, §§4–5.

theorem Irreducible.exists_valuation_pow_lt {K : Type u_1} [Field K] [ValuativeRel K] [IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (γ : (ValuativeRel.ValueGroupWithZero K)ˣ) : ∃ (n : ℕ), (ValuativeRel.valuation K) ↑π ^ n < ↑γ

The valuations of the powers of a uniformizer π of K eventually drop below any nonzero value of the valuation.

theorem TauCeti.isAdic_maximalIdeal (K : Type u_1) [Field K] [ValuativeRel K] [IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer] [TopologicalSpace K] [IsValuativeTopology K] : IsAdic (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)

The topology of 𝒪[K] is the 𝓂[K]-adic topology: the powers 𝓂[K] ^ n are open, and every neighbourhood of 0 in 𝒪[K] contains one of them.

theorem TauCeti.hasBasis_nhds_zero_maximalIdeal_pow (K : Type u_1) [Field K] [ValuativeRel K] [IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer] [TopologicalSpace K] [IsValuativeTopology K] : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ n)

The powers of the maximal ideal form a neighbourhood basis of 0 in K: a subset of K is a neighbourhood of 0 exactly when it contains 𝓂[K] ^ n for some n.

theorem TauCeti.isOpen_image_maximalIdeal_pow (K : Type u_1) [Field K] [ValuativeRel K] [IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer] [TopologicalSpace K] [IsValuativeTopology K] (n : ℕ) : IsOpen (Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ n))

Each power 𝓂[K] ^ n of the maximal ideal is open in K.

theorem TauCeti.isCompact_image_maximalIdeal_pow (K : Type u_1) [Field K] [ValuativeRel K] [IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer] [TopologicalSpace K] [IsValuativeTopology K] [CompactSpace ↥(ValuativeRel.valuation K).integer] (n : ℕ) : IsCompact (Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ n))

If 𝒪[K] is compact, as for a nonarchimedean local field, then each power 𝓂[K] ^ n of the maximal ideal is compact in K.