Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems
Functional Analysis
2008-08-21 v1 Logic
Abstract
We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.
Keywords
Cite
@article{arxiv.0808.2705,
title = {Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems},
author = {Thierry Coquand and Bas Spitters},
journal= {arXiv preprint arXiv:0808.2705},
year = {2008}
}
Comments
This is an expanded version of our paper [CS05a]. For the convenience of the reader we have included more details and added a few clarifications. There are no new results. We are grateful to Bob Lubarsky and Fred Richman for suggesting improvements in the presentation