Tate algebras in finitely many variables are noetherian

Over a complete nonarchimedean field K, the Tate algebra K⟨X₁, …, Xₙ⟩ of unit-radius restricted power series in finitely many variables is a noetherian ring.

The proof is the induction on the number of variables of Bosch–Güntzer–Remmert. A Tate algebra in no variables is K. For the inductive step, let I be a nonzero ideal of the Tate algebra in the variables Option σ, and f ∈ I nonzero. After an automorphism of the Tate algebra, f is a restricted series in the variable none over the Tate algebra T in the variables σ which is distinguished with a unit dominant coefficient (TauCeti.MvPowerSeries.exists_algEquiv_isDistinguished_isUnit). Weierstrass division then makes the quotient by f a finite T-module (TauCeti.PowerSeries.IsDistinguished.finite_quotient), so it is a noetherian ring when T is, and the image of I in it is finitely generated. Together with the generator f of the kernel, this shows that I is finitely generated.

Main results

• TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring: the Tate algebra in finitely many variables over a complete nonarchimedean field is noetherian.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.6, Theorem 1.

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

Tate algebras are noetherian. Over a complete nonarchimedean field K, the Tate algebra K⟨X₁, …, Xₙ⟩ of unit-radius restricted power series in finitely many variables is a noetherian ring.