Tate algebras satisfy the Rückert hypotheses

Let K be a complete nonarchimedean field and T = K⟨X₁, …, Xₙ⟩ a Tate algebra. The inclusion of polynomials T[Y] → T⟨Y⟩ into the Tate algebra in one more variable satisfies the Rückert hypotheses of TauCeti.RingTheory.Polynomial.Rueckert, with the Weierstrass polynomials as the distinguished set: the monic polynomials ω which are distinguished of degree deg ω at the unit radius, equivalently whose Gauss norm is one.

• Monic factors of Weierstrass polynomials are Weierstrass polynomials (TauCeti.PowerSeries.IsDistinguished.of_dvd).
• Weierstrass division identifies T[Y] ⧸ (ω) with T⟨Y⟩ ⧸ (ω) (TauCeti.PowerSeries.IsDistinguished.polynomialQuotientEquiv).
• After an automorphism of K⟨X, Y⟩ every nonzero series is distinguished in Y with a unit dominant coefficient (TauCeti.MvPowerSeries.exists_algEquiv_isDistinguished_isUnit), and Weierstrass preparation makes it a unit multiple of a Weierstrass polynomial.

The general descent results then pass from T to T⟨Y⟩; this is how unique factorisation of Tate algebras is proved (TauCeti.MvPowerSeries.uniqueFactorizationMonoid).

Main results

• TauCeti.MvPowerSeries.isRueckert_polynomialToRestricted: the Rückert hypotheses for T[Y] → T⟨Y⟩ and the Weierstrass polynomials.

References

• S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis, §§5.2.1–5.2.5.

theorem TauCeti.MvPowerSeries.isRueckert_polynomialToRestricted {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] : (↑(PowerSeries.polynomialToRestricted 1)).IsRueckert {p : Polynomial ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) | p.Monic ∧ PowerSeries.IsDistinguished 1 p.natDegree ↑p}

Tate algebras satisfy the Rückert hypotheses. The inclusion of polynomials over the Tate algebra T = K⟨X₁, …, Xₙ⟩ into the Tate algebra T⟨Y⟩ in one more variable satisfies the Rückert hypotheses for the Weierstrass polynomials: the monic polynomials over T which are distinguished of their degree at the unit radius.