The p-adic integers are a Huber ring, and not a Tate ring

ℤ_[p] with its norm topology is a Huber ring, with (ℤ_[p], (p)) as a pair of definition, and it is not a Tate ring. It is the roadmap's Layer-0 example after the discrete case, and the first to separate TauCeti.Huber.IsHuberRing from TauCeti.Huber.IsTateRing: the topology is adic for the proper ideal (p), so no unit is topologically nilpotent.

Main results

• TauCeti.Huber.PadicInt.coe_maximalIdeal_pow: (p)ⁿ is the closed ball of radius p⁻ⁿ. Openness is Mathlib's IsLocalRing.isOpen_maximalIdeal_pow.
• TauCeti.Huber.PadicInt.isAdic_maximalIdeal: the norm topology of ℤ_[p] is the (p)-adic topology. Mathlib has IsAdicComplete (maximalIdeal ℤ_[p]) ℤ_[p] but not this comparison of topologies, which is what a pair of definition requires.
• TauCeti.Huber.PadicInt.instIsLinearTopology: consequently ℤ_[p] is linearly topologized, and TauCeti.Huber.PadicInt.isTopologicallyNilpotent_iff_dvd: its topologically nilpotent elements are the multiples of p.
• TauCeti.Huber.PadicInt.isHuberRing and TauCeti.Huber.PadicInt.not_isTateRing: the two halves of the example.

Implementation notes

The pair of definition (ℤ_[p], (p)) is the general adic pair TauCeti.Huber.PairOfDefinition.adic of TauCeti/RingTheory/Huber/Adic.lean, applied to the maximal ideal.

Scope

Only ℤ_[p] is treated here. The roadmap's remaining Layer-0 examples — ℚ_[p] and F⸨t⸩ are Tate, and ℚ_p⟨T₁,…,Tₙ⟩ is complete and strongly noetherian — are not proved in this file.

References

• Wedhorn, Adic Spaces, §6, where Huber and Tate rings are introduced (Proposition and Definition 6.1) and ℤ_[p] is the standard example of a Huber ring that is not Tate.

theorem TauCeti.Huber.PadicInt.coe_maximalIdeal_pow {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : ↑(IsLocalRing.maximalIdeal ℤ_[p] ^ n) = {x : ℤ_[p] | ‖x‖ ≤ ↑p ^ (-↑n)}

The n-th power of the maximal ideal of ℤ_[p] is the closed ball of radius p⁻ⁿ: this is what ties the norm topology to the (p)-adic one.

theorem TauCeti.Huber.PadicInt.isAdic_maximalIdeal {p : ℕ} [Fact (Nat.Prime p)] : IsAdic (IsLocalRing.maximalIdeal ℤ_[p])

The norm topology of ℤ_[p] is the (p)-adic topology.

instance TauCeti.Huber.PadicInt.instIsLinearTopology {p : ℕ} [Fact (Nat.Prime p)] : IsLinearTopology ℤ_[p] ℤ_[p]

The norm topology of ℤ_[p] is linear: the ideals (p ^ n) are a neighbourhood basis of zero.

theorem TauCeti.Huber.PadicInt.isTopologicallyNilpotent_iff_dvd {p : ℕ} [Fact (Nat.Prime p)] {c : ℤ_[p]} : IsTopologicallyNilpotent c ↔ ↑p ∣ c

A p-adic integer is topologically nilpotent exactly when it is divisible by p.

instance TauCeti.Huber.PadicInt.isHuberRing {p : ℕ} [Fact (Nat.Prime p)] : IsHuberRing ℤ_[p]

ℤ_[p] is a Huber ring, with (ℤ_[p], (p)) as a pair of definition: the norm topology is the adic topology of the principal ideal (p).

theorem TauCeti.Huber.PadicInt.not_isTateRing {p : ℕ} [Fact (Nat.Prime p)] : ¬IsTateRing ℤ_[p]

ℤ_[p] is not a Tate ring: it admits no pseudouniformiser. Together with TauCeti.Huber.PadicInt.isHuberRing this separates IsHuberRing from IsTateRing.