Revisiting Zariski Main Theorem from a constructive point of view

with MariEmi Alonso and Thierry Coquand.

Abstract :

This paper deals with the Peskine version of Zariski Main Theorem published in 1965 and discusses some applications. It is written in the style of Bishop's constructive mathematics. Being constructive, each proof in this paper can be interpreted as an algorithm for constructing explicitly the conclusion from the hypothesis. The main non-constructive argument in the proof of Peskine is the use of minimal prime ideals. Essentially we substitute this point by two dynamical arguments; one about gcd's, using subresultants, and another using our notion of strong transcendence.
In fact we prove a slightly different version of Peskine Theorem.
Let  A  be a ring with an ideal  I  and  B=A[x1 ,…,xn ]  be a finitely generated extension of  A   such that  B/IB  is a finite  A/I-algebra, then there exists  s  in  1+IB  such that  s, sx1 , …, sxn   are integral over  A.
As consequences we obtain algorithmic versions for the Multivariate Hensel Lemma and the structure theorem of quasi-finite algebras.