localic completion

Localic completion


If XX is a metric space, we can construct a version of its Cauchy completion as a locale, by taking as basic opens formal symbols B δ(x)B_\delta(x) representing open balls, and imposing relations ensuring that the points are Cauchy filters. (We can equivalently regard XX as a Lawvere metric space and build a locale whose points are “Cauchy profunctors”.) This is the localic completion of XX.

The construction can also be generalized in various ways.


Consider the collection of “formal balls” B(x,δ)B(x,\delta), where xXx\in X and δ +\delta\in\mathbb{Q}^+ (technically this is just another notation for the ordered pair (x,δ)X× +(x,\delta)\in X\times \mathbb{Q}^+). We say:

  • B(x,δ)B(y,ϵ)B(x,\delta)\le B(y,\epsilon) if d(x,y)+δϵd(x,y)+\delta\le\epsilon
  • B(x,δ)<B(y,ϵ)B(x,\delta)\lt B(y,\epsilon) if d(x,y)+δ<ϵd(x,y)+\delta\lt\epsilon

The localic completion of XX is the locale presented by generators B(x,δ)B(x,\delta) and relations:

  1. If B(x,δ)B(y,ϵ)B(x,\delta)\le B(y,\epsilon) (as above) then B(x,δ)B(y,ϵ)B(x,\delta)\le B(y,\epsilon) (in the locale)
  2. = xXB(x,ϵ)\top = \bigvee_{x\in X} B(x,\epsilon) for any ϵ\epsilon
  3. B(x,δ)B(y,ϵ)={B(z,η)B(z,η)B(x,δ) and B(z,η)B(y,ϵ)}B(x,\delta)\cap B(y,\epsilon) = \bigvee \{ B(z,\eta) \mid B(z,\eta) \le B(x,\delta) \text{ and } B(z,\eta) \le B(y,\epsilon) \}
  4. B(x,δ)={B(y,ϵ)B(y,ϵ)<B(x,δ)}B(x,\delta) = \bigvee \{ B(y,\epsilon) \mid B(y,\epsilon) \lt B(x,\delta) \}

Vickers combines conditions (3) and (4) into:

  • B(x,δ)B(y,ϵ)={B(z,η)B(z,η)<B(x,δ) and B(z,η)<B(y,ϵ)}B(x,\delta)\cap B(y,\epsilon) = \bigvee \{ B(z,\eta) \mid B(z,\eta) \lt B(x,\delta) \text{ and } B(z,\eta) \lt B(y,\epsilon) \}

On the other hand, condition (3) makes sense for any poset of generators replacing {B(x,δ)}\{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 XX is the classifying locale for Cauchy filters in XX that are additionally rounded (condition (4)).


  • When XX 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 XX to be a pseudometric space, a Lawvere metric space, or even a “metric locale?”. We can also allow XX 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, From intuitionistic to point-free topology (2005) U.U.D.M. Report 2005:47. link
  • Erik Palmgren, A constructive and functorial embedding of locally compact metric spaces into locales. Topology and its Applications, 154 (2007), 1854–1880.
  • 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.