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:

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,δ)andB(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:

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)).



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.