Searcharxiv⌕ Search

arXiv subjects

Bas Spitters

Publications and source records attributed to Bas Spitters.

41 records · Page 3Linked to original sources
arXiv2009

Locatedness and overt sublocales

Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected. Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact set is Bishop compact iff it is located. We translate this result to formal topology. `Bishop compact' is translated as compact and overt. We propose a definition of located predicate on subspaces in formal topology. We call a sublocale located if it can be presented by a formal topology with a located predicate. We prove that a closed sublocale of a compact regular locale has a located predicate iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact -- that is, totally bounded and complete -- iff its localic completion is compact overt. Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales. We work constructively, predicatively and avoid the use of the axiom of countable choice. Consequently, all our results are valid in any predicative topos.

math.LO↗
arXiv2008

Almost periodic functions, constructively

The almost periodic functions form a natural example of a non-separable normed space. As such, it has been a challenge for constructive mathematicians to find a natural treatment of them. Here we present a simple proof of Bohr's fundamental theorem for almost periodic functions which we then generalize to almost periodic functions on general topological groups.

cs.LO↗
arXiv2008

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

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.

math.FA↗
arXiv2008

Constructive pointfree topology eliminates non-constructive representation theorems from Riesz space theory

In Riesz space theory it is good practice to avoid representation theorems which depend on the axiom of choice. Here we present a general methodology to do this using pointfree topology. To illustrate the technique we show that almost f-algebras are commutative. The proof is obtained relatively straightforward from the proof by Buskes and van Rooij by using the pointfree Stone-Yosida representation theorem by Coquand and Spitters.

math.FA↗