Presenting de Groot duality of stably compact spaces (Q2182316)

Stably compact spaces have a very rich theory which emulates in the wide class of \(T_0\) spaces as many properties as seem reasonable of classical compact \(T_2\) spaces. Any well-formed duality should be such that the double dual of \(X\) equals \(X\). This is exactly what happens with de Groot duality in the case of stably compact spaces. De Groot duality of stably compact spaces induces a family of dualities on various powerdomain constructions. In the point-free setting, \textit{S. Vickers} [Theor. Comput. Sci. 316, No. 1--3, 259--296 (2004; Zbl 1047.06007)] showed that the de Groot dual of the upper powerlocale of a stably compact locale is the lower powerlocale of its dual. In the point-set setting, \textit{J. Goubault-Larrecq} [Math. Struct. Comput. Sci. 20, No. 2, 169--237 (2010; Zbl 1193.06005)] showed that the dual of the Plotkin powerdomain of a stably compact space is the Plotkin powerdomain of its dual; the same holds for the probabilistic powerdomain. In this paper, the author gives a constructive account of the de Groot duality of stably compact spaces in the setting of strong proximity lattice, a point-free representation of a stably compact space, and shows that strong proximity lattices have a structural duality which reflects the de Groot duality of stably compact spaces in a simple way. The notion of strong continuous entailment relation is introduced, which can be thought of as a presentation of a strong proximity lattice by generators and relations. This new notion allows us to identify de Groot duals of stably compact spaces by analysing the duals of their presentations. A number of constructions on strong proximity lattices using strong continuous entailment relations and study their de Groot duals are carried out. The examples include various powerlocales, patch topology and the space of valuations. These examples illustrate the simplicity of constructive approach by which we can reason about the de Groot duality of stably compact spaces.