A convenient category of locales

TL;DR

The paper develops a point-free analogue of the category of compactly generated Hausdorff spaces by defining the category $\mathsf{kHLoc}$ of compactly generated strongly Hausdorff locales via a density comonad $T$ arising from the inclusion $\mathsf{KHLoc}\hookrightarrow\mathsf{HLoc}$. It proves the density comonad is idempotent and that $\mathsf{kHLoc}$ is the category of $T$-coalgebras, providing a coreflective, cartesian closed environment. By relating to Escardó's construction and employing Hofmann–Lawson duality, the work situates $\mathsf{kHLoc}$ as a robust, well-behaved locale-theoretic replacement for fiberwise topology. The main technical engine combines final functors, density comonads, and a key lemma ensuring the cartesian closed structure via carefully managed colimits and limits. This yields a powerful framework for working with fiberwise and point-free topologies in a cartesian closed setting.

Abstract

The notion of Kan extendable subcategories was initially introduced to define the category of compactly generated fibrewise topological spaces over a T1 base space and to establish its cartesian closure. In this paper, we show that the same framework can likewise be applied to define the category of compactly generated strongly Hausdorff locales and to prove that it, too, is cartesian closed

Theorems & Definitions (57)

• Definition 1.1
• Proposition 1.2
• Proposition 1.3
• Corollary 1.4
• Lemma 1.5
• Definition 1.6
• Theorem 1.7
• Proposition 2.1
• Definition 2.2
• Proposition 2.3