×

A universal characterization of the double powerlocale. (English) Zbl 1047.06006

Summary: The double powerlocale \(\mathbb P(X)\) (found by composing, in either order, the upper and lower powerlocale constructions \(P_{\text U}\) and \(P_{\text L}\)) is shown to be isomorphic in \([\mathbf{Loc}^{\text{op}},\mathbf{Set}]\) to the double exponential \(\mathbb S^{\mathbb S^X}\) where \(\mathbb S\) is the Sierpiński locale. Further \(P_U(X)\) and \(P_L(X)\) are shown to be the subobjects of \(\mathbb P(X)\) comprising, respectively, the meet semilattice and join semilattice homomorphisms. A key lemma shows that, for any locales \(X\) and \(Y\), natural transformations from \(\mathbb S^X\) (the presheaf \(\mathbf{Loc}(\_ \times X, \mathbb S)\)) to \(\mathbb S^Y\) (i.e. \(\mathbf{Loc}(\_ \times Y, \mathbb S\))) are equivalent to dcpo morphisms (Scott continuous maps) from the frame \(\Omega X\) to \(\Omega Y\). It is also shown that \(\mathbb S^X\) has a localic reflection in \([\mathbf{Loc}^{\text{op}},\mathbf{Set}]\) whose frame is the Scott topology on \(\Omega X\). The reasoning is constructive in the sense of topos validity.

MSC:

