The interval rings B^I are strongly noetherian #
Let O be the ring of integers of a valuation v : Valuation K ℝ≥0 on a field K, perfect of
characteristic p, and let ϖ ∈ O be a pseudouniformiser. For radii 0 < ρ₁ ≤ ρ₂ < 1, the
radius ring A = A^{ρ₂} (TauCeti.WittVector.RadiusRing) maps isometrically to the interval ring
B = B^{[ρ₁, ρ₂]} (TauCeti.WittVector.IntervalRing).
For every finite family of positive real radii c, the ring B{T/c} of restricted power series
is a quotient of A{T/c, U/ρ₁⁻¹} by evaluation at U = p⁻¹
(TauCeti.WittVector.RadiusRing.restrictedEvalIntervalRing_surjective), and the latter is
noetherian by Kedlaya's Theorem 3.2
(TauCeti.WittVector.RadiusRing.isNoetherianRing_isRestricted_subring). So every B{T/c} is
noetherian, which is Kedlaya's Theorem 4.10. At unit radii these rings are the completed Huber
algebras B⟨X₁, …, Xₙ⟩ (TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussEquiv), so B is
strongly noetherian in Huber's sense (Kedlaya, Remark 4.11), for every closed interval
[ρ₁, ρ₂].
The file also presents B as an open quotient of a Huber algebra over A in one variable at unit
radius, when ρ₁ ^ a = v(ϖ) ^ b with a ≠ 0. Then the element [ϖ] ^ b / p ^ a of B has norm
one at the radius ρ₁, and the continuous map
ψ : A⟨X⟩ → B, X ↦ [ϖ] ^ b / p ^ a,
out of the one-variable restricted series ring over A is an open quotient map. This is the
surjective half of the third isomorphism of Kedlaya's Lemma 4.9,
A^r_{L,E}{T}/(pT - [z ^ n]) ≅ B^{I'''}_{L,E}, with p ^ a in place of p.
The key estimate takes place in 𝕎 O[1/(p [ϖ])], which is dense in B: writing an element as
y / (p [ϖ]) ^ m and expanding y = ∑ᵢ [yᵢ] pⁱ into Teichmüller terms, it is a finite sum of
monomials e ([ϖ] ^ b / p ^ a) ^ j whose coefficients e ∈ 𝕎 O[1/[ϖ]] have norm at most
ρ₁⁻ᵃ times its own norm. So the closure of the image under ψ of every neighbourhood of zero is
a neighbourhood of zero, and completeness of A⟨X⟩ removes the closure
(TauCeti.isOpenMap_of_closure_image_mem_nhds).
Main results #
TauCeti.WittVector.isNoetherianRing_isRestricted_subring_intervalRing: the ringsB^{[ρ₁, ρ₂]}{T/c}in finitely many variables are noetherian for all positive radii.TauCeti.WittVector.isStronglyNoetherian_intervalRing:B^{[ρ₁, ρ₂]}is strongly noetherian for allρ₁ ≤ ρ₂.TauCeti.WittVector.RadiusRing.isOpenQuotientMap_restrictedSeries_toIntervalRing: the evaluationA⟨X⟩ → B,X ↦ [ϖ] ^ b / p ^ a, is an open quotient map whenρ₁ ^ a = v(ϖ) ^ b.
References #
- K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016, no. 8, 2544–2567; arXiv:1410.5160v3, Theorem 3.2, Lemma 4.9, Theorem 4.10 and Remark 4.11.
The interval ring is an open quotient of restricted series over the radius ring (Kedlaya,
Lemma 4.9, third isomorphism, surjectivity). Let ρ₁ ≤ ρ₂, a ≠ 0 and ρ₁ ^ a = v(ϖ) ^ b. A
continuous ring homomorphism ψ : A^{ρ₂}⟨X⟩ → B^{[ρ₁, ρ₂]} extending the coefficient map and
sending X to [ϖ] ^ b / p ^ a is an open quotient map. Such a ψ exists, and is unique, by
TauCeti.WittVector.RadiusRing.existsUnique_continuous_denseRange_restrictedSeries_toIntervalRing.
Kedlaya's Theorem 4.10. For ρ₁ ≤ ρ₂, the ring B^{[ρ₁, ρ₂]}{T/c} of restricted power
series over the interval ring in finitely many variables is noetherian, for all positive radii c.
After numbering the variables, it is a quotient of A^{ρ₂}{T/c, U/ρ₁⁻¹}
(TauCeti.WittVector.RadiusRing.restrictedEvalIntervalRing_surjective), which is noetherian by
Kedlaya's Theorem 3.2.
The interval ring B^I is strongly noetherian (Kedlaya, Theorem 4.10 and Remark 4.11),
for all radii ρ₁ ≤ ρ₂: each completed Huber algebra B^I⟨X₁, …, Xₙ⟩ is the Gauss-normed ring
B^I{X₁, …, Xₙ} of unit-radius restricted series, which is noetherian by
TauCeti.WittVector.isNoetherianRing_isRestricted_subring_intervalRing.