# Localic completion of generalized metric spaces II: Powerlocales

That’s the paper that I have just had accepted, and you can find it on my web page. However, I won’t get far explaining it without also also explaining its predecessor “Localic completion of generalized metric spaces I”. In fact I’ll probably spend most of my time explaining what the titles mean.

“Localic completion”, roughly speaking, means describing the points of the completion of a metric space as the models of a logical theory – but the logic here is the so-called geometric logic. The logical theory then has the virtue of describing both the points and the topology all in one go. Such localic techniques have been used in denotational semantics since the 1980s and are particularly useful in constructive reasoning.

For the metric spaces (and these can be understood in a highly generalized sense that includes asymmetric metrics) the points of the completion come out as “Cauchy filters of formal balls”. Perhaps I’ll have time to illustrate this with the reals as completion of the rationals.

The powerlocale paper uses this localic approach for hyperspaces, i.e. spaces whose points are subspaces of some other space. Specifically, if X is the metric space then the hyperspaces of its completion can be described by completing the finite powerset of X, with appropriate metrics. Interestingly, the corresponding subspaces of the completion do not have to be finite.

I will also say something about the 10 years it took me to get the paper published.

(Sandwiches will be provided.)

This talk is part of the Lab Lunch series.