Localic Metric spaces and the localic Gelfand duality

TL;DR

This paper extends the constructive Gelfand duality to a duality between compact regular locales and unital abelian localic C*-algebras, developing a theory of localic metric and Banach spaces.

Contribution

It introduces a constructive framework for localic metric and Banach spaces and proves a duality extending Gelfand duality into the localic setting.

Findings

Constructive theory of localic metric spaces developed

Extension of Gelfand duality to localic C*-algebras proved

Analysis of localic completion and pull-back behavior conducted

Abstract

In this paper we prove, as conjectured by B.Banachewski and C.J.Mulvey, that the constructive Gelfand duality can be extended into a duality between compact regular locales and unital abelian localic C*-algebras. In order to do so we develop a constructive theory of localic metric spaces and localic Banach spaces, we study the notion of localic completion of such objects and the behaviour of these constructions with respect to pull-back along geometric morphisms.