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.