A uniform view of localic realcompactness (Q1818627)

Classically, a space \(X\) is usually defined to be realcompact if every homomorphism \(C(X)\to{\mathbb R}\), where \(C(X)\) is the \(\mathbb R\)-algebra of continuous real-valued functions on \(X\), is given by evaluation at a (unique) point of \(X\). It is well known that this is equivalent to saying that \(X\) is embeddable as a closed subspace of a power of \(\mathbb R\), and also to the condition that, for any space \(Y\), each homomorphism \(C(X)\to C(Y)\) is induced by a unique continuous map \(Y\to X\). The first investigation of realcompactness for locales was carried out by G. D.~Reynolds in 1979 (he actually worked with toposes rather than locales, but the difference is immaterial in the present context): he showed that the second and third conditions above, when suitably reworded for locales, are still equivalent, but (because of the existence of non-spatial locales) the third condition is not equivalent to the special case of itself when \(Y\) is the one-point space, which is traditionally taken as the definition. Subsequently, J.~Madden and J.~Vermeer showed that Reynolds' definition is equivalent to the Lindelöf property for regular locales; thus it is not a `conservative extension' of realcompactness for spaces. In the present paper, the author uses techniques from the study of uniform locales to investigate the difference between Reynolds' condition, which he calls `strong realcompactness', and `mere' realcompactness which he defines by the direct localic translation of the first definition above. In particular, he shows that a completely regular locale is realcompact in the weaker sense iff it is complete in its real uniformity. He also analyses the use of choice principles in the work of Reynolds and of Madden-Vermeer, and shows that some of their results are in fact provable in ZF set theory without choice.