Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Seminormal Rings (following Thierry Coquand)

Henri Lombardi, Claude Quitté

TL;DR

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.

Abstract

The Traverso-Swan theorem says that a reduced ring A is seminormal if and only if the natural morphism from Pic(A) to Pic(A[X]) is an isomorphism. We give here all the details needed to understand the elementary constructive proof for this result given by Thierry Coquand in the paper: On seminormality. J. Algebra 305, no. 1-3, 577-584, (2006). In this new version we have fixed a little typo in Theorem 3.8: the hypothesis seminormal was missing.

Seminormal Rings (following Thierry Coquand)

TL;DR

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.

Abstract

The Traverso-Swan theorem says that a reduced ring A is seminormal if and only if the natural morphism from Pic(A) to Pic(A[X]) is an isomorphism. We give here all the details needed to understand the elementary constructive proof for this result given by Thierry Coquand in the paper: On seminormality. J. Algebra 305, no. 1-3, 577-584, (2006). In this new version we have fixed a little typo in Theorem 3.8: the hypothesis seminormal was missing.
Paper Structure (6 sections, 31 theorems, 15 equations)

This paper contains 6 sections, 31 theorems, 15 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Traverso-Swan theorem, with integral rings
  4. Introduction
  5. Préliminaires
  6. Théorème de Traverso-Swan. Le cas intègre.

Key Result

Proposition 2.4

Let $P\in\mathbf{A}^{n\times n}$. The matrix $P$ is idempotent and its image is free of rang $r$ if and only if there exist two matrices $X\in\mathbf{A}^{n\times r}$ and $Y\in\mathbf{A}^{r\times n}$ such that $YX=\mathrm{I}_r$ and $P=XY$. Moreover, Another possible characterisation is that the matrix $\mathrm{Diag}(P,0_r)$ is similar to the standard projection matrix $\mathrm{I}_{n+r,r}$.

Theorems & Definitions (33)

  • Proposition 2.4
  • Lemma 2.5
  • Lemma 2.6
  • Proposition 2.7
  • Corollary 2.8
  • Lemma 2.10
  • Theorem 2.11
  • Lemma 3.1
  • Lemma 3.2
  • Theorem 3.3
  • ...and 23 more