Theorem. Closure of algebraic cpos under product [dt-004C]
If D and E are algebraic cpos, then so is their product construction D \times E.
Proof.
In the following proof, we show that \mathsf {K}(D) \times \mathsf {K}(E) is a basis for the product D \times E and thereby show via Theorem [dt-004B] that D \times E is algebraic if D and E are.
- \mathsf {K}(D) \times \mathsf {K}(E) \subseteq \mathsf {K}(D \times E): Let (x,y) \in \mathsf {K}(D) \times \mathsf {K}(E). To show that (x,y) is compact, let us assume that (x,y) \in \bigsqcup X where X \subseteq D \times E is directed. We must show that there exists some element e of X such that our (x,y) \sqsubseteq e. As (x,y) \in \bigsqcup X, by the definition of lub on products we can conclude that:
\begin {array}{lcl}
x & \sqsubseteq & \bigsqcup \pi _0[ X] \\
y & \sqsubseteq & \bigsqcup \pi _1[X]
\end {array}
Here we use the notation f[X] to indicate the image of a function on a set, i.e. \{ f(v) \mid v \in X \}.
Since x and y are both compact, there must exist x' \in \pi _0[ X] and y' \in \pi _1[ X] such that x \sqsubseteq x' and y \sqsubseteq y'. While it does not follow that (x', y') \in X, we know that there must exist a pair (a,b) \in X such that x' \sqsubseteq a and y' \sqsubseteq b as X is directed. Hence (a,b) can be our element e \in X that is approximated by (x,y), i.e. (x,y) \sqsubseteq (a,b). - \mathop {\downarrow }(x,y) is directed for all (x,y) \in D \times E: \begin {array}{lcl} \mathop {\downarrow }(x,y) &= & \{ (a,b) \in \mathsf {K}(D) \times \mathsf {K}(E) \mid (a,b) \sqsubseteq (x,y) \} \\ & = & \{ a \in \mathsf {K}(D) \mid a \sqsubseteq x \} \times \{ b \in \mathsf {K}(E) \mid b \sqsubseteq y \}\\ & = & \mathop {\downarrow }(x) \times \mathop {\downarrow }(y) \end {array} Because D and E are algebraic, \mathop {\downarrow }(x) and \mathop {\downarrow }(y) are directed. As directedness is closed under product, \mathop {\downarrow }(x,y) is directed too.
- (x,y) = \bigsqcup \mathop {\downarrow }(x,y) Starting from the right hand side: \begin {array}{lclr} \bigsqcup \mathop {\downarrow }(x,y) & = & \bigsqcup (\mathop {\downarrow }(x) \times \mathop {\downarrow }(y)) & \text {(part 2)}\\ & = & (\bigsqcup (\mathop {\downarrow }(x), \bigsqcup \mathop {\downarrow }(y))) & \text {(lub on products)}\\ & = & (x,y) & \text {($D$, $E$ are {algebraic})} \end {array}