Revisiting Zariski Main Theorem from a constructive point of view

TL;DR

This paper revisits the Peskine version of Zariski Main Theorem using constructive mathematics, providing explicit algorithms and avoiding non-constructive arguments, with applications to algorithmic algebra.

Contribution

It offers a constructive reinterpretation of Peskine's Zariski Main Theorem, replacing non-constructive parts with dynamical arguments and deriving algorithmic versions of key algebraic results.

Findings

Provides explicit algorithms from constructive proofs.

Replaces non-constructive minimal prime ideals with dynamical arguments.

Derives algorithmic versions of Multivariate Hensel Lemma and quasi-finite algebra structure theorem.

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 particular we obtain algorithmic versions for the Multivariate Hensel Lemma and the structure theorem of quasi-finite algebras.