pith. sign in

arxiv: 2311.14261 · v5 · pith:6MOJF52Bnew · submitted 2023-11-24 · 🧮 math.CT

Commutation of Smyth and Hoare Power Constructions in Well-filtered Dcpos

Huijun Hou , Qingguo Li This is my paper

Pith reviewed 2026-05-24 06:39 UTC · model grok-4.3

classification 🧮 math.CT
keywords well-filtered dcposHoare power constructionSmyth power constructionpowerdomain commutativitymonads on dcposEilenberg-Moore algebrasframes
0
0 comments X

The pith

The Hoare and Smyth power constructions commute on a well-filtered dcpo precisely when the dcpo satisfies property (KC) and its Scott topology equals the upper Vietoris topology on the Smyth power construction.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper shows that the Hoare power construction H and Smyth power construction Q commute for well-filtered dcpos L, meaning HQ(L) is isomorphic to QH(L), exactly when L has the (KC) property and the Scott topology on Q(L) matches the upper Vietoris topology. The authors extend both constructions to monads on the category WF of well-filtered dcpos equipped with Scott-continuous maps. They further describe the Eilenberg-Moore category of the composite monad obtained via a distributive law as a subcategory of the category of frames.

Core claim

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.

What carries the argument

The Hoare power construction H and Smyth power construction Q, extended as monads on the category WF of well-filtered dcpos with Scott-continuous maps, with the (KC) property serving as the additional condition for their commutativity.

If this is right

  • HQ(L) is isomorphic to QH(L) exactly under the stated (KC) and topology conditions.
  • The composite monad obtained from H and Q via a distributive law has its Eilenberg-Moore category equal to a subcategory of Frm.
  • Commutativity holds on the full category WF rather than only on the narrower class of Us-admitting dcpos.
  • The result supplies a criterion for when combined powerdomain constructions preserve the structure of well-filtered dcpos.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The (KC) property may turn out to be equivalent to other known separation or consonance conditions in the literature on dcpos.
  • One could check whether common examples such as the Scott topology on algebraic domains automatically satisfy both required conditions.
  • If the topology coincidence holds more broadly, the result would allow direct transfer of algebraic properties between the two power constructions without additional checks.

Load-bearing premise

That the Hoare and Smyth constructions extend to monads on the category of well-filtered dcpos with Scott-continuous maps.

What would settle it

A concrete well-filtered dcpo L that satisfies (KC) yet has Scott topology strictly finer than the upper Vietoris topology on Q(L), yielding non-isomorphic HQ(L) and QH(L).

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript extends the Hoare power construction H and Smyth power construction Q to monads on the category WF of well-filtered dcpos. It proves that HQ(L) ≅ QH(L) for a well-filtered dcpo L if and only if L satisfies property (KC) (a consonance-like condition) and the Scott topology coincides with the upper Vietoris topology on Q(L). It further investigates the Eilenberg-Moore category of the composed monad under a distributive law and shows it is a subcategory of Frm.

Significance. If the central iff characterization holds, the result supplies a precise, checkable condition for commutation of these power constructions in the well-filtered setting, extending the earlier result for Us-admitting dcpos. The monad extensions and the explicit identification of the algebras with a subcategory of frames are concrete contributions to domain-theoretic powerdomain theory.

minor comments (3)
  1. [§1] §1 (Introduction): the precise definition of property (KC) and the statement of the topology-coincidence condition appear only later; moving a brief formulation to the introduction would improve readability.
  2. The proof that the functors extend to monads on WF is referenced to prior work [11] but the adaptation steps for well-filteredness (as opposed to Us-admissibility) are not summarized; a short paragraph outlining the changes would help.
  3. Notation: the symbols H, Q, and the composite monad are used before their formal definitions; a dedicated notation subsection or early table would reduce reader effort.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work and the recommendation of minor revision. The report does not list any specific major comments.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The derivation defines H and Q as functors on WF, extends them to monads, introduces property (KC) as an external condition on L, and proves the isomorphism HQ(L) ≅ QH(L) precisely when (KC) holds together with Scott = upper Vietoris on Q(L). No equation or step reduces by construction to a fitted input, self-definition, or self-citation chain; the cited [11] supplies only background definitions that the paper adapts explicitly, leaving the central iff claim independent and externally falsifiable via the stated topological and order-theoretic properties of L.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard definitions of well-filtered dcpos, the Hoare and Smyth power constructions, and the extension of these to monads on WF; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption Well-filtered dcpos with Scott-continuous maps form a category WF on which H and Q extend to monads.
    Stated directly in the abstract as the setting for the commutativity result.
  • domain assumption The property (KC) is well-defined and analogous to consonance.
    Invoked as the key condition in the iff statement.

