Surjectivity of maps of Tate algebras from lifts of generators

Let Φ : R{Y/d} → S{X/c} be a ring homomorphism between rings of restricted power series with their Gauss norms, over ultrametric normed rings R and S, with R{Y/d} complete (for instance when R is complete), and suppose that Φ does not increase norms. If every constant from a dense additive subgroup D ⊆ S and every variable Xᵢ has a preimage of no larger norm, then Φ is surjective.

Indeed, the polynomials with coefficients in D lift without increasing the norm, since the Gauss norm of a polynomial is the largest weighted norm of its terms. These polynomials are dense (MvPowerSeries.dense_closure_monomial), so the successive approximation argument of Mathlib's controlled_closure_of_complete lifts every element of S{X/c}.

This is how one presents rings of convergent functions on annuli as quotients of Tate algebras at real radii, as in Kedlaya's Lemma 4.9 for the interval rings of the Fargues–Fontaine curve: the lifts of the constants come from an explicit Laurent expansion.

Main results

• MvPowerSeries.surjective_of_exists_lift: a norm-nonincreasing ring homomorphism of Tate algebras with a complete source is surjective when the constants from a dense additive subgroup and the variables lift without increasing the norm.

References

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

theorem MvPowerSeries.surjective_of_exists_lift {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [NormedCommRing R] [IsUltrametricDist R] [NormedCommRing S] [IsUltrametricDist S] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] {d : τ → ℝ} [∀ (j : τ), Fact (0 < d j)] {Φ : ↥(IsRestricted.subring d) →+* ↥(IsRestricted.subring c)} [CompleteSpace ↥(IsRestricted.subring d)] (hΦ : ∀ (f : ↥(IsRestricted.subring d)), ‖Φ f‖ ≤ ‖f‖) {D : AddSubgroup S} (hDense : Dense ↑D) (hC : ∀ a ∈ D, ∃ (f : ↥(IsRestricted.subring d)), Φ f = (algebraMap S ↥(IsRestricted.subring c)) a ∧ ‖f‖ ≤ ‖a‖) (hX : ∀ (i : σ), ∃ (f : ↥(IsRestricted.subring d)), Φ f = ⟨X i, ⋯⟩ ∧ ‖f‖ ≤ c i) : Function.Surjective ⇑Φ

Surjectivity from lifts of generators. Let Φ : R{Y/d} → S{X/c} be a ring homomorphism of Tate algebras that does not increase the Gauss norm, with R{Y/d} complete. If every constant from a dense additive subgroup D of S and every variable Xᵢ is the image of an element of no larger norm, then Φ is surjective.