Affinoid algebras are the algebras topologically of finite type

Let K be a complete nonarchimedean field with a nontrivial absolute value. There are two notions of an affinoid K-algebra in the library.

• The classical one, TauCeti.IsAffinoidAlgebra K B, is purely algebraic: B is a quotient of a Tate algebra K⟨X₁, …, Xₙ⟩ as a K-algebra, with no norm or topology on B.
• Huber's one is topological: B is a topological K-algebra admitting an open quotient map of K-algebras from the completed Tate algebra, that is TauCeti.Huber.IsTopologicallyFiniteType (algebraMap K B) (Wedhorn, Definition 5.57). Together with its power-bounded subring B°, such an algebra is what Wedhorn's Definition 7.56 calls an affinoid K-algebra.

This file proves that the two notions agree on every complete ultrametric normed K-algebra B (TauCeti.Huber.isTopologicallyFiniteType_algebraMap_iff_isAffinoidAlgebra). One direction holds for any topology on B (TauCeti.Huber.IsTopologicallyFiniteType.exists_surjective_algHom). For the other, every surjection π : K⟨X₁, …, Xₙ⟩ → B of K-algebras is automatically continuous (TauCeti.IsAffinoidAlgebra.continuous_algHom). Read through the identification of the completed Huber Tate algebra with the Gauss-normed one (TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussAlgEquiv), it is then a presentation in Huber's sense by the open mapping theorem (TauCeti.Huber.isStrictlyTopologicallyFiniteType_of_surjective). Thus every algebraic Tate presentation of B induces its norm topology.

So the theory of algebras topologically of finite type applies to the classical affinoid algebras with their Banach topology. In particular they are strongly noetherian Tate rings (TauCeti.IsAffinoidAlgebra.isStronglyNoetherian), and their adic spectra are affinoid adic spaces (TauCeti.ValuationSpectrum.isAdic_presentationLimitPreAdicSpace_of_isAffinoidAlgebra).

Main results

• TauCeti.IsAffinoidAlgebra.isTopologicallyFiniteType: a complete ultrametric normed affinoid K-algebra is topologically of finite type over K.
• TauCeti.Huber.isTopologicallyFiniteType_algebraMap_iff_isAffinoidAlgebra: for a complete ultrametric normed K-algebra, being topologically of finite type over K is equivalent to being affinoid.
• TauCeti.IsAffinoidAlgebra.isStronglyNoetherian: a complete ultrametric normed affinoid K-algebra is strongly noetherian.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 5.57 and Definition 7.56.
• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §6.1.1 and §6.1.3.

theorem TauCeti.IsAffinoidAlgebra.isTopologicallyFiniteType {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u_2} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) : Huber.IsTopologicallyFiniteType (algebraMap K B)

A complete ultrametric normed affinoid algebra is topologically of finite type (Wedhorn, Definition 5.57): its norm topology is the quotient topology of a Tate presentation. Every surjection K⟨X₁, …, Xₙ⟩ → B of K-algebras is a presentation in Huber's sense, by automatic continuity and the open mapping theorem.

theorem TauCeti.IsAffinoidAlgebra.isStronglyNoetherian {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u_2} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) : Huber.IsStronglyNoetherian B

A complete ultrametric normed affinoid algebra is strongly noetherian: being topologically of finite type over the strongly noetherian Tate ring K, every completed Tate algebra over it is noetherian.

theorem TauCeti.Huber.isTopologicallyFiniteType_algebraMap_iff_isAffinoidAlgebra {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u_2} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] : IsTopologicallyFiniteType (algebraMap K B) ↔ IsAffinoidAlgebra K B

Affinoid algebras are the algebras topologically of finite type. A complete ultrametric normed K-algebra B is topologically of finite type over K in Huber's sense (Wedhorn, Definition 5.57) exactly when it is a quotient of a Tate algebra K⟨X₁, …, Xₙ⟩ as a K-algebra.