Abstract :
Let E be the ring of integer valued polynomials over Z . This ring is known to be a Prüfer domain. But it seems there does not exist an algorithm for inverting a nonzero finitely generated ideal of E.
In this note we show how to obtain such an algorithm by deciphering a
classical abstract proof that uses localisations of E at all prime ideals of E.
This confirms a general program of deciphering abstract
classical proofs in order to obtain algorithmic proofs.
Résumé :
Nous notons E l'anneau des polynômes à valeurs entières (en une variable) sur Z.
Il est connu que cet anneau est un anneau de Prüfer, par exemple parce que l'on a étudié ses idéaux premiers et que les localisés correspondants sont des anneaux de valuation.
Cependant, il ne semble pas que l'on connaisse d'algorithme pour inverser un idéal de type fini non nul de E.
Nous montrons dans cette note comment le décryptage de la preuve classique évoquée ci-dessus permet de résoudre le problème algorithmique correspondant.
Ceci confirme la faisabilité du programme général de réécriture sous le slogan : les mathématiques classiques sont constructives, si l'on veut bien se donner la peine de regarder en détail ce qui se cache derrière les raccourcis audacieux usuellement pratiqués.