I'm struggling with a claim in Example 6.2 from Steve Awodey's Category Theory (2nd Ed.). The context is the following: $P$ and $Q$ are $\omega$CPO's, $Q^P = \{ f: P \to Q \mid \text{ $f$ is monotone and $\omega$-continuous}\}$, and $\epsilon: Q^P \times P \to Q$ is defined by $\epsilon(f,p) = f(p)$. I want to prove that $\epsilon$ is $\omega$-continuous, meaning that $\epsilon$ preserves all $\omega$-colimits, i.e., $\epsilon\left(\varinjlim (d_n,e_n)\right) = \varinjlim \epsilon(d_n, e_n)$. Below is the part I was able to do.
Given an $\omega$-chain $DE: (d_0, e_0) \leq (d_1, e_1) \leq (d_2, e_2) \leq \dots$ in $Q^P \times P$, with colimit $L = (L_1, L_2)$, we want to prove that the colimit of the $\omega$-chain $\epsilon(DE): \epsilon(d_0, e_0) \leq \epsilon(d_1, e_1) \leq \epsilon(d_2, e_2) \leq \dots$ is $\epsilon(L)$. From the fact that $L$ is a colimit of $DE$, we have, immediately, that:
(i) $L$ is an upper bound for $DE$. That is, for all $n \in \mathbb{N}$, $(d_n, e_n) \leq (L_1, L_2)$, i.e., $d_n \leq L_1$ and $e_n \leq L_2$.
(ii) If $L' = (L_1', L_2') \in Q^P \times P$ is an upper bound for $DE$, then $L \leq L'$, i.e., $L_1 \leq L_1'$ and $L_2 \leq L_2'$, i.e., $L_2 \leq L_2'$ and, for all $p \in P$, $L_1(p) \leq L_1'(p)$.
Observe that
- $\epsilon(L)$ is an upper bound for $\epsilon(DE)$. That is, for all $n \in \mathbb{N}$, $d_n(e_n) = \epsilon(d_n, e_n) \leq \epsilon(L) = L_1(L_2)$. In fact, given $n \in \mathbb{N}$, we have, by (i), $e_n \leq L_2$. Since $d_n$ is monotone, it follows that $d_n(e_n) \leq d_n(L_2)$. But, by (i), $d_n \leq L_1$. So, $d_n(p) \leq L_1(p)$, for all $p \in P$. In particular, for $p = L_2$, we have $d_n(L_2) \leq L_1(L_2)$. Now, from $d_n(e_n) \leq d_n(L_2)$ and $d_n(L_2) \leq L_1(L_2)$, we obtain $d_n(e_n) \leq L_1(L_2)$, as intended.
- If $q \in Q$ is an upper bound for $\epsilon(DE)$, then $\epsilon(L) \leq q$. In fact, given $q \in Q$, with $d_n(e_n) \leq q$ for all $n \in \mathbb{N}$, ...
I just found an answer: Propositions 1.2.11-1.2.13 of Barendregt's The Lambda Calculus, Its Syntax and Semantics. Below is my version of the proof.
Proposition 1: $Q^P$ is an $\omega$CPO.
Proof: Given any $\omega$-chain $D: d_0 \leq d_1 \leq d_2 \leq \dots$ in $Q^P$, we need to prove that it has a colimit $d_{\omega}$. Observe that, for all $p \in P$, we have a $\omega$-chain $D(p): d_0(p) \leq d_1(p) \leq d_2(p) \leq \dots$, in $Q$, which has a colimit $d_{\omega}(p)$. The map $p \mapsto d_{\omega}(p) = \varinjlim_{n \in \mathbb{N}} d_n(p)$ defines an element $d_{\omega} \in Q^P$ such that
Thus, $d_{\omega}$ is the least upper bound for $D$. Since $D$ is an arbitrary $\omega$-chain in $Q^P$, we conclude that $Q^P$ is an $\omega$CPO. $\square$
Proposition 2: The evaluation map $\epsilon: Q^P \times P \to Q$ is $\omega$-continuous.
Proof: Given an $\omega$-chain $DE: (d_0, e_0) \leq (d_1, e_1) \leq (d_2, e_2) \leq \dots$ in $Q^P \times P$, with colimit $L = (L_1, L_2)$, we want to prove that the colimit of the $\omega$-chain $\epsilon(DE): \epsilon(d_0, e_0) \leq \epsilon(d_1, e_1) \leq \epsilon(d_2, e_2) \leq \dots$ is $\epsilon(L)$. From the fact that $L$ is a colimit of $DE$, we have, immediately, that:
(i) $L$ is an upper bound for $DE$. That is, for all $n \in \mathbb{N}$, $(d_n, e_n) \leq (L_1, L_2)$, i.e., $d_n \leq L_1$ and $e_n \leq L_2$.
(ii) If $L' = (L_1', L_2') \in Q^P \times P$ is an upper bound for $DE$, then $L \leq L'$, i.e., $L_1 \leq L_1'$ and $L_2 \leq L_2'$, i.e., $L_2 \leq L_2'$ and, for all $p \in P$, $L_1(p) \leq L_1'(p)$.
Furthermore,
(iii) $L_1 = \varinjlim_{n \in \mathbb{N}} d_n$. Proof: By (i), we have that $d_n \leq L_1$, for all $n \in \mathbb{N}$. Moreover, if $L_1'$ is an upper bound for $D$, then $(L_1', L_2)$ is an upper bound for $DE$, which implies, by (ii), that $L_1 \leq L_1'$.
(iv) $L_2 = \varinjlim_{n \in \mathbb{N}} e_n$. Proof: By (i), we have that $e_n \leq L_2$, for all $n \in \mathbb{N}$. Moreover, if $L_2'$ is an upper bound for $E$, then $(L_1, L_2')$ is an upper bound for $DE$, which implies, by (ii), that $L_2 \leq L_2'$.
Finally, observe that
$\epsilon(L)$ is an upper bound for $\epsilon(DE)$. That is, for all $n \in \mathbb{N}$, $\epsilon(d_n, e_n) \leq \epsilon(L)$. Equivalently, for all $n \in \mathbb{N}$, $d_n(e_n) \leq L_1(L_2)$. In fact, given $n \in \mathbb{N}$, we have, by (i), $e_n \leq L_2$. Since $d_n$ is monotone, it follows that $d_n(e_n) \leq d_n(L_2)$. But, by (i), $d_n \leq L_1$. So, $d_n(p) \leq L_1(p)$, for all $p \in P$. In particular, for $p = L_2$, we have $d_n(L_2) \leq L_1(L_2)$. Now, from $d_n(e_n) \leq d_n(L_2)$ and $d_n(L_2) \leq L_1(L_2)$, we obtain $d_n(e_n) \leq L_1(L_2)$, as intended.
If $q \in Q$ is an upper bound for $\epsilon(DE)$, then $\epsilon(L) \leq q$. In fact, given $q \in Q$, with $d_n(e_n) \leq q$ for all $n\in \mathbb{N}$, we have that, for all $i,j\in \mathbb{N}$, there is a $p = \max\{i,j\}$ such that $d_i(e_j) \leq d_i(e_p) \leq d_p(e_p) \leq q$. Thus, for all $i \in \mathbb{N}$, $q$ is an upper bound of the $\omega$-chain $D_iE: d_i(e_0) \leq d_i(e_1) \leq d_i(e_2) \leq \dots$. But, since $L_2 = \varinjlim_{j \in \mathbb{N}} e_j$ and each $d_i$, with $i \in \mathbb{N}$, is continuous, we have that, for all $i \in \mathbb{N}$, $d_i(L_2) = \varinjlim_{j \in \mathbb{N}} d_i(e_j)$ is the least upper bound for $D_iE$. Hence, $d_i(L_2) \leq q$, for all $i \in \mathbb{N}$. So, $q$ is an upper bound for the $\omega$-chain $D(L_2): d_0(L_2) \leq d_1(L_2) \leq d_2(L_2) \leq \dots $. Now, recall that $L_1 = \varinjlim_{i \in \mathbb{N}} d_i$ and, by Proposition 1, the colimit of any $\omega$-chain $d_0 \leq d_1 \leq d_2 \leq \dots$ in $Q^P$ is the function $d_\omega$ given by $d_{\omega}(p) = \varinjlim_{i \in \mathbb{N}} d_i(p)$, for all $p \in P$. Thus, $L_1(L_2) = d_\omega(L_2) = \varinjlim_{i \in \mathbb{N}} d_i(L_2)$. So, $L_1(L_2)$ is the least upper bound of the $\omega$-chain $D(L_2): d_0(L_2) \leq d_1(L_2) \leq d_2(L_2) \leq \dots$. On the other hand, we have seen that $q$ is an upper bound for $D(L_2)$. Therefore, $\epsilon(L) = L_1(L_2) \leq q$, as intended. $\square$