$\sigma$-locales in Formal Topology

TL;DR

This paper demonstrates that $\sigma$-locales can be understood within Formal Topology, showing their relation to Lindelöf elements and providing a constructive characterization of dense sublocales, all under countable choice.

Contribution

It establishes a connection between $\sigma$-locales and Formal Topology, and characterizes dense sublocales constructively, extending the theory of point-free topology.

Findings

$\sigma$-locales are representable as Lindelöf elements in formal topologies.

Constructive characterization of the smallest dense $\sigma$-sublocale.

Development relies on the axiom of countable choice.

Abstract

A $\sigma$-frame is a poset with countable joins and finite meets in which binary meets distribute over countable joins. The aim of this paper is to show that $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch of Formal Topology, that is, intuitionistic and predicative point-free topology. Every $\sigma$-frame $L$ is the lattice of Lindel\"of elements (those for which each of their covers admits a countable subcover) of a formal topology of a specific kind which, in its turn, is a presentation of the free frame over $L$. We then give a constructive characterization of the smallest (strongly) dense $\sigma$-sublocale of a given $\sigma$-locale, thus providing a "$\sigma$-version" of a Boolean locale. Our development depends on the axiom of countable choice.