[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.