Seminormal rings (following Thierry Coquand)
with Claude Quitté
Theoretical Computer Science 392, (2008), 113-127.
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
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.