<p>Here's an attempt (please check!).</p>

<p>We have that $\bot_D = d$, where</p>

<p>$$
d_i = \bigsqcup^{D_i} \{\bot_i,f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),\ldots\}
$$</p>

<p>By construction (and monotonicity), the above is the supremum of an $\omega$-chain inside $D_i$, so $d_i$ is well defined.</p>

<p>It is an element of $D$ since, by continuity,</p>

<p>$$
\begin{array}{ll}
&amp; f_i(d_{i+1}) \\
= &amp; f_i(\bigsqcup^{D_{i+1}} \{\bot_{i+1},f_{i+1}(\bot_{i+2}),f_{i+1}(f_{i+2}(\bot_{i+3})),\ldots\}) \\
= &amp; \bigsqcup^{D_{i}} \{f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\
= &amp; \bigsqcup^{D_{i}} \{\bot_i, f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\
= &amp; d_i
\end{array}
$$</p>

<p>To prove that $d$ is the bottom, we take any $x \in D$, and we observe</p>

<p>$$
\begin{array}{ll}
&amp; d_i \sqsubseteq x_i \\
\Leftarrow &amp; \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq x_i \\
\Leftarrow &amp; \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq f_i \circ \cdots \circ f_k (x_{k+1})\\
\Leftarrow &amp; \forall k\geq i.\ \bot_{k+1} \sqsubseteq x_{k+1}\\
\Leftarrow &amp; {\sf true}
\end{array}
$$</p>

CC BY-SA 3.0
2017-05-29T16:12:41.623Z
This proof checks out, and I found the same argument in Smyth-Plotkin's "The Category-Theoretic Solution to Recursive Domain Equations". The key step is that the set of images of _|_s is directed because the diagram is codirected, so the proof immediately generalizes. That's also why the proof doesn't generalize to equalizers, because you won't be able to take the join.
Max New
CC BY-SA 3.0
2017-05-29T16:04:06.597Z
2017-05-29T16:04:06.597Z
chi
<p>In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category of embedding-projection pairs has $\omega$-colimits. Specifically they say it is sufficient for the category to have $\omega^{op}$-limits.</p>

<p>They then have a theorem that the category of CPOs has all $\omega^{op}$ limits, but the proof is incomplete and I don't see how it could be completed.</p>

<p>To be clear in their book the category CPO has as objects directed complete partial orders with a least element and as maps continuous (not neccesarily strict!) functions.</p>

<p>Their proof proceeds as follows. Given a diagram ${D_n,f_n}_{n\in\omega}$ ($f_n : D_{n+1} \to D_n)$, their proposed limit is 
$$D = \{ \alpha : \Pi_{n\in\omega} D_n | \forall n, f_n(\alpha_{n+1}) = \alpha_{n} \}$$</p>

<p>with the pointwise ordering.
This is definitely the product of that diagram in DCPO, but I don't see why $D$ must have a least element. In particular, you can't pick $\alpha_n = \bot_n \in D_n$ since the functions $f_n$ are not assumed to be strict.</p>

<p>However, restricting to strict continuous functions is all they need anyway because embedding-projection pairs of CPOs are strict anyway (embedding because it's a left adjoint, projection because it's a retract of the embedding). However this doesn't seem quite right either because for example a right adjoint wouldn't necessarily have to be strict, so it seems less general.</p>

<p>So to summarize</p>

<ol>
<li>Is there a way to prove $D$ is a CPO or a concrete counterexample?</li>
<li>If it's not, what is the right way to "fix" to their formula for solving recursive domain equations? Specifically, we do want to limit the construction to a category of CPOs since they have the bottom elements needed for recursive domain equations, but restricting to limits of strict functions seems stronger than necessary (though sufficient for my needs for now).</li>
</ol>

<p>I know I could go back through Wand and Plotkin and Pitts and probably find the answers to (3) there, but it would be nice to have a succinct general construction like in their book chapter. Specifically I would like a reference that includes Pitt's minimal invariants work (otherwise Abramsky-Jung is probably sufficient).</p>

CC BY-SA 3.0
2017-05-27T18:49:11.240Z
Since the category has all products, you can simplify your question to: does it have equalizers? (I think not.) So then the question is whether $\omega^\mathrm{op}$-limits exist "by accident".
Andrej Bauer
CC BY-SA 3.0
2017-05-29T15:12:32.533Z
In Abramsky&Jung "Domain Theory", the DCPO category is proved complete (not just $\omega$-) in that way, but there a DCPO can have no bottom element.
chi
<ct.category-theory><domain-theory>
Does the Category of CPOs have omega^op limits?
Max New
# Does the Category of CPOs have omega^op limits?

(Asked by: username_0 on 2017-05-26)

In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category of embedding-projection pairs has $\omega$-colimits. Specifically they say it is sufficient for the category to have $\omega^{op}$-limits.

They then have a theorem that the category of CPOs has all $\omega^{op}$ limits, but the proof is incomplete and I don't see how it could be completed.

To be clear in their book the category CPO has as objects directed complete partial orders with a least element and as maps continuous (not neccesarily strict!) functions.

Their proof proceeds as follows. Given a diagram ${D\_n,f\_n}\_{n\in\omega}$ ($f\_n : D\_{n+1} \to D\_n)$, their proposed limit is
$$D = \{ \alpha : \Pi\_{n\in\omega} D\_n | \forall n, f\_n(\alpha\_{n+1}) = \alpha\_{n} \}$$

with the pointwise ordering.
This is definitely the product of that diagram in DCPO, but I don't see why $D$ must have a least element. In particular, you can't pick $\alpha\_n = \bot\_n \in D\_n$ since the functions $f\_n$ are not assumed to be strict.

However, restricting to strict continuous functions is all they need anyway because embedding-projection pairs of CPOs are strict anyway (embedding because it's a left adjoint, projection because it's a retract of the embedding). However this doesn't seem quite right either because for example a right adjoint wouldn't necessarily have to be strict, so it seems less general.

So to summarize

1. Is there a way to prove $D$ is a CPO or a concrete counterexample?
2. If it's not, what is the right way to "fix" to their formula for solving recursive domain equations? Specifically, we do want to limit the construction to a category of CPOs since they have the bottom elements needed for recursive domain equations, but restricting to limits of strict functions seems stronger than necessary (though sufficient for my needs for now).

I know I could go back through Wand and Plotkin and Pitts and probably find the answers to (3) there, but it would be nice to have a succinct general construction like in their book chapter. Specifically I would like a reference that includes Pitt's minimal invariants work (otherwise Abramsky-Jung is probably sufficient).

**Tags:** ct.category-theory, domain-theory
> **Comments:**
> **username_1**: Since the category has all products, you can simplify your question to: does it have equalizers? (I think not.) So then the question is whether $\omega^\mathrm{op}$-limits exist "by accident".  
> **username_2**: In Abramsky&Jung "Domain Theory", the DCPO category is proved complete (not just $\omega$-) in that way, but there a DCPO can have no bottom element.  

---

## 1 answers

### Answer by username_2 on 2017-05-29. Score: 7 | Accepted answer

Here's an attempt (please check!).

We have that $\bot\_D = d$, where

$$
d\_i = \bigsqcup^{D\_i} \{\bot\_i,f\_i(\bot\_{i+1}),f\_i(f\_{i+1}(\bot\_{i+2})),\ldots\}
$$

By construction (and monotonicity), the above is the supremum of an $\omega$-chain inside $D\_i$, so $d\_i$ is well defined.

It is an element of $D$ since, by continuity,

$$
\begin{array}{ll}
& f\_i(d\_{i+1}) \\
= & f\_i(\bigsqcup^{D\_{i+1}} \{\bot\_{i+1},f\_{i+1}(\bot\_{i+2}),f\_{i+1}(f\_{i+2}(\bot\_{i+3})),\ldots\}) \\
= & \bigsqcup^{D\_{i}} \{f\_i(\bot\_{i+1}),f\_i(f\_{i+1}(\bot\_{i+2})),f\_i(f\_{i+1}(f\_{i+2}(\bot\_{i+3}))),\ldots\} \\
= & \bigsqcup^{D\_{i}} \{\bot\_i, f\_i(\bot\_{i+1}),f\_i(f\_{i+1}(\bot\_{i+2})),f\_i(f\_{i+1}(f\_{i+2}(\bot\_{i+3}))),\ldots\} \\
= & d\_i
\end{array}
$$

To prove that $d$ is the bottom, we take any $x \in D$, and we observe

$$
\begin{array}{ll}
& d\_i \sqsubseteq x\_i \\
\Leftarrow & \forall k\geq i.\ f\_i \circ \cdots \circ f\_k(\bot\_{k+1}) \sqsubseteq x\_i \\
\Leftarrow & \forall k\geq i.\ f\_i \circ \cdots \circ f\_k(\bot\_{k+1}) \sqsubseteq f\_i \circ \cdots \circ f\_k (x\_{k+1})\\
\Leftarrow & \forall k\geq i.\ \bot\_{k+1} \sqsubseteq x\_{k+1}\\
\Leftarrow & {\sf true}
\end{array}
$$

> **Comments:**
> **username_0**: This proof checks out, and I found the same argument in Smyth-Plotkin's "The Category-Theoretic Solution to Recursive Domain Equations". The key step is that the set of images of _|_s is directed because the diagram is codirected, so the proof immediately generalizes. That's also why the proof doesn't generalize to equalizers, because you won't be able to take the join.  

---