06D22 Frames, locales
54B20 Hyperspaces in general topology
54C35 Function spaces in general topology
54B30 Categorical methods in general topology
03F55 Intuitionistic mathematics
06B35 Continuous lattices and posets, applications
18F20 Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects)
18B25 Topoi
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Abramsky, S.; Vickers, S. J., Quantales, observational logic and process semantics, Math. Structures Comput. Sci., 3, 161-227 (1993) · Zbl 0823.06011
[2] Carboni, A.; Rosolini, G., Locally cartesian closed exact completions, J. Pure Appl. Algebra, 154, 103-116 (2000) · Zbl 0962.18001
[3] M. Escardó, Topology of data types and computability concepts, submitted for publication, draft available on web at http://www.cs.bham.ac.uk/ mhe/papers/barbados.pdf; M. Escardó, Topology of data types and computability concepts, submitted for publication, draft available on web at http://www.cs.bham.ac.uk/ mhe/papers/barbados.pdf
[4] Flannery, K. E.; Martin, J. J., The Hoare and Smyth powerdomain constructions commute under composition, J. Comput. System Sci., 40, 125-135 (1990) · Zbl 0699.06008
[5] Fraser, G. A., The semilattice tensor product of distributive lattices, Trans. Amer. Math. Soc., 217, 183-194 (1976) · Zbl 0355.06013
[6] Hyland, J. M.E., Function spaces in the category of locales, (Banaschewski, B.; Hoffmann, R.-E., Continuous Lattices. Continuous Lattices, Lecture Notes in Mathematics, Vol. 871 (1981), Springer), 264-281 · Zbl 0483.54005
[7] Johnstone, P. T., Stone spaces, Cambridge Studies in Advanced Mathematics, Vol. 3 (1982), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0499.54001
[8] Johnstone, P. T., Vietoris locales and localic semi-lattices, (Hoffmann, R.-E., Continuous Lattices and their Applications. Continuous Lattices and their Applications, Pure and Applied Mathematics, Vol. 101 (1985), Marcel Dekker: Marcel Dekker New York), 15-18
[9] P.T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Vol. 2, Oxford Logic Guides, Vol. 44, Oxford University Press, Oxford, 2002.; P.T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Vol. 2, Oxford Logic Guides, Vol. 44, Oxford University Press, Oxford, 2002. · Zbl 1071.18002
[10] Johnstone, P. T.; Linton, F. E., Finiteness and decidability: II, Math. Proc. Cambridge Philos. Soc., 84, 207-218 (1978) · Zbl 0391.18004
[11] Johnstone, P. T.; Vickers, S. J., Preframe presentations present, (Carboni, A.; Pedicchio, M. C.; Rosolini, G., Category Theory—Proceedings, Como, 1990. Category Theory—Proceedings, Como, 1990, Lecture Notes in Mathematics, Vol. 1488 (1991), Springer: Springer Berlin), 193-212 · Zbl 0764.18004
[12] A. Joyal, M. Tierney, An Extension of the Galois Theory of Grothendieck, Memoirs of the American Mathematical Society, Vol. 309, American Mathematical Society, Providence, RI, 1984, pp. vii+71.; A. Joyal, M. Tierney, An Extension of the Galois Theory of Grothendieck, Memoirs of the American Mathematical Society, Vol. 309, American Mathematical Society, Providence, RI, 1984, pp. vii+71. · Zbl 0541.18002
[13] Markowsky, G., Categories of chain-complete posets, Theoret. Comput. Sci., 4, 125-135 (1977) · Zbl 0366.18003
[14] S.B. Nadler, Hyperspaces of Sets, Pure and Applied Mathematics Monographs, Vol. 49, Marcel Dekker, New York, 1978.; S.B. Nadler, Hyperspaces of Sets, Pure and Applied Mathematics Monographs, Vol. 49, Marcel Dekker, New York, 1978. · Zbl 0432.54007
[15] Plotkin, G. D., A powerdomain construction, SIAM J. Comput., 5, 452-487 (1976) · Zbl 0355.68015
[16] G.D. Plotkin, Postgraduate lecture notes in advanced domain theory, Technical Report, Department of Computing Science, University of Edinburgh, 1981.; G.D. Plotkin, Postgraduate lecture notes in advanced domain theory, Technical Report, Department of Computing Science, University of Edinburgh, 1981.
[17] E. Robinson, Power-domains, modalities and the Vietoris monad, Technical Report 98, Computer Laboratory, University of Cambridge, 1986.; E. Robinson, Power-domains, modalities and the Vietoris monad, Technical Report 98, Computer Laboratory, University of Cambridge, 1986.
[18] A. Schalk, Algebras for generalized power constructions, Ph.D Thesis, Technische Hochschule Darmstadt, 1993.; A. Schalk, Algebras for generalized power constructions, Ph.D Thesis, Technische Hochschule Darmstadt, 1993. · Zbl 0900.68275
[19] Smyth, M., Power domains, J. Comput. System Sci., 16, 23-36 (1978) · Zbl 0391.68011
[20] Taylor, P., Sober spaces and continuations, Theory Appl. Categories, 10, 248-299 (2002) · Zbl 1007.03058
[21] C.F. Townsend, Preframe techniques in constructive locale theory, Ph.D Thesis, Department of Computing, Imperial College, London, 1996.; C.F. Townsend, Preframe techniques in constructive locale theory, Ph.D Thesis, Department of Computing, Imperial College, London, 1996.
[22] Vickers, S. J., Topology via Logic (1989), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0668.54001
[23] Vickers, S. J., Information systems for continuous posets, Theoret. Comput. Sci., 114, 201-229 (1993) · Zbl 0779.06006
[24] S.J. Vickers, Locales are not pointless, in: C.L. Hankin, I.C. Mackie, P.R. Nagarajan (Eds.), Theory and Formal Methods of Computing 1994, Imperial College Press, London, 1995, pp. 199-216.; S.J. Vickers, Locales are not pointless, in: C.L. Hankin, I.C. Mackie, P.R. Nagarajan (Eds.), Theory and Formal Methods of Computing 1994, Imperial College Press, London, 1995, pp. 199-216. · Zbl 0846.18003
[25] Vickers, S. J., Constructive points of powerlocales, Math. Proc. Cambridge Philos. Soc., 122, 207-222 (1997) · Zbl 0879.54008
[26] Vickers, S. J., Topical categories of domains, Math. Structures Comput. Sci., 9, 569-616 (1999) · Zbl 0946.18001
[27] S.J. Vickers, The double powerlocale and exponentiation: a case study in geometric reasoning, submitted for publication, draft available on web at http://www.cs.bham.ac.uk/ sjv; S.J. Vickers, The double powerlocale and exponentiation: a case study in geometric reasoning, submitted for publication, draft available on web at http://www.cs.bham.ac.uk/ sjv
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.