[retour]

##
Seminormal rings (following Thierry Coquand)

english pdf.
Version française.

with Claude Quitté

Theoretical Computer Science ** 392**, (2008), 113-127.
** Abstract :**

The Traverso-Swan theorem says that a reduced ring A is seminormal if and only if
the natural homomorphism form Pic(A) to Pic(A[X]) is an isomorphism (Traverso 1970, Swan 1980).
We give here all the details
needed to understand the elementary constructive proof
for this result given by Thierry Coquand
in:

Coquand T. On seminormality J. Algebra 305, (2006), 577-584.

This example is typical of a new constructive method.
The final proof is simpler than the initial classical one.

More important: the classical argument by absurdum using
``an abstract ideal object'' is deciphered with a general technique
based on the following idea: purely ideal objects constructed using TEM and Choice may be replaced by concrete objects that are ``finite approximations'' of these ideal objects.