Generating an ideal by successive approximation

In a complete normed ring, let F be a finite subset and S a set. If every element y of S can be approximated by a combination of F up to an error of at most ε ‖y‖, for a fixed ε < 1, with coefficients bounded in terms of ‖y‖ and with the error again in S, then S lies in the left ideal generated by F (TauCeti.subset_idealSpan_of_approx). Iterating the approximation on the errors gives convergent coefficient series. Taking for S a left ideal containing F, whose errors automatically stay in S, this is how Gröbner-type arguments prove that ideals of complete normed rings are finitely generated, as in Kedlaya's proof that rings of restricted power series over a Euclidean normed ring are noetherian. Taking for S a set that is not an ideal is how Kedlaya obtains Euclidean division from a division whose remainder is either of smaller degree or smaller by a uniform factor.

When the norm is ultrametric, the bound ‖b x‖ * ‖x‖ ≤ ‖y‖ on the coefficients of a single approximation survives the iteration: every approximated y is exactly a combination ∑ x ∈ F, a x * x with ‖a x‖ * ‖x‖ ≤ ‖y‖ (TauCeti.exists_eq_sum_mul_of_approx). This gives strict generating systems of ideals of Tate algebras.

References

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

theorem TauCeti.subset_idealSpan_of_approx {A : Type u_1} [NormedRing A] [CompleteSpace A] {S : Set A} {F : Finset A} {ε : ℝ} (hε1 : ε < 1) (happrox : ∀ y ∈ S, ∃ (b : A → A), (∀ x ∈ F, ‖b x‖ * ‖x‖ ≤ ‖y‖) ∧ y - ∑ x ∈ F, b x * x ∈ S ∧ ‖y - ∑ x ∈ F, b x * x‖ ≤ ε * ‖y‖) : S ⊆ ↑(Ideal.span ↑F)

Successive approximation along a set. In a complete normed ring, let F be a finite subset and ε < 1. If every y ∈ S is within ε ‖y‖ of a combination ∑ x ∈ F, b x * x with ‖b x‖ * ‖x‖ ≤ ‖y‖ whose error again lies in S, then S lies in the left ideal generated by F.

theorem TauCeti.exists_eq_sum_mul_of_approx {A : Type u_1} [NormedRing A] [IsUltrametricDist A] [CompleteSpace A] {S : Set A} {F : Finset A} {ε : ℝ} (hε1 : ε < 1) (happrox : ∀ y ∈ S, ∃ (b : A → A), (∀ x ∈ F, ‖b x‖ * ‖x‖ ≤ ‖y‖) ∧ y - ∑ x ∈ F, b x * x ∈ S ∧ ‖y - ∑ x ∈ F, b x * x‖ ≤ ε * ‖y‖) {y : A} (hy : y ∈ S) : ∃ (a : A → A), y = ∑ x ∈ F, a x * x ∧ ∀ x ∈ F, ‖a x‖ * ‖x‖ ≤ ‖y‖

Strict successive approximation along a set. In a complete ultrametric normed ring, under the hypotheses of TauCeti.subset_idealSpan_of_approx, every y ∈ S is a combination ∑ x ∈ F, a x * x with ‖a x‖ * ‖x‖ ≤ ‖y‖: the bound on the coefficients of a single approximation step survives the iteration.