nLab constructive Gelfand duality theorem

Idea

There is a statement and proof of Gelfand duality in constructive mathematics. This therefore makes sense in any topos.

Examples

• An application of constructive Gelfand duality in the presheaf topos over the semilattice of commutative subalgebras of a C-star algebra produces an internal locale from any noncommmutative $C^*$-algebra. See semilattice of commutative subalgebras.

References

A proof of Gelfand duality claimed to be constructive was given in.

• Bernhard Banaschewski; Christopher J. Mulvey, A globalisation of the Gelfand duality theorem Annals of Pure and Applied Logic, 137(1–3):62–103, 2006

This uses however Barr's theorem which requires itself non-constructive logic and requires the ambient topos to be a Grothendieck topos

A fully constructive proof is claimed in

• Thierry Coquand, Bas Spitters, Constructive Gelfand duality for $C^*$-algebras , Mathematical Proceedings of the Cambridge Philosophical society , Volume 147, Issue 02, September 2009, pp 323-337 (arXiv:0808.1518)

A review of some aspects of constructive Gelfand duality (with an eye towards Bohr toposes) is in

• Chris Heunen, Klaas Landsman, Bas Spitters, section 2 of A topos for algebraic quantum theory, Comm. Math. Phys. 291:63–110, 2009, free access doi, arXiv:0709.4364

Further disussion:

• Simon Henry: Constructive Gelfand duality for non-unital commutative $C^\ast$-algebras [arXiv:1412.2009]

• Simon Henry, Localic Metric spaces and the localic Gelfand duality [arXiv:1411.0898]