Lattice-ordered groups generated by ordered groups and regular systems of ideals

Lattice-ordered groups generated by ordered groups and regular systems of ideals (pdf)
Rocky Mountain Journal of Mathematics 49, (2019), 1449--1489. On arXiv ArXiv 1701.05115 . On hal hal-01427208
with Thierry Coquand and Stefan Neuwirth. (2018).

Abstract
Unbounded entailment relations, introduced by [Paul Lorenzen 1951], are a slight variant of a notion which plays a fundamental role in logic see [Scott 1974] and in algebra. We propose to define systems of ideals for a commutative ordered monoid G as unbounded single-conclusion entailment relations that preserve its order and are equivariant: they describe all morphisms from G to meet-semilattice-ordered monoids generated by (the image of) G. Taking an article by [Lorenzen 1953] as a starting point, we also describe all morphisms from a commutative ordered group G to lattice-ordered groups generated by G through unbounded entailment relations that preserve its order, are equivariant, and satisfy a ``regularity'' property invented by [Lorenzen 1950]; we call them regular systems of ideals. In particular, the free lattice-ordered group generated by G is described by the finest regular system of ideals for G, and we provide an explicit description for it; it is order-reflecting if and only if the morphism is injective, so that the Lorenzen-Clifford-Dieudonné theorem fits in our framework. In fact, Lorenzen's research in algebra is motivated by the system of Dedekind ideals for the divisibility group of an integral domain R; in particular, we provide an explicit description of the lattice-ordered group granted by Wolfgang Krull's ``Fundamentalsatz'' if (and only if) R is integrally closed as the ``regularisation'' of the Dedekind system of ideals.