Predicative theories of continuous lattices

TL;DR

This paper develops a predicative framework for continuous lattices using strong proximity join-semilattices, characterising them via coalgebras and entailment relations, thus clarifying their logical and topological foundations.

Contribution

It introduces strong proximity join-semilattices as a predicative model of continuous lattices, linking coalgebraic and logical characterisations within point-free topology.

Findings

Characterisation of strong proximity join-semilattices via coalgebras of the lower powerlocale

Logical presentation of these structures as strong continuous finitary covers

Explicit connection between predicative structures and continuous lattices in point-free topology

Abstract

We introduce a notion of strong proximity join-semilattice, a predicative notion of continuous lattice which arises as the Karoubi envelop of the category of algebraic lattices. Strong proximity join-semilattices can be characterised by the coalgebras of the lower powerlocale on the wider category of proximity posets (also known as abstract bases or R-structures). Moreover, locally compact locales can be characterised in terms of strong proximity join-semilattices by the coalgebras of the double powerlocale on the category of proximity posets. We also provide more logical characterisation of a strong proximity join-semilattice, called a strong continuous finitary cover, which uses an entailment relation to present the underlying join-semilattice. We show that this structure naturally corresponds to the notion of continuous lattice in the predicative point-free topology. Our result makes the predicative and finitary aspect of the notion of continuous lattice in point-free topology more explicit.