pith-pipeline@v0.9.0 · 5723 in / 1388 out tokens · 23029 ms · 2026-05-24T06:39:25.123625+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    Borceux, Handbook of Categorical Algebra: Volume 2, Categories and Structures, En- cyclopedia of mathematics and its applications , Cambridge, Cambridge University Press, 1994

    F. Borceux, Handbook of Categorical Algebra: Volume 2, Categories and Structures, En- cyclopedia of mathematics and its applications , Cambridge, Cambridge University Press, 1994

    work page 1994

  2. [2]

    Beck, Distributive laws, In B

    J. Beck, Distributive laws, In B. Eckmann, editor, Seminar on triples and categorical homology theory, Springer, Berlin, Heidelberg, 1969: 119-140

    work page 1969

  3. [3]

    Y. Chen, H. Kou and Z. Lyu, Two topologies on the lattice of Scott closed subsets, Topology and its Applications , 306 (2022): 107918

    work page 2022

  4. [4]

    de Brecht, T

    M. de Brecht, T. Kawai, On the commutativity of the powerspace constructions, Logical Methods in Computer Science , 15 (2019): 13:1–13:25

    work page 2019

  5. [5]

    Dolecki, G

    S. Dolecki, G. H. Greco and A. Lechicki, When do the upper Kuratowski topology (home- omorphically, Scott topology) and the co-compact topology coincide? Transactions of the American Mathematical Society, 347 (1995): 2869-2884

    work page 1995

  6. [6]

    K. E. Flannery, J. J. Martin, The Hoare and Smyth power domain constructors commute under composition, Journal of Computer and System Sciences , 40 (1990): 125-135

    work page 1990

  7. [7]

    Fritz, P

    T. Fritz, P. Perrone and S. Rezagholi, Probability, valuations, hyperspace: Three monads on top and the support as a morphism, Mathematical Structures in Computer Science , 31 (2021): 850-897

    work page 2021

  8. [8]

    M. H. Escard´ o, Properly injective spaces and function spaces,Topology and its Applications, 89 (1998): 75-120

    work page 1998

  9. [9]

    Gierz, K

    G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, Continuous Lattices and Domains, Volume 93 of Encyclopedia of Mathematics and its Applications , Cambridge, Cambridge University Press, 2003

    work page 2003

  10. [10]

    Goubault-Larrecq, Non-Hausdorff Topology and Domain Theory, Volume 22 of New Mathematical Monographs, Cambridge, Cambridge University Press, 2013

    J. Goubault-Larrecq, Non-Hausdorff Topology and Domain Theory, Volume 22 of New Mathematical Monographs, Cambridge, Cambridge University Press, 2013

    work page 2013

  11. [11]

    R. Heckmann, An upper power domain construction in terms of strongly compact sets, In- ternational Conference on Mathematical Foundations of Programming Semantics , Springer, Berlin, Heidelberg, 1991: 272-293

    work page 1991

  12. [12]

    Heckmann, Lower and upper power domain constructions commute on all cpos, Infor- mation Processing Letters, 40 (1991): 7-11

    R. Heckmann, Lower and upper power domain constructions commute on all cpos, Infor- mation Processing Letters, 40 (1991): 7-11

    work page 1991

  13. [13]

    W. K. Ho, J. Goubault-Larrecq, A. Jung and X. Xi, The Ho-Zhao Problem, Logical Methods in Computer Science , 14 (2018): 139-144. 16

    work page 2018

  14. [14]

    H. Hou, H. Miao, Q. Li, The order-K-ification monads, Mathematical Structures in Computer Science, 34 (2024): 45-62

    work page 2024

  15. [15]

    X. Jia, A. Jung and Q. Li, A note on coherence of dcpos, Topology and its Applications, 209 (2016): 235-238

    work page 2016

  16. [16]

    Kock, Monads for which structures are adjoint to units, Journal of Pure and Applied Algebra, 104 (1995): 41-59

    A. Kock, Monads for which structures are adjoint to units, Journal of Pure and Applied Algebra, 104 (1995): 41-59

    work page 1995

  17. [17]

    Mac Lane, Categories for the Working Mathematician, Volume 5 of Graduate Texts in Mathematics, Springer, Berlin, 1998

    S. Mac Lane, Categories for the Working Mathematician, Volume 5 of Graduate Texts in Mathematics, Springer, Berlin, 1998

    work page 1998

  18. [18]

    Moggi, Notions of computation and monads, Information and Computation, 93(1) (1991): 55-92

    E. Moggi, Notions of computation and monads, Information and Computation, 93(1) (1991): 55-92

    work page 1991

  19. [19]

    G. D. Plotkin, A powerdomain construction, SIAM Journal on Computing , 5 (1976): 452- 487

    work page 1976

  20. [20]

    Schalk, Algebras for generalized power constructions, PhD Thesis, Technische Hochschule Darmstadt, 1993

    A. Schalk, Algebras for generalized power constructions, PhD Thesis, Technische Hochschule Darmstadt, 1993

    work page 1993

  21. [21]

    M. B. Smyth, Powerdomains, In International Symposium on Mathematical Foundations of Computer Science, Springer, Berlin, Heidelberg, (1976): 537-543

    work page 1976

  22. [22]

    Vickers, The double powerlocale and exponentiation: a case study in geometric logic, Theory and Applications of Categories , 12 (2004): 372-422

    S. Vickers, The double powerlocale and exponentiation: a case study in geometric logic, Theory and Applications of Categories , 12 (2004): 372-422

    work page 2004

  23. [23]

    X. Xi, J. Lawson, On well-filtered spaces and ordered sets, Topology and its Applications , 228 (2017): 139-144

    work page 2017

  24. [24]

    X. Xu, X. Wen and X. Xi, Scott topology on Smyth power posets, Mathematical Structures in Computer Science , 33 (2023): 832-867. 17

    work page 2023