Seminormal rings (following Thierry Coquand)

The Traverso-Swan theorem says that a reduced ring A is seminormal if and only if the natural homomorphism Pic A Pic A[X] is an isomorphism ([18, 17]). We give here all the details needed to understand the elementary constructive proof for this result given by Thierry Coquand in [2]. 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 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.

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Henri Lombardi, Claude Quitté
• Keywords: Elementary Constructive Proof, Ideal Objects, Natural Homomorphism Pic, TCS 2008, Theoretical Computer Science