Tate algebras are unique factorisation domains

Over a complete nonarchimedean field K, the Tate algebra K⟨X₁, …, Xₙ⟩ is a unique factorisation domain. By Mathlib's UniqueFactorizationMonoid.instIsIntegrallyClosed it is therefore integrally closed, so Mathlib's going-down theorem applies to every integral extension of a Tate algebra by a domain, such as the Noether normalisation of an affinoid domain.

The proof is by induction on the number of variables, writing K⟨X, Y⟩ as the univariate Tate algebra K⟨X⟩⟨Y⟩. The inclusion K⟨X⟩[Y] → K⟨X⟩⟨Y⟩ satisfies the Rückert hypotheses for the Weierstrass polynomials (TauCeti.MvPowerSeries.isRueckert_polynomialToRestricted), and Rückert's factorial descent (RingHom.IsRueckert.uniqueFactorizationMonoid) passes unique factorisation from K⟨X⟩ to K⟨X⟩⟨Y⟩.

Main results

• TauCeti.MvPowerSeries.uniqueFactorizationMonoid: the Tate algebra in finitely many variables over a complete nonarchimedean field is a unique factorisation domain.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §5.2.6, Theorem 1, using the descent of §5.2.5.

instance TauCeti.MvPowerSeries.uniqueFactorizationMonoid {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_2} [Finite σ] : UniqueFactorizationMonoid ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)

Tate algebras are unique factorisation domains. Over a complete nonarchimedean field K, the Tate algebra K⟨X₁, …, Xₙ⟩ in finitely many variables is a unique factorisation domain.