Convergence in Formal Topology: a unifying notion

TL;DR

This paper introduces a unified, abstract notion of convergence in formal topology, enabling a uniform, predicative approach to generating various structures like locales, quantales, and suplattices, and clarifies their categorical properties.

Contribution

It proposes a general convergence concept that unifies existing definitions, leading to a predicative, inductive framework for formal covers, locales, and quantales, and refines key categorical theorems.

Findings

Unified convergence framework for formal topology structures

Predicative, inductive generation of locales, quantales, and suplattices

Categorical characterization of free structures and their relations

Abstract

Several variations on the definition of a Formal Topology exist in the literature. They differ on how they express convergence, the formal property corresponding to the fact that open subsets are closed under finite intersections. We introduce a general notion of convergence of which any previous definition is a special case. This leads to a predicative presentation and inductive generation of locales (formal covers), commutative quantales (convergent covers) and suplattices (basic covers) in a uniform way. Thanks to our abstract treatment of convergence, we are able to specify categorically the precise sense according to which our inductively generated structures are free, thus refining Johnstone's coverage theorem. We also obtain a natural and predicative version of a fundamental result by Joyal and Tierney: convergent covers (commutative quantales) correspond to commutative co-semigroups over the category of basic covers (suplattices).