Commutation of Smyth and Hoare Power Constructions in Well-filtered Dcpos
Huijun Hou, Qingguo Li
TL;DR
This work characterizes when the Hoare power construction and the Smyth power construction commute on the category of well-filtered dcpos. It proves that HQ(L) and QH(L) are isomorphic precisely when L satisfies the KC property and the Scott topology on Q(L) matches the upper Vietoris topology, establishing a deep link between order-theoretic and hyperspace topologies. The paper extends both constructions to monads on WF and analyzes the composite monad QH, showing its Eilenberg–Moore algebras form a subcategory of frames, with HQ and QH coinciding in core-compact locally compact sober cases. It also situates these results within the Beck distributive-law framework, clarifying the algebraic structure underlying nondeterministic semantics in well-filtered dcpos and highlighting open questions for extending the equivalence beyond core-compact settings.
Abstract
Prior work [11] established a commutativity result for the Hoare power construction and a modified version of the Smyth power construction consisting of strongly compact sets, which is defined for Us-admitting dcpos, where Us-admissability is well-filteredness with compact sets replaced by strongly compact sets. In this paper, we consider the Hoare power construction H and the Smyth power construction Q on the category WF of well-filtered dcpos with Scott-continuous maps. Actually, the functors H and Q can be extended to monads. We prove that H and Q commute, that is, HQ(L) is isomorphic to QH(L) for a well-filtered dcpo L, if and only if L satisfies a property similar to consonance that we call (KC) and the Scott topology coincides with the upper Vietoris topology on Q(L). We also investigate the Eilenberg-Moore category of the monad composed by H and Q under a distributive law on WF and characterize it to be a subcategory of the category Frm, which is composed of all frames and all frame homomorphisms.