Residue fields of algebras topologically of finite type over a field

Let k be a complete nonarchimedean field and B a topological k-algebra topologically of finite type, that is IsTopologicallyFiniteType (algebraMap k B). This file proves Wedhorn's Proposition 5.61: for every maximal ideal m of B the residue field B ⧸ m is a finite extension of k.

A presentation of B is a surjection from the completed Tate algebra k⟨X₁, …, Xₙ⟩, which is the Gauss-normed algebra of restricted power series (TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussAlgEquiv). So the statement is the Nullstellensatz for quotients of Tate algebras, TauCeti.MvPowerSeries.finite_quotient_of_surjective.

Over a finite extension of k the norm of k extends uniquely, so this is what attaches to a maximal ideal of B a point of the adic spectrum Spa(B, B°) (Wedhorn, Example 7.58).

Main results

• TauCeti.Huber.IsTopologicallyFiniteType.exists_surjective_algHom: a k-algebra topologically of finite type is a quotient of a Tate algebra k⟨X₁, …, Xₙ⟩.
• TauCeti.Huber.IsTopologicallyFiniteType.finite_quotient_of_isMaximal: the residue field of a maximal ideal of a k-algebra topologically of finite type is finite over k.

References

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

theorem TauCeti.Huber.IsTopologicallyFiniteType.exists_surjective_algHom {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u_2} [CommRing B] [TopologicalSpace B] [Algebra K B] (h : IsTopologicallyFiniteType (algebraMap K B)) : ∃ (n : ℕ) (φ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1) →ₐ[K] B), Function.Surjective ⇑φ

A K-algebra topologically of finite type is a quotient of a Tate algebra: there is a surjective K-algebra map onto it from the Gauss-normed algebra K⟨X₁, …, Xₙ⟩ of restricted power series, for some n.

theorem TauCeti.Huber.IsTopologicallyFiniteType.finite_quotient_of_isMaximal {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u_2} [CommRing B] [TopologicalSpace B] [Algebra K B] (h : IsTopologicallyFiniteType (algebraMap K B)) (m : Ideal B) [m.IsMaximal] : Module.Finite K (B ⧸ m)

Wedhorn, Proposition 5.61. Over a complete nonarchimedean field K, the residue field B ⧸ m of every maximal ideal of a K-algebra B topologically of finite type is a finite extension of K.