Hostname: page-component-cd9895bd7-hc48f Total loading time: 0 Render date: 2024-12-26T16:36:55.540Z Has data issue: false hasContentIssue false
  • English
  • Français

Sublocales in formal topology

Published online by Cambridge University Press:  12 March 2014

Steven Vickers
Steven Vickers*
Affiliation:
School of Computer Science, The University of Birmingham, Birmingham, B15 2TT, UK, E-mail: [email protected], URL: http://www.cs.bham.ac.uk/~sjv
Get access Rights & Permissions [Opens in a new window]

Abstract

The paper studies how the localic notion of sublocale transfers to formal topology. For any formal topology (not necessarily with positivity predicate) we define a sublocale to be a cover relation that includes that of the formal topology. The family of sublocales has set-indexed joins. For each set of base elements there are corresponding open and closed sublocales, boolean complements of each other. They generate a boolean algebra amongst the sublocales. In the case of an inductively generated formal topology, the collection of inductively generated sublocales has coframe structure.

Overt sublocales and weakly closed sublocales are described, and related via a new notion of “rest closed” sublocale to the binary positivity predicate. Overt, weakly closed sublocales of an inductively generated formal topology are in bijection with “lower powerpoints”, arising from the impredicative theory of the lower powerlocale.

Compact sublocales and fitted sublocales are described. Compact fitted sublocales of an inductively generated formal topology are in bijection with “upper powerpoints”, arising from the impredicative theory of the upper powerlocale.

Keywords

formal topologylocalesublocaleinductively generatedopenclosedweakly closedcompactfittedpowerlocale
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 72 , Issue 2 , June 2007 , pp. 463 - 482
Copyright
Copyright © Association for Symbolic Logic 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Bunge, M. and Funk, J. [1996], Constructive theory of the lower powerlocale, Mathematical Structures in Computer Science, vol. 6, pp. 69–83.CrossRefGoogle Scholar
Coquand, T., Sambin, G., Smith, J., and Valentini, S. [2003], Inductively generated formal topologies, Annals of Pure and Applied Logic, vol. 124, pp. 71–106.CrossRefGoogle Scholar
Escardó, M. H. [2003], Joins in the frame of nuclei, Applied Categorical Structures, vol. 11, no. 2, pp. 117–124.CrossRefGoogle Scholar
Gambino, N. [2006], Heyting-valued interpretations for constructive set theory, Annals of Pure and Applied Logic, vol. 137, pp. 164–188.CrossRefGoogle Scholar
Johnstone, P.T. [1982], Stone spaces, Cambridge Studies in Advanced Mathematics, no. 3, Cambridge University Press.Google Scholar
Johnstone, P.T. [1985], Vietoris locales and localic semi-lattices, Continuous lattices and their applications (Hoffmann, R.-E., editor), Pure and Applied Mathematics, no. 101, Marcel Dekker, pp. 155–18.Google Scholar
Johnstone, P.T. [2002], Sketches of an elephant: A topos theory compendium, vol. 2, Oxford Logic Guides, no. 44, Oxford University Press.Google Scholar
Maietti, M. E. and Valentini, S. [2004], A structural investigation on formal topology: Corefiection of formal covers and exponentiability, this Journal, vol. 69, pp. 967–1005.Google Scholar
Negri, S. [2002], Continuous domains as formal spaces, Mathematical Structures in Computer Science, vol. 12, pp. 19–52.CrossRefGoogle Scholar
Sambin, G. [1987], Intuitionistic formal spaces – a first communication, Mathematical logic and its applications (Skordev, Dimiter G., editor), Plenum, pp. 187–204.CrossRefGoogle Scholar
Sambin, G. [2003], Some points in formal topology, Theoretical Computer Science, vol. 305, pp. 347–408.CrossRefGoogle Scholar
Valentini, S. [2005], The problem of the formalization of constructive topology, Archive for Mathematical Logic, vol. 44, pp. 115–129.CrossRefGoogle Scholar
Vickers, S. [1989], Topology via logic, Cambridge University Press.Google Scholar
Vickers, S. [1995], Locales are not pointless, Theory and formal methods of computing 1994 (Hankin, C.L., Mackie, I.C., and Nagarajan, R., editors), Imperial College Press, London, pp. 199–216.Google Scholar
Vickers, S. [1997], Constructive points of powerlocales, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 122, pp. 207–222.CrossRefGoogle Scholar
Vickers, S. [1999], Topical categories of domains, Mathematical Structures in Computer Science, vol. 9, pp. 569–616.CrossRefGoogle Scholar
Vickers, S. [2005], Some constructive roads to Tychonoff, From sets and types to topology and analysis: Towards practicable foundations for constructive mathematics (Crosilla, Laura and Schuster, Peter, editors), Oxford Logic Guides, vol. 48, Oxford University Press, pp. 223–238.CrossRefGoogle Scholar
Vickers, S. [2006], Compactness in locales and formal topology, Annals of Pure and Applied Logic, vol. 137, pp. 413–438.CrossRefGoogle Scholar