Closure operators on dcpos

TL;DR

This paper explores the properties of closure operators on dcpos, establishing their lattice structure, proving Tarski's theorem constructively, and applying these concepts to convex geometries and special posets.

Contribution

It provides a comprehensive analysis of closure operators on dcpos, including lattice completeness, constructive proofs of key theorems, and applications to convex geometries.

Findings

The poset of closure operators on a dcpo forms a complete lattice.

Constructive proof of Tarski's theorem for dcpos.

Identification of convex geometries related to closure operators.

Abstract

We examine collective properties of closure operators on posets that are at least dcpos. The first theorem sets the tone of the paper: it tells how a set of preclosure maps on a dcpo determines the least closure operator above it, and pronounces the related induction principle, and its sibling, the obverse induction principle. Using this theorem we prove that the poset of closure operators on a dcpo is a complete lattice, and then provide a constructive proof of the Tarski's theorem for dcpos. We go on to construct the joins in the complete lattice of Scott-continuous closure operators on a dcpo, and to prove that the complete lattice of nuclei on a preframe is a frame, giving some constructions in the special case of the frame of all nuclei on a frame. In the rather drawn-out proof if the Hofmann-Mislove-Johnstone theorem we show off the utility of the obverse induction, applying it in the proof of the crucial lemma. After that we shift a viewpoint and prove some results, analogous to the results about dcpos, for posets in which certain special subposets have enough maximal elements; these results actually specialize to dcpos, but at the price of using the axiom of choice. We conclude by pointing out two convex geometries associated with closure operators on a dcpo.