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.


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?”. 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, A constructive and functorial embedding of locally compact metric spaces into locales

Revised on January 9, 2016 02:44:15 by Mike Shulman (