If $X$ is a metric space, we can construct a version of its Cauchy completion as a locale, by taking as basic opens formal symbols $B_\delta(x)$ representing open balls, and imposing relations ensuring that the points are Cauchy filters. (We can equivalently regard $X$ as a Lawvere metric space and build a locale whose points are “Cauchy profunctors”.) This is the localic completion of $X$.
The construction can also be generalized in various ways.
Consider the collection of “formal balls” $B(x,\delta)$, where $x\in X$ and $\delta\in\mathbb{Q}^+$ (technically this is just another notation for the ordered pair $(x,\delta)\in X\times \mathbb{Q}^+$). We say:
The localic completion of $X$ is the locale presented by generators $B(x,\delta)$ and relations:
Vickers combines conditions (3) and (4) into:
On the other hand, condition (3) makes sense for any poset of generators replacing $\{B(x,\delta)\}$, and simply says that we regard the generators as a base rather than a subbase. Since the elements of a formal topology automatically form a base, Palmgren (who works with formal topologies) can omit condition (3).
When interpreted as a geometric theory, conditions (1)–(4) say that the localic completion of $X$ is the classifying locale for Cauchy filters in $X$ that are additionally rounded (condition (4)).
When $X$ is the rational numbers $\mathbb{Q}$, this yields the locale of real numbers, which is in many respects better-behaved constructively than either its space of points (the Dedekind real numbers) or the completion of $\mathbb{Q}$ by Cauchy sequences (the Cauchy real numbers). Thus, the localic completion provides a “good” notion of completion for arbitrary metric spaces which generalizes the good localic real numbers.
By localically completing $\mathbb{Q}$ under a different metric, we obtain a “locale of p-adic numbers”; see this MO question.
We can allow $X$ to be a pseudometric space, a Lawvere metric space, or even a “metric locale?”. We can also allow $X$ to be a certain sort of uniform space, with uniformity induced by a family of upper real number valued pseudometrics. See the references.
Steve Vickers, “Localic Completion Of Generalized Metric Spaces II: Powerlocales”, pdf
Simon Henry, Localic Metric spaces and the localic Gelfand duality, arXiv
Erik Palmgren, Continuity on the real line and in formal spaces. (2003). Revised version of U.U.D.M. Report 2003:32. link
Erik Palmgren, Resolution of the uniform lower bound problem in constructive analysis, link
Bas Spitters, Locatedness and overt sublocales, doi:10.1016/j.apal.2010.07.002 APAL
Thierry Coquand, Erik Palmgren, Bas Spitters, Metric complements of overt closed sets, Mathematical Logic Quarterly, 57(4), 373-378, 2011. link
Tatsuji Kawai, A point-free characterisation of Bishop locally compact metric spaces, link
Tatsuji Kawai. Localic completion of uniform spaces. Log. Methods Comput. Sci. 13 2017), no. 3, Paper No. 22, 39pp. arxiv
Last revised on January 5, 2018 at 16:38:37. See the history of this page for a list of all contributions to it.