Restricted power series over a Euclidean normed ring are noetherian #
Let R be a complete ring whose norm is multiplicative and ultrametric, and let
deg : R → ℕ be a Euclidean degree compatible with the norm:
deg y = deg xwhenever‖x - y‖ < ‖x‖, so the degree only sees the leading part of an element;- for
x ≠ 0, everyycan be writteny = z * x + wwith‖w‖ ≤ ‖y‖and eitherw = 0ordeg w < deg x.
Then for every finite set of variables σ and all positive radii c : σ → ℝ, the ring
R{T/c} of restricted power series with the Gauss norm at the radii c is left noetherian
(TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_division). This is Kedlaya's
analogue of the Hilbert basis theorem, stated for an abstract Euclidean normed ring. Kedlaya
proves it for the completion A^r of W(𝒪_L)[[x] : x ∈ L] for the Gauss norm λ_r, which is
Euclidean in this sense for the degree read off from its Newton polygon (his Remark 2.7 and
Proposition 2.9), and deduces that the rings B^I of the Fargues–Fontaine curve are strongly
noetherian. A complete nonarchimedean division ring satisfies the
hypotheses with deg = 0, so its Tate algebras at arbitrary radii are left noetherian
(TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring).
The argument gives more than finite generation. Every left ideal H has finitely many nonzero
elements x such that each y ∈ H is a combination ∑ a x * x with ‖a x‖ * ‖x‖ ≤ ‖y‖
(TauCeti.MvPowerSeries.exists_finset_eq_sum_mul_isRestricted_subring_of_division): no
cancellation between the terms is needed to represent y. For Tate algebras at unit polyradius
the generators can be normalised to Gauss norm one, and the coefficients are then bounded by
‖y‖ (Ideal.exists_finset_norm_eq_one_isRestricted_subring). In particular, the map
(a x)ₓ ↦ ∑ a x * x from the finite free module with the maximum norm onto H induces on H
its subspace topology, making H complete and hence closed
(TauCeti.MvPowerSeries.isClosed_ideal_isRestricted_subring_of_division).
Running the same Gröbner reduction on an arbitrary series y whenever y is strictly farther from
0 than from H — using an element of H strictly closer to y than ‖y‖ to supply the divisor
at the leading index of y — shows that every left ideal is strictly closed: for every y, the
coset y + H has an element of minimal Gauss norm
(TauCeti.MvPowerSeries.exists_norm_sub_le_isRestricted_subring_of_division,
Ideal.exists_norm_sub_le_isRestricted_subring), even when the coefficient ring is not spherically
complete.
Proof #
The argument is a Gröbner-basis argument. Fix a monomial order on the exponents. The leading
index of a nonzero restricted series is the largest exponent, for the monomial order, at which
its weighted coefficient norm attains the Gauss norm. For an ideal H, the pairs (leading
index, degree of the leading coefficient) of the nonzero elements of H lie in the
well-quasi-ordered set (σ →₀ ℕ) × ℕ (Dickson's lemma). So finitely many elements of H
realise all the minimal pairs, and every nonzero element of H has a pair above one of theirs.
Fix ε < 1 bounding, relative to the norm, the weighted coefficients of these finitely many
elements beyond their leading indices. Let y have ‖y‖ ≤ M and ‖y‖ > θ ≥ ε M, and suppose some
h ∈ H satisfies ‖y - h‖ < ‖y‖ (for instance h = y when y ∈ H). Then h shares the leading
index and leading-coefficient degree of y. A reduction step divides the leading coefficient of y
by the leading coefficient of a chosen x, shifted to the leading index of y. This replaces that
coefficient by a remainder of smaller degree or of weighted norm at most θ. It changes
coefficients at larger indices only by at most ε M ≤ θ, which by the compatibility of deg with
the norm keeps the degrees of the large ones. Recording, at each index, one more than the degree of
each coefficient of weighted norm above θ, reduction strictly decreases in the colexicographic
order. That order is well founded:
- for
y ∈ Handθ = ε ‖y‖, after finitely many stepsyis withinε ‖y‖of a combination∑ b x * xof the chosen elements with‖b x‖ * ‖x‖ ≤ ‖y‖; iterating gives a convergent expansion ofywhose ultrametric coefficient bound survives (TauCeti.exists_eq_sum_mul_of_approx); - for arbitrary
yat positive distancedfromHandθ = max d (ε ‖y‖), finitely many steps produceg ∈ Hwith‖y - g‖ ≤ max d (ε ‖y‖), and iterating untilεⁿ ‖y‖ ≤ dattainsd.
This follows Kedlaya's proof, with two reorganisations: Dickson's lemma is applied directly to
the pairs above instead of to Kedlaya's minimal leading degrees d_I, and his argument by
contradiction on an infinite reduction sequence is replaced by the well-founded potential.
Main results #
TauCeti.MvPowerSeries.exists_finset_eq_sum_mul_isRestricted_subring_of_division: every left ideal of restricted power series over a complete ring with a multiplicative ultrametric norm and a compatible Euclidean degree has a finite strict generating system.TauCeti.MvPowerSeries.isClosed_ideal_isRestricted_subring_of_divisionandTauCeti.MvPowerSeries.exists_norm_sub_le_isRestricted_subring_of_division: every left ideal is closed and every coset contains an element of minimal Gauss norm.Ideal.exists_finset_eq_sum_mul_isRestricted_subring,Ideal.exists_finset_norm_eq_one_isRestricted_subring, andIdeal.exists_norm_sub_le_isRestricted_subring: the same for Tate algebras over a complete nonarchimedean division ring, with generators of Gauss norm one at unit polyradius.TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_division: restricted power series at arbitrary positive radii in finitely many variables over a complete ring with a multiplicative ultrametric norm and a compatible Euclidean degree form a left noetherian ring.TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring: Tate algebras in finitely many variables at arbitrary positive radii over a complete nonarchimedean division ring are left 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, Theorem 3.2 and Lemmas 3.8–3.9.
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.6, Theorem 1, and §5.2.7, Proposition 2.
Strict generators of ideals of restricted power series, from the argument of Kedlaya's
Theorem 3.2 for an abstract Euclidean normed ring.
Let R be a complete ring with a multiplicative ultrametric norm, and deg : R → ℕ
a degree such that deg y = deg x whenever ‖x - y‖ < ‖x‖, and such that for x ≠ 0 every y
can be divided as y = z * x + w with ‖w‖ ≤ ‖y‖ and either w = 0 or deg w < deg x. Then
for finitely many variables and all positive radii c, every left ideal H of the ring of
restricted power series has a finite set F of nonzero elements such that every y ∈ H is a
combination ∑ x ∈ F, a x * x with ‖a x‖ * ‖x‖ ≤ ‖y‖. In particular F generates H, and
F is empty when H = ⊥.
Left ideals of restricted power series over a Euclidean normed ring are closed. Under the
hypotheses of exists_finset_eq_sum_mul_isRestricted_subring_of_division, every left ideal H of
IsRestricted.subring c has a finite strict generating system and is therefore complete and closed
for the Gauss norm.
Least-norm coset representatives for ideals of restricted power series. Under the
hypotheses of exists_finset_eq_sum_mul_isRestricted_subring_of_division, every left ideal H is
strictly closed: for every restricted series y, there is h ∈ H minimising ‖y - h‖ over H.
Kedlaya's Hilbert basis theorem for restricted power series, the argument of Kedlaya's
Theorem 3.2 for an abstract Euclidean normed ring.
Let R be a complete ring with a multiplicative ultrametric norm, and deg : R → ℕ
a degree such that deg y = deg x whenever ‖x - y‖ < ‖x‖, and such that for x ≠ 0 every y
can be divided as y = z * x + w with ‖w‖ ≤ ‖y‖ and either w = 0 or deg w < deg x. Then
for finitely many variables and all positive radii c, the ring of restricted power series
with its Gauss norm at the radii c is left noetherian.
Tate algebras are left noetherian. Over a complete nonarchimedean division ring K,
the ring of restricted power series in finitely many variables at arbitrary positive radii c is
left noetherian: K satisfies the hypotheses of
isNoetherianRing_isRestricted_subring_of_division with the zero degree.
Strict generators of ideals of Tate algebras. Over a complete nonarchimedean division ring
K, in finitely many variables and at arbitrary positive radii c, every left ideal H of the
Tate algebra has a finite set F of nonzero elements such that every y ∈ H is a combination
∑ x ∈ F, a x * x with ‖a x‖ * ‖x‖ ≤ ‖y‖.
Strict generators of norm one. Over a complete nonarchimedean division ring K, every
left ideal H of the Tate algebra K⟨X⟩ at unit polyradius in finitely many variables has a
finite set F of generators of Gauss norm one such that every y ∈ H is a combination
∑ x ∈ F, a x * x with ‖a x‖ ≤ ‖y‖. The set F is empty when H = ⊥.
Strict closedness of ideals of Tate algebras ([Bosch, Güntzer, Remmert, Non-Archimedean
Analysis][bosch-guntzer-remmert], §5.2.7, Proposition 2). Over a complete nonarchimedean division
ring K, in finitely many variables and at arbitrary positive radii c, every left ideal H is
strictly closed: for every y, there is h ∈ H minimising ‖y - h‖ over H.