A globalisation of the Gelfand duality theorem (Q2575765)

This is the culmination of a long sequence of papers by the two authors, presenting a constructive version of the Gelfand duality theorem which can be applied internally in an arbitrary topos. The key to constructivizing the theorem is to regard the maximal spectrum of a commutative \(C^*\)-algebra not as a space but as a locale: one shows that any such locale is compact and completely regular, that any compact completely regular locale is isomorphic to the maximal ideal locale of its algebra of continuous complex-valued functions, and that any commutative \(C^*\)-algebra is representable as the algebra of continuous functions on its maximal ideal locale. Whilst the ideas involved in this proof have all been known to experts, thanks to an unpublished preprint, for over 20 years, it is good to have all the details publicly available at last. The authors discuss the interpretation of their duality when the base topos is the topos of sheaves on a compact Hausdorff space, and when it is the topos of \(G\)-sets for a group \(G\). They also comment on the asymmetry inherent in their approach, in that the maximal ideal spaces have become `pointfree' but the \(C^*\)-algebras themselves are still `point-determined', and speculate on the possibility of a more symmetric treatment in which the \(C^*\)-algebras also become localic.