The Nullstellensatz for Tate algebras

Let K be a complete nonarchimedean field and Tₙ = K⟨X₁, …, Xₙ⟩ the Tate algebra of restricted power series in finitely many variables. This file proves that for every maximal ideal m of Tₙ the residue field Tₙ ⧸ m is a finite extension of K, and so is the residue field of every maximal ideal of a quotient of Tₙ. When K is algebraically closed these residue fields are therefore K itself. This is the input that makes a maximal ideal of an affinoid algebra a point of its adic spectrum, by extending the norm of K to the finite extension.

The proof is the Noether normalisation argument of Bosch–Güntzer–Remmert, by induction on the number of variables. A maximal ideal m of K⟨X, Y⟩ contains a nonzero series f, since the variable Y is not a unit. An automorphism of K⟨X, Y⟩ makes f distinguished in Y with a unit dominant coefficient (TauCeti.MvPowerSeries.exists_algEquiv_isDistinguished_isUnit), and Weierstrass division then makes K⟨X⟩⟨Y⟩ ⧸ (f) a finite module over K⟨X⟩ (TauCeti.PowerSeries.IsMulDistinguished.finite_quotient). So the residue field of m is finite over K⟨X⟩, and integral over the quotient of K⟨X⟩ by the contraction of m. That quotient is therefore a field, finite over K by induction.

Main results

• TauCeti.MvPowerSeries.finite_quotient_of_isMaximal: the residue field of a maximal ideal of K⟨X₁, …, Xₙ⟩ is finite over K.
• TauCeti.MvPowerSeries.finite_quotient_of_surjective: the same for every quotient of K⟨X₁, …, Xₙ⟩, which is Wedhorn's Proposition 5.61.
• TauCeti.MvPowerSeries.bijective_algebraMap_quotient_of_surjective: over an algebraically closed K these residue fields are K.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §6.1.2, Corollary 3.
• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 5.61.

theorem TauCeti.MvPowerSeries.finite_quotient_of_isMaximal {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] (m : Ideal ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)) [m.IsMaximal] : Module.Finite K (↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) ⧸ m)

The Nullstellensatz for Tate algebras (Bosch–Güntzer–Remmert, §6.1.2, Corollary 3). Over a complete nonarchimedean field K, the residue field K⟨X₁, …, Xₙ⟩ ⧸ m of every maximal ideal of the Tate algebra in finitely many variables is a finite extension of K.

theorem TauCeti.MvPowerSeries.finite_quotient_of_surjective {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u_2} [CommRing B] [Algebra K B] {σ : Type u_3} [Finite σ] {φ : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) →ₐ[K] B} (hφ : Function.Surjective ⇑φ) (m : Ideal B) [m.IsMaximal] : Module.Finite K (B ⧸ m)

Residue fields of quotients of Tate algebras. If a K-algebra B is a quotient of the Tate algebra K⟨X₁, …, Xₙ⟩ over a complete nonarchimedean field K, then the residue field B ⧸ m of every maximal ideal of B is a finite extension of K.

theorem TauCeti.MvPowerSeries.bijective_algebraMap_quotient_of_surjective {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] {B : Type u_2} [CommRing B] [Algebra K B] {σ : Type u_3} [Finite σ] {φ : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) →ₐ[K] B} (hφ : Function.Surjective ⇑φ) (m : Ideal B) [m.IsMaximal] : Function.Bijective ⇑(algebraMap K (B ⧸ m))

Residue fields over an algebraically closed field. If K is an algebraically closed complete nonarchimedean field and the K-algebra B is a quotient of the Tate algebra K⟨X₁, …, Xₙ⟩, then the residue field of every maximal ideal m of B is K: the structure map K → B ⧸ m is bijective.