Restricted power series over the radius rings A^r are noetherian

The radius ring A^r (TauCeti.WittVector.RadiusRing) is complete, with a multiplicative ultrametric norm, and its degree only depends on the leading part of an element (TauCeti.WittVector.RadiusRing.degree_eq_of_norm_sub_lt, Kedlaya's Remark 2.7) and admits Euclidean division (TauCeti.WittVector.RadiusRing.exists_eq_mul_add, Kedlaya's Proposition 2.9). These are the hypotheses of TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_division, so the rings A^r{T₁/ρ₁, …, Tₙ/ρₙ} of restricted power series are noetherian (Kedlaya, Theorem 3.2). At unit radii these are the completed Huber algebras A^r⟨X₁, …, Xₙ⟩ (TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussEquiv), so A^r is strongly noetherian.

Main results

• TauCeti.WittVector.RadiusRing.isNoetherianRing_isRestricted_subring : the rings A^r{T₁/ρ₁, …, Tₙ/ρₙ} of restricted power series are noetherian.
• TauCeti.WittVector.RadiusRing.isStronglyNoetherian : A^r is strongly noetherian.

References

• K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016, no. 8, 2544–2567; arXiv:1410.5160v3, Remark 2.7, Proposition 2.9 and Theorem 3.2.

instance TauCeti.WittVector.RadiusRing.isNoetherianRing_isRestricted_subring (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} {O : Type u_2} [Field K] [CommRing O] [Algebra O K] {v : Valuation K NNReal} {ϖ : O} [CharP O p] [PerfectRing O p] (hv : v.Integers O) (hϖ : ϖ ≠ 0) (hϖ' : v ((algebraMap O K) ϖ) < 1) {ρ : NNReal} (hρ : ρ ∈ Set.Ioo 0 1) {σ : Type u_3} [Finite σ] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] : IsNoetherianRing ↥(MvPowerSeries.IsRestricted.subring c)

Kedlaya's Hilbert basis theorem for A^r (Kedlaya, Theorem 3.2). For finitely many variables and all positive radii c, the ring A^r{T/c} of restricted power series over the radius ring with its Gauss norm is noetherian.

instance TauCeti.WittVector.RadiusRing.isStronglyNoetherian (p : ℕ) [Fact (Nat.Prime p)] {K : Type u_1} {O : Type u_2} [Field K] [CommRing O] [Algebra O K] {v : Valuation K NNReal} {ϖ : O} [CharP O p] [PerfectRing O p] (hv : v.Integers O) (hϖ : ϖ ≠ 0) (hϖ' : v ((algebraMap O K) ϖ) < 1) {ρ : NNReal} (hρ : ρ ∈ Set.Ioo 0 1) : Huber.IsStronglyNoetherian (RadiusRing p hv hϖ hϖ' hρ)

The radius ring A^r is strongly noetherian: each completed Huber algebra A^r⟨X₁, …, Xₙ⟩ is the Gauss-normed ring A^r{X₁, …, Xₙ} of unit-radius restricted series, which is noetherian by Kedlaya's Theorem 3.2.