Adic completeness of the ring of integers of a complete nonarchimedean field

Let K be a complete nonarchimedean normed field and let O be its ring of integers, in the sense that O is a ring of integers (Valuation.Integers) for the valuation NormedField.valuation given by the norm. Divisibility in O is governed by the norm: ϖ ^ n divides x exactly when ‖x‖ ≤ ‖ϖ‖ ^ n. Consequently, if 0 < ‖ϖ‖ < 1, the ϖ-adic filtration of O is cofinal with the balls about zero; and whenever ‖ϖ‖ < 1 (including ϖ = 0), O is ϖ-adically complete and Hausdorff. Likewise any two pseudouniformisers, nonzero elements of norm less than one, each divide a power of the other, so the ϖ-adic topology does not depend on the choice of pseudouniformiser ϖ.

For a complete perfect nonarchimedean field F of characteristic p with pseudouniformiser ϖ, this is the completeness input for the ring of integers 𝒪_F required to make the Witt vectors A_inf = W(𝒪_F) complete for their (p, [ϖ])-adic topology.

Main results

• Valuation.Integers.mem_span_singleton_pow_iff_norm_le: x ∈ (ϖ) ^ n exactly when ‖x‖ ≤ ‖ϖ‖ ^ n.
• Valuation.Integers.radical_span_singleton_eq_of_norm_lt_one: any two pseudouniformisers, nonzero elements of norm less than one, generate ideals with the same radical.
• Valuation.Integers.isAdicComplete_span_singleton: if ‖ϖ‖ < 1, then O is ϖ-adically complete.

theorem Valuation.Integers.mem_span_singleton_pow_iff_norm_le {K : Type u_1} {O : Type u_2} [NormedField K] [IsUltrametricDist K] [CommRing O] [Algebra O K] (hv : NormedField.valuation.Integers O) {ϖ x : O} {n : ℕ} : x ∈ Ideal.span {ϖ} ^ n ↔ ‖(algebraMap O K) x‖ ≤ ‖(algebraMap O K) ϖ‖ ^ n

In the ring of integers of a nonarchimedean normed field, x lies in (ϖ) ^ n exactly when ‖x‖ ≤ ‖ϖ‖ ^ n.

theorem Valuation.Integers.mem_radical_span_singleton_of_norm_lt_one {K : Type u_1} {O : Type u_2} [NormedField K] [IsUltrametricDist K] [CommRing O] [Algebra O K] (hv : NormedField.valuation.Integers O) {ϖ ϖ' : O} (hϖ : ‖(algebraMap O K) ϖ‖ < 1) (hϖ' : ϖ' ≠ 0) : ϖ ∈ (Ideal.span {ϖ'}).radical

In the ring of integers of a nonarchimedean normed field, an element ϖ of norm less than one lies in the radical of the principal ideal generated by any nonzero ϖ': some power of ϖ has norm at most ‖ϖ'‖, so is divisible by ϖ'.

theorem Valuation.Integers.radical_span_singleton_eq_of_norm_lt_one {K : Type u_1} {O : Type u_2} [NormedField K] [IsUltrametricDist K] [CommRing O] [Algebra O K] (hv : NormedField.valuation.Integers O) {ϖ ϖ' : O} (hϖ0 : ϖ ≠ 0) (hϖ : ‖(algebraMap O K) ϖ‖ < 1) (hϖ'0 : ϖ' ≠ 0) (hϖ' : ‖(algebraMap O K) ϖ'‖ < 1) : (Ideal.span {ϖ}).radical = (Ideal.span {ϖ'}).radical

Pseudouniformisers generate ideals with the same radical. In the ring of integers of a nonarchimedean normed field, two nonzero elements of norm less than one each divide a power of the other.

theorem Valuation.Integers.isAdicComplete_span_singleton {K : Type u_1} {O : Type u_2} [NormedField K] [IsUltrametricDist K] [CommRing O] [Algebra O K] [CompleteSpace K] (hv : NormedField.valuation.Integers O) {ϖ : O} (hϖ : ‖(algebraMap O K) ϖ‖ < 1) : IsAdicComplete (Ideal.span {ϖ}) O

The ring of integers of a complete nonarchimedean field is ϖ-adically complete for every ϖ of norm less than one.