Henselianity of nonarchimedean local fields

The integer ring of a nonarchimedean local field is complete for the topology of its maximal ideal, and is therefore a Henselian local ring. It is also complete for the adic topology of every positive power 𝓂[K] ^ (n + 1) of the maximal ideal, which defines the same topology, and is therefore Henselian at each of them: a simple approximate root modulo 𝓂[K] ^ (n + 1) lifts to a root congruent to it modulo 𝓂[K] ^ (n + 1).

Main results

• TauCeti.henselianLocalRing_integer: the integer ring of a nonarchimedean local field is a Henselian local ring.
• TauCeti.isAdicComplete_maximalIdeal_pow_succ: the integer ring is complete for the adic topology of each positive power of its maximal ideal, hence Henselian at it through Mathlib's IsAdicComplete.henselianRing.

instance TauCeti.henselianLocalRing_integer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : HenselianLocalRing ↥(ValuativeRel.valuation K).integer

The integer ring of a nonarchimedean local field is a Henselian local ring: it is local and complete for the topology of its maximal ideal.

instance TauCeti.isAdicComplete_maximalIdeal_pow_succ (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : IsAdicComplete (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ (n + 1)) ↥(ValuativeRel.valuation K).integer

The integer ring of a nonarchimedean local field is complete for the adic topology of every positive power of its maximal ideal. Mathlib records the completeness at 𝓂[K] itself for the uniformity attached to the topological additive group K; the powers follow because the 𝓂[K] ^ (n + 1)-adic filtration is cofinal in the 𝓂[K]-adic one.