Making a restricted series distinguished in one variable

Let R be an ultrametric normed commutative ring with ‖1‖ = 1, and let σ be finite. Separating the variable Y = X none identifies the unit-radius Tate algebra in the variables Option σ with restricted power series in Y over the Tate algebra in the variables σ (TauCeti.Huber.restrictedOptionEquiv). A nonzero series need not be distinguished in Y in this picture: its dominant coefficients may all involve the other variables. This file shows that an isometric R-algebra automorphism of the Tate algebra repairs this. Every nonzero series is carried to one which is distinguished in Y, and whose dominant Y-coefficient differs from a constant of the same norm by less than that norm. Over a complete nonarchimedean field this dominant coefficient is therefore a unit.

This is the input that Weierstrass division in Y, with coefficients in the Tate algebra in the remaining variables, needs in order to prove that Tate algebras are noetherian.

The automorphism is the triangular substitution

Y ↦ Y,    Xᵢ ↦ Xᵢ + Y ^ (b ^ (k i + 1)),

for an enumeration k : σ ≃ Fin n and a base b exceeding every exponent appearing in a monomial of maximal coefficient norm. It sends the monomial X ^ ν to a polynomial which, as a polynomial in Y, is monic of degree ν none + ∑ᵢ b ^ (k i + 1) * ν (some i). These degrees are base-b expansions, so they differ for the finitely many dominant monomials, and the dominant monomial of largest degree gives the distinguished coefficient.

Main results

• TauCeti.MvPowerSeries.exists_algEquiv_isDistinguished: over an ultrametric normed commutative ring, an isometric automorphism makes a nonzero series distinguished in Y, with dominant coefficient close to a constant of the same norm.
• TauCeti.MvPowerSeries.exists_algEquiv_isDistinguished_isUnit: over a complete nonarchimedean field, the dominant coefficient is moreover a unit.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.4.
• The choice of exponents b ^ (k i + 1) and the comparison of base-b expansions follow the proof of Mathlib's Noether normalization lemma, Mathlib.RingTheory.NoetherNormalization.

theorem TauCeti.MvPowerSeries.exists_algEquiv_isDistinguished {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (f : ↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1)) (hf : f ≠ 0) : ∃ (e : ↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1) ≃ₐ[R] ↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1)) (s : ℕ) (a : R), (∀ (g : ↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1)), ‖e g‖ = ‖g‖) ∧ ‖a‖ = ‖f‖ ∧ PowerSeries.IsDistinguished 1 s ↑(Huber.restrictedOptionEquiv (e f)) ∧ ‖(PowerSeries.coeff s) ↑(Huber.restrictedOptionEquiv (e f)) - (algebraMap R ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)) a‖ < ‖f‖

Distinguishing automorphisms of Tate algebras. Over an ultrametric normed commutative ring with ‖1‖ = 1, every nonzero unit-radius restricted series f in the variables Option σ, for finite σ, is carried by an isometric R-algebra automorphism e to a series distinguished in the variable none: written as a restricted series in that variable over the Tate algebra in the variables σ, e f is distinguished of some degree s. Moreover its coefficient in degree s is within less than ‖f‖ of a constant a with ‖a‖ = ‖f‖.

theorem TauCeti.MvPowerSeries.exists_algEquiv_isDistinguished_isUnit {σ : Type u_1} {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [Finite σ] (f : ↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1)) (hf : f ≠ 0) : ∃ (e : ↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1) ≃ₐ[K] ↥(MvPowerSeries.IsRestricted.subring fun (x : Option σ) => 1)) (s : ℕ), PowerSeries.IsDistinguished 1 s ↑(Huber.restrictedOptionEquiv (e f)) ∧ IsUnit ((PowerSeries.coeff s) ↑(Huber.restrictedOptionEquiv (e f)))

Distinguishing automorphisms of Tate algebras over a field. Over a complete nonarchimedean field K, every nonzero element f of the Tate algebra in the variables Option σ, for finite σ, is carried by a K-algebra automorphism to a series which, as a restricted series in the variable none over the Tate algebra in the variables σ, is distinguished of some degree s with a unit coefficient in degree s. These are the hypotheses of Weierstrass division and preparation over the Tate algebra in the variables σ.