Isocompactness in the Category of Locales

We study isocompactness in Loc defined, exactly as in Top, by requiring that every countably compact closed sublocale be compact. This is a genuine extension of the same-named topological concept since every Boolean (or, even more emphatically, every paracompact) locale is isocompact. A slightly stronger variant is defined by decreeing that the closure of every complemented countably compact sublocale be compact. Dropping the adjective “complemented” yields a formally even stronger property, which we show to be preserved by finite products. Metrizable locales (or, more generally, perfectly normal locales) do not distinguish between the three variants of isocompactness. Each of the stronger variants of isocompactness travels across a proper map of locales, and in the opposite direction if the map is a surjection in Loc.