General insertion and extension theorems for localic real functions (Q531326)

In an earlier paper [J. Pure Appl. Algebra 213, No. 6, 1064--1074 (2009; Zbl 1187.06005)], the authors and the reviewer introduced a pointfree version of real-valued (not necessarily continuous or semicontinuous) functions. In the present paper, the authors build on this notion to obtain a general insertion theorem for arbitrary comparable localic real functions that nicely unifies the pointfree versions of the Katětov-Tong insertion theorem (for normal locales) and the Stone insertion theorem (for extremally disconnected locales). This result is a pointfree extension of the well-known topological insertion theorem of \textit{R. Blair} [Czech. Math. J. 31(106), 63--74 (1981; Zbl 0481.54009)] and \textit{E. P. Lane} [in: Topology, Proc. Conf., Vol.~4, No.~2, Ohio Univ. 1979, 463--478 (1980; Zbl 0443.54012)] characterizing the insertion of a continuous real function between two arbitrary comparable real functions. On the way, the authors consider Katětov relations in lattices and study complete separation of sublocales. They then proceed to establish a localic analogue of the topological extension theorem of \textit{S. Mrówka} [Nieuw Arch. Wiskd., III. Ser. 16, 94--111 (1968; Zbl 0183.40901)] that provides a necessary and sufficient condition (in terms of complete separation of certain sublocales) for extending a bounded real function from a complemented sublocale to the whole locale.