Insertion and extension results for pointfree complete regularity (Q386819)

Since the advent of lower and upper semicontinuity in locales (to the development of which the current authors -- either jointly, solely, or in collaboration with other authors -- have contributed most significantly), there have been insertion-type characterisations of higher separation axioms. An example is that a locale \(L\) is normal precisely if whenever \(f \leq g\), where \(f\) is an upper semicontinuous real function on \(L\) and \(g\) lower semicontinuous, then a continuous real function on \(L\) can be inserted between them [\textit{J. Picado}, Topology Appl. 153, No. 16, 3203--3218 (2006; Zbl 1104.06007)]. Corresponding to this theorem is an extension theorem saying that a closed sublocale of a normal locale is \(C\)-embedded [\textit{J. Gutiérrez García}, J. Pure Appl. Algebra 213, No. 6, 1064--1074 (2009; Zbl 1187.06005)]. As is the case with other works of these authors (individual, joint, or with other collaborators), this paper is lucidly written. It starts with a well-motivated question. In [\textit{J. Gutiérrez García} and \textit{T. Kubiak}, Appl. Gen. Topol. 8, No. 2, 239--242 (2007; Zbl 1152.54020)] a function \(f : X \to [0, 1]\) is called compact-like if \(f^{-1} [t, 1]\) is compact for every \(t \in (0, 1]\). It is then proved that a topological space \(X\) is completely regular if and only if for any functions \(f, g : X \to [0, 1]\) with \(f\) compact-like, \(g\) lower semicontinuous, and \(f \leq g\), there is a continuous function \(h : X \to [0, 1]\) such that \(f \leq h \leq g\). Naturally, then, one may ask if such an insertion-type characterisation holds for locales. The main theme of the paper addresses this question. A full answer is not known, but a partial one covering a large class of locales is available. By first characterising regular and completely regular spaces in terms of compact sublocales (of the spaces viewed as locales), they define what they call \(c\)-regular and completely \(c\)-regular locales. Every (completely) regular locale is (completely) \(c\)-regular. In fact, for a wide class of locales (including the spatial ones and the zero-dimensional ones) (complete) regularity is equivalent to (complete) \(c\)-regularity, but it is not known if this holds for all locales. The insertion theorem (after defining in a natural way upper and lower compact-like real functions on a locale) is then proved. It says that if \(L\) is a completely \(c\)-regular locale and \(f \leq g\), for some upper compact-like \(f\) and lower compact-like \(g\), then a continuous real function on \(L\) can be inserted between \(f\) and \(g\). The converse holds for locales in which compact sublocales are complemented. The accompanying extension theorem states that every closed sublocale of a completely \(c\)-regular locale is \(C\)-embedded.