Colimits in the category $\mathbf {Cpo}$ [dt-004P]

Definition $\omega$ -chains of cpos in the category $\mathbf {Cpo}$ [dt-004Q]

An $\omega$ -chain of cpos in the category $\mathbf {Cpo}$ consists of a family of cpos $\{A_i \mid i \in \mathbb {N} \}$ , together with a family of continuous functions $\{ f_i : A_i\twoheadrightarrow A_{i+1} \mid i \in \mathbb {N}\}$ , shown below:

A cpo $A$ is an upper bound of an $\omega$ -chain of cpos in the category $\mathbf {Cpo}$ if there is a family of continuous functions $\{g_i : A_i \twoheadrightarrow A \mid i \in \mathbb {N}\}$ such that the following diagram commutes (i.e. $g_i = g_{i+1} \circ f_i$ for all $i \in \mathbb {N}$ ):

A cpo $A$ is the least upper bound of an $\omega$ -chain of cpos if is both an upper bound and if there exists a unique $k$ for any other upper bound $B$ such that the following diagram commutes (i.e. $h_i = k \circ g_i$ for all $i \in \mathbb {N}$ ):

The least upper bound of such an $\omega$ -chain is also called its colimit.

Note: Uniqueness of lubs is up to isomorphism. That is, if $A$ and $B$ are both colimits of our $\omega$ -chain, then $A \simeq B$ .