Monsky–Washnitzer algebras are noetherian

Over a complete ultrametric normed field K, the Monsky–Washnitzer algebra K⟨X⟩† in finitely many variables is a noetherian ring.

The proof is the classical induction on the number of variables via Weierstrass theory. Write W = K⟨X⟩† and W' = K⟨X, Y⟩†, with Y = X none, and regard W' as a W-algebra through washnitzerAlgebra.optionC. A nonzero ideal I of W' contains a nonzero series f, and a triangular automorphism of W' makes f distinguished in Y of some degree s, with a unit coefficient in degree s. Overconvergent Weierstrass division by f shows that W' ⧸ (f) is spanned over W by 1, Y, …, Y ^ (s - 1), so it is a finite W-module. If W is noetherian, W' ⧸ (f) is then a noetherian module, hence I is finitely generated.

The Weierstrass-division finiteness step is also exposed for any finite map annihilating a distinguished series with a unit coefficient in the distinguished degree. A Weierstrass polynomial ω ∈ K⟨X⟩†[Y], monic with coefficients of Gauss norm at most 1, is such a series, so a finite map whose kernel contains ω is finite over K⟨X⟩†. Dagger algebras, the quotients of Monsky–Washnitzer algebras, are noetherian.

Main results

• TauCeti.Dagger.washnitzerAlgebra.finite_comp_optionC_of_isDistinguished: a finite map annihilating such a distinguished series is finite over the algebra in one fewer variable.
• TauCeti.Dagger.washnitzerAlgebra.finite_comp_optionC_of_isMonicOfDegree: the same for a finite map annihilating a Weierstrass polynomial.
• TauCeti.Dagger.washnitzerAlgebra.isNoetherianRing: K⟨X⟩† is noetherian for finitely many variables.
• TauCeti.Dagger.IsDaggerAlgebra.isNoetherianRing: dagger algebras are noetherian.

References

• E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.3 (iii) and §1.4 (1).
• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.6, Theorem 1 (the same argument for Tate algebras).

theorem TauCeti.Dagger.washnitzerAlgebra.finite_comp_optionC_of_isDistinguished {σ : Type u_1} {K : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_3} [CommRing A] [Algebra K A] {g : ↥(washnitzerAlgebra (Option σ) K)} {s : ℕ} (hg : PowerSeries.IsDistinguished 1 s ↑(MvPowerSeries.restrictedOptionEquiv ((toTate (Option σ) K) g))) (hu : IsUnit ((PowerSeries.coeff s) ↑(MvPowerSeries.restrictedOptionEquiv ((toTate (Option σ) K) g)))) {π : ↥(washnitzerAlgebra (Option σ) K) →ₐ[K] A} (hπ : π.Finite) (hzero : π g = 0) : (π.comp optionC).Finite

A finite map annihilating a distinguished series is already finite over the algebra in one fewer variable. The distinguished coefficient must be a unit; no reducedness or surjectivity of the map is required.

theorem TauCeti.Dagger.washnitzerAlgebra.finite_comp_optionC_of_isMonicOfDegree {σ : Type u_1} {K : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_3} [CommRing A] [Algebra K A] {ω : Polynomial ↥(washnitzerAlgebra σ K)} {s : ℕ} (hm : ω.IsMonicOfDegree s) (hle : ∀ k < s, ‖ω.coeff k‖ ≤ 1) {π : ↥(washnitzerAlgebra (Option σ) K) →ₐ[K] A} (hπ : π.Finite) (hzero : π (polynomialToOption ω) = 0) : (π.comp optionC).Finite

A finite map annihilating a Weierstrass polynomial ω ∈ K⟨X⟩†[Y], evaluated at Y, is already finite over K⟨X⟩†. Here ω is monic of degree s and its lower coefficients have Gauss norm at most 1; such an ω is distinguished of degree s in Y at unit radius, with leading coefficient 1.

instance TauCeti.Dagger.washnitzerAlgebra.isNoetherianRing {σ : Type u_1} {K : Type u_2} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [Finite σ] : IsNoetherianRing ↥(washnitzerAlgebra σ K)

Monsky–Washnitzer algebras are noetherian. Over a complete ultrametric normed field K, the algebra K⟨X⟩† of overconvergent power series in finitely many variables is a noetherian ring. No characteristic or nontrivial-norm assumption is needed.

theorem TauCeti.Dagger.IsDaggerAlgebra.isNoetherianRing {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] : IsNoetherianRing A

Dagger algebras are noetherian. Over a complete ultrametric normed field K, every K-dagger algebra is a quotient of a noetherian Monsky–Washnitzer algebra.