arXiv subjects
Publications and source records attributed to Henri Lombardi.
We study etale topology and the notion of Azumaya algebra over a commutative ring constructively. As an application of the syntactic version of Barr's Theorem, we show the equivalence between two definitions of Azumaya algebra.
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.
This paper is the English translation of the first 4 sections of the article ``Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon. Algèbre et théorie des nombres, 2006'', after some corrections. Sections 5-7 of the original article are treated a bit more simply in the book ``Henri Lombardi and Claude Quitté. Commutative algebra: constructive methods. Finite projective modules. Springer, 2015.'' We study the notion of dimension introduced by Heitmann in his remarkable article ``Generating non-Noetherian modules efficiently, Mich. Math. J., 31, (1084)'' as well as a related notion, only implicit in his proofs. We first develop this within the general framework of the theory of distributive lattices and spectral spaces. -- Cet article est une version corrigée des 4 premières sections de l'article ``Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Mathématiques de Besançon. Algèbre et théorie des nombres, 2006'' Les sections 5 à 7 de l'article original sont traitées de manière un peu plus simple dans ``Henri Lombardi and Claude Quitté. Commutative algebra: constructive methods. Finite projective modules. Springer, 2015.'' Nous étudions la notion de dimension introduite par Heitmann dans son article remarquable ``Generating non-Noetherian modules efficiently, Mich. Math. J., 31, (1084)'', ainsi qu'une notion voisine, seulement implicite dans ses démonstrations. Nous développons ceci d'abord dans le cadre général de la théorie des treillis distributifs et des espaces spectraux. Nous appliquons ensuite cette problématique dans le cadre de l'algèbre commutative.
We define the notion of {\em rational presentation of a complete metric space} in order to study metric spaces from the algorithmic complexity point of view. In this setting, we study some presentations of the space $\czu$ of uniformly continuous real functions over [0,1] with the usual norm: $\norme{f}_{\infty} = {\bf Sup} \{ \abs{f(x)} ; \;0 \leq x \leq 1\}.$ This allows us to have a comparison of a global kind between complexity notions attached to these presentations. In particular, we get a generalisation of Hoover's results concerning the {\sl Weierstrass approximation theorem in polynomial time}. We get also a generalisation of previous results on analytic functions which are computable in polynomial time.
We give an elementary proof of the theorem which states that a finite unramified algebra over a discrete field is tracically étale. -- Nous donnons une démonstration élémentaire du théorème selon lequel toute algèbre nette sur un cors discret est étale, de dimension finie comme espace vectoriel et traciquement étale.
The central objective of this article is to provide an elementary proof of the following theorem, of which we are unaware of any trace in the existing literature. If $B$ is a net finite free algebra over a commutative ring $A$, then it is tracically étale (its trace form is nondegenerate) and a fortiori étale over A. As indicated in the title, our proof is based on algebraic identities. This confirms the implicit adage that much of the most abstract commutative algebra is concentrated in algebraic identities concerning matrices of polynomials over an arbitrary commutative ring. -- -- -- L'objectif central de cet article est de donner une démonstration élémentaire du théorème suivant, dont nous ne connaissons pas de trace dans la littérature existante. Si $B$ est une algèbre libre finie nette sur $A$, alors elle est traciquement étale (sa forme trace est non dégénérée) et à fortiori étale sur $A$. Comme indiqué dans le titre, notre démonstration est basée sur des identités algébriques. Cela confirme l'adage implicite selon lequel une grande partie de l'algèbre commutative la plus abstraite se concentre dans des identités algébriques concernant les matrices de polynômes sur un anneau commutatif arbitraire.
We give a general method for producing various effective Null and Positivstellensätze, and getting new Positivstellensätze in algebraically closed valued fields and ordered groups. These various effective Nullstellensätze produce algebraic identities certifying that some geometric conditions cannot be simultaneously satisfied. We produce also constructive versions of abstract classical results of algebra based on Zorn's lemma in several cases where such constructive version did not exist. For example, the fact that a real field can be totally ordered, or the fact that a field can be embedded in an algebraically closed field. Our results are based on the concepts we develop of dynamical proofs and simultaneous collapse.
We give an elementary and constructive proof for a theorem of de Smit et Lenstra. Note: In version 1, was missing the proof that "completely secant" implies "1-secant"
There are several classical characterisations of the valuative dimension of a commutative ring. Constructive versions of this dimension have been given and proven to be equivalent to the classical notion within classical mathematics, and they can be used for the usual examples of commutative rings. To the contrary of the classical versions, the constructive versions have a clear computational content. This paper investigates the computational relationship between three possible constructive definitions of the valuative dimension of a commutative ring. In doing so, it proves these constructive versions to be equivalent within constructive mathematics.
This note aims to construct an ``intrinsic'' splitting field for the polynomial $Y^n-1$ over the rational field $\bf Q$, in a way that Gauss, Kummer, Kronecker and Bishop would have liked. Contrary to the usual presentations, our construction does not use any splitting field of $Y^n-1$ which would be given before demonstrating the irreducibility of the cyclotomic polynomial.
The category of distributive lattices is, in classical mathematics, antiequivalent to the category of spectral spaces. We give here some examples and a short dictionary for this antiequivalence. We propose a translation of several abstract theorems (in classical mathematics) into constructive ones, even in the case where points of a spectral space have no clear constructive content. La catégorie des treillis distributifs et celle des espaces spectraux sont antiéquivalentes (en mathématiques classiques). Nous proposons ici un petit dictionnaire pour cette antiéquivalence. Nous indiquons comment un certain nombre de théorèmes étranges des mathématiques classiques obtiennent un contenu constructif grâce à cette antiéquivalence, même dans le cas, fréquent, où les points des espaces spectraux considérés n'ont pas de contenu constructif clair.
We propose a slight modification of the Berlekamp-Massey Algorithm for obtaining the minimal polynomial of a given linearly recurrent sequence. Such a modification enables to explain it in a simpler way and to adapt it to lazy evaluation.
In Chapter 3 of his Notes on constructive mathematics, Martin-L{ö}f describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of computable functions is not needed from a constructive point of view. We give in this paper a constructive theory of ordinals that is similar to Martin-L{ö}f's theory, but based only on the two relations "$x \leq y$" and "$x < y$", i.e., without considering sequents whose intuitive meaning is a classical disjunction. In our setting, the operation "supremum of ordinals" plays an important rôle through its interactions with the relations "$x \leq y$" and "$x < y$". This allows us to approach as much as we may the notion of linear order when the property "$α\leq β$ or $β\leq α$" is provable only within classical logic. Our aim is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties. Note that by adding classical logic, we would recover the ordinals of usual classical mathematics, at the cost of a loss of computability for most statements given in the usual form.
We compare two henselisations of a residually discrete valuation domain. Our constructive proof that a certain natural morphism is an isomorphism is also a proof in classical mathematics. Although this isomorphism is implicitly accepted as obvious in the literature, it seems that no proof was previously available.
Lorenzen's ``Algebraische und logistische Untersuchungen über freie Verbände'' appeared in 1951 in The Journal of Symbolic Logic. These ``Investigations'' have immediately been recognised as a landmark in the history of infinitary proof theory. Their approach and method of proof have not been incorporated into the corpus of proof theory. Lorenzen proves the admissibility of cut by double induction, on the cut formula and on the complexity of the derivations, without using any ordinal assignment, contrary to the presentation of cut elimination in most standard texts on proof theory. We propose this introduction with the intent of giving a new impetus to their reception. The ``Investigations'' are best known for providing a constructive proof of consistency for ramified type theory without axiom of reducibility. They do so by showing that it is a part of a trivially consistent ``inductive calculus'' that describes our knowledge of arithmetic without detour. The proof resorts only to the inductive definition of formulas and theorems. They propose furthermore a definition of a semilattice, of a distributive lattice, of a pseudocomplemented semilattice, and of a countably complete boolean algebra as deductive calculuses, and show how to present them for constructing conservatively the respective free object over a given preordered set. They illustrate that lattice theory is a bridge between algebra and logic for which the construction of an element corresponds to a step in a proof. We shall describe the history of their reception, which focusses mainly on the omega-rule. The fruitfulness of this device is immediately recognised by Kurt Schütte. It triggers the analysis by Ackermann (1951) of the infinitary inductive definition of the accessibility predicate with the goal of proving transfinite induction up to ordinal terms beyond epsilon_0, which is also taken over by Schütte (1952).
Let M be a finitely generated submodule of a free module over a multivariate polynomial ring with coefficients in a discrete coherent ring. We prove that its module MLT(M ) of leading terms is countably generated and provide an algorithm for computing explicitly a generating set. This result is also useful when MLT(M ) is not finitely generated. Suppose that the base ring is strongly discrete coherent. We provide a Buchberger-like algorithm and prove that it converges if, and only if, the module of leading terms is finitely generated. We also provide a constructive version of Hilbert's syzygy theorem by following Schreyer's method.
In 1955, Paul Lorenzen is a mathematician who devotes all his research to foundations of mathematics, on a par with Hans Hermes, but his academic background is algebra in the tradition of Helmut Hasse and Wolfgang Krull. This shift from algebra to logic goes along with his discovery that his ``algebraic works [...] have been concerned with a problem that has formally the same structure as the problem of consistency of the classical calculus of logic'' (letter to Carl Friedrich Gethmann dated 14 January 1988). After having provided a proof of consistency for arithmetic in 1944 and published it in 1951, Lorenzen inquires still further into the foundations of mathematics and arrives at the conviction that analysis can also be given a predicative foundation. Wilhelm Ackermann as well as Paul Bernays have pointed out to him in 1947 that his views are very close to those proposed by Hermann Weyl in Das Kontinuum (1918): sets are not postulated to exist beforehand; they are being generated in an ongoing process of comprehension. This seems to be the reason for Lorenzen to get into contact with Weyl, who develops a genuine interest into Lorenzen's operative mathematics and welcomes with great enthusiasm his Einf{ü}hrung in die operative Logik und Mathematik (1955), which he studies line by line. This book's aim is to grasp the objects of analysis by means of inductive definitions; the most famous achievement of this enterprise is a generalised inductive formulation of the Cantor-Bendixson theorem that makes it constructive. This mathematical kinship is brutally interrupted by Weyl's death in 1955; a planned visit by Lorenzen at the Institute for Advanced Study in Princeton takes place only in 1957--1958. As told by Kuno Lorenz, Lorenzen's first Ph.D. student, a discussion with Alfred Tarski during this visit provokes a turmoil in Lorenzen's operative research program that leads to his abandonment of language levels and to a great simplification of his presentation of analysis by distinguishing only between ``definite'' and ``indefinite'' quantifiers: the former govern domains for which a proof of consistency is available and secures the use of the law of excluded middle; the latter govern those for which there isn't, e.g. the real numbers. Lorenzen states in his foreword to Differential und Integral (1965) that he is faithful to Weyl's approach of Das Kontinuum in this simplification. This history motivates a number of mathematical and philosophical issues about predicative mathematics: how does Weyl's interest into Lorenzen's operative mathematics fit with his turn to Brouwer's intuitionism as expressed in ``{Ü}ber die neue Grundlagenkrise der Mathematik'' (1921)? Why does Lorenzen turn away from his language levels and how does this turn relate to Weyl's conception of predicative mathematics? What do Lorenzen's conceptions of mathematics reveal about Weyl's conceptions?
In this memoir, we seek to construct a dynamical theory as complete as possible to describe the algebraic properties of the field of real numbers in constructive mathematics without axiom of dependent choice. We propose a theory which turns out to be very close to the theory of real closed local rings in classical mathematics. The theory of real closed rings is presented here in constructive form as a natural purely equational theory, which uses virtual root functions introduced in previous work. This work is also a first step through an essential goal for the future, which is to obtain a constructive version of o-minimal structures.