Locatedness and overt sublocales

DOI10.1016/J.APAL.2010.07.002zbMATH Open1223.03053arXivmath/0703561OpenAlexW2165730173MaRDI QIDQ638474FDOQ638474

Authors: Bas Spitters 

Publication date: 12 September 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected. Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact set is Bishop compact iff it is located. We translate this result to formal topology. `Bishop compact' is translated as compact and overt. We propose a definition of located predicate on subspaces in formal topology. We call a sublocale located if it can be presented by a formal topology with a located predicate. We prove that a closed sublocale of a compact regular locale has a located predicate iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact -- that is, totally bounded and complete -- iff its localic completion is compact overt. Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales. We work constructively, predicatively and avoid the use of the axiom of countable choice. Consequently, all our results are valid in any predicative topos.

Full work available at URL: https://arxiv.org/abs/math/0703561

Recommendations

• Metric complements of overt closed sets
• A point-free characterisation of Bishop locally compact metric spaces
• Almost locatedness in uniform spaces
• Sublocales in formal topology
• Locating subsets of a normed space

zbMATH Keywords

constructive mathematicsformal topologyformal spacesBishop compact setconstructive locale theorylocatednessovert sublocalesVietoris locale

Mathematics Subject Classification ID

Frames, locales (06D22) Other constructive mathematics (03F65) Constructive and recursive analysis (03F60)

Cites Work

• Title not available (Why is that?)
• Sheaves in geometry and logic: a first introduction to topos theory
• An extension of the Galois theory of Grothendieck
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Intuitionism. An introduction
• Some points in formal topology.
• Title not available (Why is that?)
• Integrals and valuations
• Constructive points of powerlocales
• Sublocales in formal topology
• Title not available (Why is that?)
• Inductively generated formal topologies.
• Continuous domains as formal spaces
• Title not available (Why is that?)
• A constructive and functorial embedding of locally compact metric spaces into locales
• Constructivism in mathematics. An introduction. Volume II
• About Stone's notion of spectrum
• Compactification of Frames
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Aspects of general topology in constructive set theory
• On the collection of points of a formal space
• Title not available (Why is that?)
• Apartness, compactness and nearness
• Proper maps of locales
• Formal systems for some branches of intuitionistic analysis
• On the \(T_{1}\) axiom and other separation properties in constructive point-free and point-set topology
• The ``closed subgroup theorem for localic herds and pregroupoids
• Exact approximations to Stone-Čech compactification
• Open subspaces of locally compact metric spaces
• Generalized real numbers in constructive mathematics
• Remarks on the Stone-Čech and Alexandroff compactifications of locales
• Compactness in locales and in formal topology
• Adjoints and the image of the ball
• Locating subsets of a Hilbert space
• Localic completion of generalized metric spaces. II: Powerlocales
• Open sublocales of localic completions
• Metric complements of overt closed sets
• Almost locatedness in uniform spaces
• Geometric Intuition and Elementary Constructive Analysis
• Weak compactness in constructive spaces
• Locating subsets of a normed space
• Title not available (Why is that?)
• A constructive proof of the Heine-Borel covering theorem for formal reals
• Title not available (Why is that?)
• Located Operators
• Title not available (Why is that?)

Cited In (9)

• Title not available (Why is that?)
• Sublocales in formal topology
• Metric complements of overt closed sets
• Almost locatedness in uniform spaces
• Apartness, sharp elements, and the Scott topology of domains
• Structural, point-free, non-Hausdorff topological realization of Borel groupoid actions
• A point-free characterisation of Bishop locally compact metric spaces
• Converses of Bishop's lemma on located sets
• Sharp elements and apartness in domains

This page was built for publication: Locatedness and overt sublocales

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q638474)