nLab
constructive Gelfand duality theorem

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Idea

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

Examples

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 *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

Further disussion includes

Revised on June 3, 2017 05:11:04 by Urs Schreiber (178.6.236.87)