A direct constructive proof of this result, extracted from Northcott's book on Finite Free Resolutions
A simple proof of a result of Sharpe about linear equations over rings.
With Henri Lombardi and Claude Quitte. To be presented at the conference Mega 09.
Talk given in Munich, December 07
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.
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.)
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)
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.
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
Another proof of a key lemma of Galois theory, as seen by Dedekind
A short proof of the fundamental Dedekind-Mertens Lemma. This implies directly Dedekind Prague's Theorem.
Thanks to Lionel Ducos, we simplify a little the argument of the paper on generators of modules and prove Bass cancellation theorem constructively
Presents the work on number of generator of modules from the point of view of proof theory/intuitionism
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 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
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.
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
With Henri Lombardi. We give the foundations of a constructive theory of Krull dimension
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.
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.