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

TL;DR

This paper introduces a constructive approach to pointfree topology that removes reliance on the axiom of choice in Riesz space theory, exemplified by proving almost f-algebras are commutative.

Contribution

It presents a general methodology using pointfree topology to avoid non-constructive representation theorems in Riesz space theory.

Findings

Almost f-algebras are commutative.

Proofs are simplified using pointfree Stone-Yosida theorem.

Methodology avoids non-constructive axioms.

Abstract

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.