Noetherianity of the completed Tate algebras

Over a complete nonarchimedean field, the completed Huber algebra in n variables is identified with the Gauss-normed ring of unit-radius restricted series by TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussEquiv. The latter is noetherian by Weierstrass division and induction on the number of variables, and this transfers to the completed Huber algebra. In one variable it is moreover a principal ideal ring, transported from Mathlib's univariate restricted-series ring along TauCeti.Huber.restrictedMvPowerSeriesCompletionOneEquiv.

Main results

• TauCeti.Huber.isPrincipalIdealRing_restrictedMvPowerSeriesCompletion_one: every ideal of the completed one-variable Tate algebra over a complete nonarchimedean field is principal.
• TauCeti.Huber.isNoetherianRing_restrictedMvPowerSeriesCompletion: the completed Tate algebra in n variables over a complete nonarchimedean field is noetherian.
• TauCeti.Huber.IsStronglyNoetherian.of_normedField: a complete nonarchimedean normed field is strongly noetherian.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.6, for noetherianity of Tate algebras.
• T. Wedhorn, Adic Spaces, §5.6, for restricted power series and their topology.

theorem TauCeti.Huber.isPrincipalIdealRing_restrictedMvPowerSeriesCompletion_one {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] : IsPrincipalIdealRing (restrictedMvPowerSeriesCompletion 1 K)

The completed one-variable Tate algebra over a complete nonarchimedean field is a principal ideal ring. This is transported from the restricted univariate series ring, where Weierstrass division shows that every ideal has a generator.

theorem TauCeti.Huber.isNoetherianRing_restrictedMvPowerSeriesCompletion {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (n : ℕ) : IsNoetherianRing (restrictedMvPowerSeriesCompletion n K)

The completed Tate algebra over a complete nonarchimedean field is noetherian. This is transported from the Gauss-normed ring of unit-radius restricted series in n variables.

instance TauCeti.Huber.IsStronglyNoetherian.of_normedField {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] : IsStronglyNoetherian K

Complete nonarchimedean fields are strongly noetherian (Bosch–Güntzer–Remmert §5.2.6): every completed Tate algebra K⟨X₁, …, Xₙ⟩ is noetherian.