2021-06-27: The image of a DCPO need not be a DCPO           rak
================================================================

It's common for the image of a given mathematical object with
structure to again have that structure. For example, given two
groups G and H and a group homomorphism f : G -> H, the image
f(G) of f in H is again a group. For some objects and associated
morphisms, this is not true.

Today, I again [0] found myself wondering if continuous
functions preserve the structure of a dcpo. It turns out that:

Proposition: The continuous image of a dcpo need not be a dcpo.

Proof. Let D be the dcpo {0, 1, 2, ...} where x <= y if and only
if x = y. Let P be the poset {0 <= 1 <= 2 <= ...} where natural
numbers are ordered in the usual way. Let f : D -> P be the
obvious inclusion of D in P: f(x) = x. It is continuous: the
only directed sets in D are singleton sets, and f clearly
preserves their directed suprema. The image of f is all of P.
P is directed, but it does not have a directed supremum. Q.E.D.

This reminds me of an exercise in Emily Riehl's excellent book
"Category Theory in Context":

Exercise 1.3.iii. Find an example to show that the objects and
morphisms in the image of a functor F : C -> D do not
necessarily define a subcategory of D.

[0] I wrote a draft of this phlog post on 2020-02-27, but never
got around to publishing it. But my current research reminded me
of this property, so I decided to finish it and publish it.