The Constructive Lift Monad

The lift monad is the construction which to a poset freely adjoins a bottom<br />element to it, or equivalently (from the classical viewpoint), the construction which freely adjoins suprema for subsets with at most one element. In constructive mathematics (i.e. inside a topos), these two constructions are no longer equivalent, since the equivalence is based on the boolean reasoning that a set with at most one element either is a singleton {x}, or is empty.<br />Likewise based on boolean reasoning is the proof of two important properties of the lift monad T :<br />1) If a poset C has filtered suprema, then so does TC.<br />2) Every poset with a bottom element ? is "free", i.e. comes about by<br />applying T to some poset (namely the original poset less the bottom).<br />Both these properties fail to hold constructively, if the lift monad is interpreted<br />as "adding a bottom"; see Remark below. If, on the other hand,<br />we interpret the lift monad as the one which freely provides supremum for<br />each subset with at most one element (which is what we shall do), then the first property holds; and we give a necessary and sufficient condition that the second does. Finally, we shall investigate the lift monad in the context of (constructive) locale theory. I would like to thank Bart Jacobs for guiding me to the literature on Z-systems; to Gonzalo Reyes for calling my attention to Barr's work on totally connected spaces; to Steve Vickers for some pertinent correspondence.<br />I would like to thank the Netherlands Science Organization (NWO) for supporting my visit to Utrecht, where a part of the present research was carried out, and for various travel support from BRICS.