nLab
constructive Gelfand duality theorem

Context

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

Last revised on June 3, 2017 at 05:11:04. See the history of this page for a list of all contributions to it.