Tate algebras are Jacobson rings

Over a complete nonarchimedean field K, the Tate algebra K⟨X₁, …, Xₙ⟩ is a Jacobson ring: every prime ideal is an intersection of maximal ideals. Together with the Nullstellensatz TauCeti.MvPowerSeries.finite_quotient_of_isMaximal, this lets the maximal ideals, the classical points of the affinoid space, detect every radical ideal of the Tate algebra and of its quotients.

The proof is by induction on the number of variables, writing K⟨X, Y⟩ as the univariate Tate algebra K⟨X⟩⟨Y⟩ and applying TauCeti.isJacobsonRing_of_quotient_span_singleton.

• The Jacobson radical of K⟨X⟩⟨Y⟩ vanishes. If f lies in it, then so does every multiple f * a Y, for a ∈ K, so 1 + f * a Y is a unit and hence distinguished of degree 0 (TauCeti.PowerSeries.isDistinguished_zero_of_isUnit): all its positive-degree coefficients have norm smaller than 1. Choosing a as the inverse of a nonzero coefficient of f produces a coefficient of norm at least 1, unless f = 0.
• For a nonzero f, an automorphism makes f distinguished in Y with a unit dominant coefficient, and Weierstrass division makes K⟨X⟩⟨Y⟩ ⧸ (f) finite over K⟨X⟩, which is Jacobson by induction. Integral extensions of Jacobson rings are Jacobson.

The coefficient field need not be nontrivially normed: the rescaling uses only the inverse of a coefficient of f.

Main results

• TauCeti.MvPowerSeries.isJacobsonRing: the Tate algebra in finitely many variables over a complete nonarchimedean field is a Jacobson ring.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §§5.2.5–5.2.6.

instance TauCeti.MvPowerSeries.isJacobsonRing {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] : IsJacobsonRing ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)

Tate algebras are Jacobson rings. Over a complete nonarchimedean field K, every prime ideal of the Tate algebra K⟨X₁, …, Xₙ⟩ in finitely many variables is the intersection of the maximal ideals containing it.