×

Generalised powerlocales via relation lifting. (English) Zbl 1268.54004

The Vietoris powerlocale originates, as the ‘Vietoris construction’, in Peter Johnstone’s book [P. T. Johnstone, Stone spaces. Cambridge etc.: Cambridge University Press (1982; Zbl 0499.54001)], in a restricted setting (specifically, compact regular locales), and in its full generality (for arbitrary locales) in [P. T. Johnstone, Lect. Notes Pure Appl. Math. 101, 155–180 (1985; Zbl 0581.54005)]. The Vietoris powerlocale is a constructive pointfree counterpart of the well known Vietoris hyperspace construction [L. Vietoris, Monatsh. f. Math. 32, 258–280 (1922; JFM 48.0205.02)].
In the present paper, making use of ideas from coalgebraic modal logic, the authors generalise Johnstone’s construction. As the authors mention in the introductory Section 1, “the main conceptual contribution of this paper is the introduction of a generalised powerlocale construction \(V_T\) that is parametric in a functor \(T: \mathrm{Set}\to\mathrm{Set}\) satisfying some categorical conditions. Given a frame \(L\), we define its \(T\)-powerlocale \(V_TL\) (...). As we will see, the classical Vietoris powerlocale construction is an instantiation of the \(T\)-powerlocale, where we take \(T=P_{\omega}\), the covariant finite power set functor”. This construction of the \(T\)-powerlocale makes explicit the connection between the Vietoris construction and Moss’s coalgebraic cover modality [L. S. Moss, Ann. Pure Appl. Logic 96, No. 1–3, 277–317 (1999); erratum ibid. 99, No. 1–3, 241–259 (1999; Zbl 0969.03026)].
The paper starts by giving, in Section 2, some background on category theory, relation lifting, frames and their presentations, and Vietoris powerlocales.
In the long Section 3, the authors introduce the general \(T\)-powerlocale construction on frames, make some technical observations about \(T\)-powerlocales, present two instantiations of the \(T\)-powerlocale construction (in particular the \(P_{\omega}\)-powerlocale, which is isomorphic to the classical Vietoris powerlocale), extend the \(T\)-powerlocale construction to an endofunctor \(V_T\) on the category of frames (and show how to lift natural transformations between set functors \(T, T'\) to natural transformations between powerlocale functors \(V_T, V_{T'}\)) and prove that the \(T\)-powerlocale construction admits a flat-site presentation (from which it follows as a corollary that each element of \(V_TL\) has a disjunctive normal form).
Then they show, in Section 4, that the \(T\)-powerlocale construction behaves well with respect to some properties of frames: it preserves regularity, zero-dimensionality and the combination of zero-dimensionality and compactness.
The final section of the paper enumerates some open problems and directions for future research.

MSC:

54B20 Hyperspaces in general topology
03F60 Constructive and recursive analysis
03G30 Categorical logic, topoi
06D22 Frames, locales
18B25 Topoi
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] DOI: 10.1007/978-3-540-73859-6_27 · Zbl 1214.03057 · doi:10.1007/978-3-540-73859-6_27
[2] DOI: 10.1016/S0304-3975(00)00056-6 · Zbl 0951.68038 · doi:10.1016/S0304-3975(00)00056-6
[3] Categories for the working mathematician (1998) · Zbl 0906.18001
[4] Pure and Applied Mathematics 101 pp 155– (1985)
[5] Advances in Modal Logic 7, Nancy 2008 pp 193– (2008)
[6] Stone Spaces (1982) · Zbl 0499.54001
[7] DOI: 10.1007/3-540-60246-1_160 · Zbl 1193.68163 · doi:10.1007/3-540-60246-1_160
[8] DOI: 10.1007/978-3-642-03741-2_7 · Zbl 1239.68048 · doi:10.1007/978-3-642-03741-2_7
[9] DOI: 10.1006/inco.1998.2725 · Zbl 0941.18006 · doi:10.1006/inco.1998.2725
[10] DOI: 10.1016/j.entcs.2008.10.013 · Zbl 1286.68300 · doi:10.1016/j.entcs.2008.10.013
[11] Springer-Verlag Lecture Notes in Mathematics 1488 pp 193– (1991) · doi:10.1007/BFb0084221
[12] Advances in Modal Logic 7, Nancy 2008 pp 1– (2008)
[14] Automata and Algebras in Categories (1990) · Zbl 0698.18001
[16] DOI: 10.1007/BF01696886 · JFM 48.0205.02 · doi:10.1007/BF01696886
[17] DOI: 10.1016/j.tcs.2004.01.034 · Zbl 1047.06006 · doi:10.1016/j.tcs.2004.01.034
[18] DOI: 10.1016/j.apal.2005.05.028 · Zbl 1077.03041 · doi:10.1016/j.apal.2005.05.028
[19] DOI: 10.1017/S0305004196001636 · Zbl 0879.54008 · doi:10.1017/S0305004196001636
[20] Topology via logic (1989) · Zbl 0668.54001
[21] DOI: 10.1016/j.ic.2005.06.003 · Zbl 1110.68066 · doi:10.1016/j.ic.2005.06.003
[22] DOI: 10.1007/3-540-08442-8_101 · doi:10.1007/3-540-08442-8_101
[23] DOI: 10.1016/0022-4049(72)90019-9 · Zbl 0241.18003 · doi:10.1016/0022-4049(72)90019-9
[24] DOI: 10.1016/S0168-0072(98)00042-6 · Zbl 0969.03026 · doi:10.1016/S0168-0072(98)00042-6
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.