🚀 go-pugleaf

Date: Wed, 5 Aug 92 14:30:01 +0100

This is a short note giving a characterization of the regular
subobjects in the category CCCPO (3CPO) which has:

   objects: consistently complete cpos.
   morphisms: functions preserving bottom and consistent join.

Note that the morphisms are NOT arbitrary continuous functions, 
but strict ones which in addition preserve the consistent join. 

Proposition. e : A --> B is a regular monic in CCCPO iff:
1. A is a subset of B (up to isomorphism).
2. bottom is in A.
3. if X is a subset of A and is consistent in B then \/X is in A.

Proof.

=> Let f, g: B -> C form an equalizer for e : A -> B.  Then:

   1. A is isomorphic to { b in B | f(b) = g(b) }.
   2. f bottom = bottom = g bottom, so bottom is in A.
   3. Since X is a subset of A, f[X] = g[X], so
      f(\/X) = \/f[X] = \/g[X] = g(\/X), so \/X is in A.

<= Define:

      a(b) = \/{ a in A | a <= b }
      f(b) = (b,b)
      g(b) = (b,a(b))
         C = { (b,b') in BxB | a(b) <= b' <= b }

   Note that a(b) is well-defined because of condition 3, is monotone, 
   and preserves bottom, but is not continuous.
  
   Then C is a cccpo with join given:

       \/X = (b_1, b_2 v a(b_1))  where  b_i = \/(pi_i[X])

   and f, g: B -> C form an equalizer.                             []

There is an obvious variant for domains without bottom. This allows us
to extend the characterization slightly to regular subobjects in the
category of cccpo's and continuous, non-empty consistent
join-preserving, but not necessarily strict maps.

We would be interested to know whether this, or any similar result, is
known in the community. Some features are quite suggestive. One is the
monadicity of CCCPO over POSET (suggested by Paul Taylor in
correspondence with us). Another is that we are looking a split
equalizer in POSET.

Alan Jeffrey
Edmund Robinson