Geometric theories of patch and Lawson topologies

TL;DR

This paper provides geometric characterizations of patch and Lawson topologies within predicative point-free topology, using geometric theories and located subsets to describe their models and relationships.

Contribution

It introduces geometric theories for patch and Lawson topologies, connecting them with predicative notions and monads, and offers a new presentation of perfect nuclei.

Findings

Geometric characterizations of patch and Lawson topologies.

Models correspond to located points and subsets.

Lawson monad is isomorphic to the Vietoris monad.

Abstract

We give geometric characterisations of patch and Lawson topologies in the context of predicative point-free topology using the constructive notion of located subset. We present the patch topology of a stably locally compact formal topology by a geometric theory whose models are the points of the given topology that are located, and the Lawson topology of a continuous lattice by a geometric theory whose models are the located subsets of the given lattice. We also give a predicative presentation of the frame of perfect nuclei on a stably locally compact formal topology, and show that it is essentially the same as our geometric presentation of the patch topology. Moreover, the construction of Lawson topologies naturally induces a monad on the category of compact regular formal topologies, which is shown to be isomorphic to the Vietoris monad.