### Constructive Algebra

• A note on a remark of Gavin Wraith, given a coherent presentation of the notion of strictly Henselian ring.
• A note on Lorenzen's work, jww Henri Lombardi and Stefan Neuwirth
• Linear Equations

A simple proof of a result of Sharpe about linear equations over rings.

• How to build points of a curve

A fundamental algorithm (from Abhyankar). It follows from this that the space of valuation of an algebraic curves has enough points over an algebraically closed field.

• Space of Valuations

We give a pointfree description of the space of valuations of an integral domain, with some applications for characterising (integral) Prufer domains. We apply this to the beginning of a constructive theory of sheaf theory, with a natural example of scheme (algebraic curves with a cohomological definition of the genus). Here is a little update. (A sharpening of the cut-elimination statement for the space of valuation, and the remark that for Prufer ring, the isomorphism with the Zariski spectrum can be proved without cut-elimination.)

• On seminormality

Swan gave an elementary definition of seminormality, a notion due to Traverso, with an indirect proof that this is equivalent to another condition on Picard groups. We give a direct proof of this equivalence. See here for an improvement (that can be implemented in a computer algebra system)

• Zariski Main Theorem

Work in progress with Henri Lombardi and Herve Perdry. We explicit the algorithm implicit in Peskine's proof of Zariski Main Theorem and apply it to a small example. This is used to reduce "multidimensional Hensel extensions" of a local ring to simple Hensel extensions. Here is a sharper statement of the constructive version of Zariski Main Theorem.

• Space of valuation

We develop the basic constructive theory of valuative dimension, following Jaffard. In particular, we prove that if R is a Prufer domain then Kdim R[X1,...,Xn] is n + Kdim R

• Dedekind-Mertens Lemma.

A short proof of the fundamental Dedekind-Mertens Lemma. This implies directly Dedekind Prague's Theorem.

• talk1 talk2

Tutorials in Oberwolfach about "infinite objects in constructive mathematics"

• Remarks on Forster-Swan

Thanks to Lionel Ducos, we simplify a little the argument of the paper on generators of modules and prove Bass cancellation theorem constructively

• Generating non-Noetherian Modules Constructively

with Henri Lombardi and Claude Quitte. An improvement of a paper of Heitmann, with a simple constructive proof of a generalisation of the Forster-Swan theorem. Appears in Manuscripta Mathematica (2004)

• A Note on Kronecker's Theorem on Algebraic Sets

A simple and constructive proof of Kronecker's theorem. Appears in C. R. Math. Acad. Sci. Paris 338 (2004), no. 4, 291--294.

Thanks to Harold Edwards help, here is a version of the proof which I think would have been accepted by Kronecker

• Dynamical methods in algebra

Presented at the Calculemus meeting, September 2003. Contains a general introduction to dynamical methods in algebra. One way to see this is as an application of completness of hyper-resolution.

• Le bord d'un point

Contains a simple direct inductive definition of Krull dimension. This is remarkably close to Menger's definition: for spectral space X, it is of dimension <= k+1 iff any compact open has a boundary of dimension <= k

• Krull dimension dim.ps dim.dvi dim.pdf

With Henri Lombardi. We give the foundations of a constructive theory of Krull dimension

• A constructive version of Krull's Principal Ideal Theorem for Noetherian rings Krull.ps
• Algebraic Closure

We present a construction of the algebraic closure following Joyal (1975). This is a concrete illustration of algebraic logic (quantifiers as adjoints, monadic algebra), and gives an elegant formulation of quantifier elimination.

• Tiling Rectangles

If a rectangle is tiled by rectangles each of which has at least one integral side, then the tiled rectangle has at least one integral side. There is a simple proof using integrals. We present an algebraic and constructive version of this argument.