Extension by continuity in pointfree topology (Q1840750)

A common problem in topology is that of constructing a continuous extension \(\overline{f}: Z\to Y\) of a given continuous map \(f: X\to Y\) where \(X\) is a dense subspace of \(Z\). A well-known theorem due to Bourbaki establishes a criterion, in regular spaces, for the existence and uniqueness of such an extension in terms of the convergence of certain filters. In `pointfree' topology one still has a good notion of convergence for filters, due to the second author of this paper (a filter in a frame \(L\) is convergent iff it meets every cover of \(L\)); but for regular frames this condition is equivalent to containing the neighbourhood filter of a point, and hence it is easily shown to be inadequate to prove the corresponding theorem on extensions. In the present paper, the authors introduce a stronger notion of `preservation of covers', appropriate to the situation where one has a continuous map defined on a dense sublocale, and show that this suffices to prove the analogue of Bourbaki's extension theorem. The resulting theorem is very close in spirit to (the regular case of) the result commonly known as `Joyal's lemma', and indeed the latter occurs as a special case of it, as do several known reflection theorems in locale theory.