Temel Kavramlar
The lifting monad on directed-complete partial orders (dcpos) has a rich 2-categorical structure, including universal properties as a Sierpiński cone and a partial product. This enables a constructive analysis of the lifting doctrine, including the cocompleteness of lifting algebras and their symmetric monoidal closed structure.
Özet
The paper presents a comprehensive analysis of the tensorial structure of the lifting doctrine in constructive domain theory, i.e., the theory of directed-complete partial orders (dcpos) over an arbitrary elementary topos. The key insights are:
The universal property of lifting of dcpos as the Sierpiński cone is established, from which it is deduced that (1) lifting forms a Kock–Zöberlein doctrine, (2) lifting algebras, pointed dcpos, and inductive partial orders form canonically equivalent locally posetal 2-categories, and (3) the category of lifting algebras is cocomplete, with connected colimits created by the forgetful functor to dcpos.
The symmetric monoidal closure of the Eilenberg–Moore resolution of the lifting 2-monad is deduced by means of smash products, which are shown to classify both bilinear maps and strict maps, which are proven to coincide in the constructive setting. Several concrete computations of the smash product as dcpo and lifting algebra coequalisers are provided.
The paper highlights the importance of studying constructive domain theory, as modern approaches to programming semantics routinely involve computing recursive functions in non-boolean toposes, where the constructive theory of dcpos is necessary. Many results that appear "obvious" classically have not been established constructively, and the constructive domains behave differently enough from the classical ones that it would not be safe to take these results for granted.