Gröbner bases over Tate algebras

International audienceTate algebras are fundamental objects in the context of analytic geometry over the p-adics. Roughly speaking, they play the same role as polynomial algebras play in classical algebraic geometry. In the present article, we develop the formalism of Gröbner bases for Tate algebras. We prove an analogue of the Buchberger criterion in our framework and design a Buchberger-like and a F4-like algorithm for computing Gröbner bases over Tate algebras. An implementation in SM is also discussed