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 is in section 2 of

Revised on April 9, 2014 05:45:42 by Tim Porter (2.26.27.237)