Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems

TL;DR

This paper provides a constructive, formal topology-based proof of key representation theorems in functional analysis, including the Stone-Yosida, Gelfand, and related theorems, simplifying and clarifying their proofs.

Contribution

It introduces a shorter, clearer constructive proof of the Stone-Yosida theorem using formal topology, avoiding approximate eigenvalues, and derives related theorems for f-algebras and C*-algebras.

Findings

Constructive proof of Stone-Yosida theorem using formal topology

Derivation of Gelfand representation theorem for C*-algebras

Simplification of proofs by avoiding approximate eigenvalues

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.