Products [dt-002K]

Liam O'Connor

Recall Construction [dt-000E], which showed that the product of two pointed posets is itself a pointed poset. In Exercise [dt-001X] you may also have shown that $A \times B$ is also a cpo if $A$ and $B$ are cpos, with this definition for lubs: $\bigsqcup X \; = \; \left (\bigsqcup \{ x \mid \exists y.\ (x,y) \in X \}, \bigsqcup \{ y \mid \exists x.\ (x,y) \in X \}\right )$ This definition can be made a little more comprehensible by defining it in terms of the two projection operators for pairs:

DefinitionProjection operators for products [dt-0020]

Liam O'Connor

Destruction of pairs is captured by the two projection operators, defined as follows:

\begin {array}{lcl} \pi _0 : A \times B \rightarrow A & \qquad & \pi _1 : A \times B \rightarrow B \\ \pi _0(x, y) = x & & \pi _1(x, y) = y \\ \end {array}

ConstructionProduct of cpos [dt-0021]

Liam O'Connor

Given cpos $A$ and $B$ , the product $A \times B$ is itself a cpo, ordered by $(x,y) \sqsubseteq _{X \times Y} (x',y') \quad \text {iff} \quad x \sqsubseteq _X x' \land y \sqsubseteq _Y y'$ with bottom value $\bot _{X \times Y}$ being $(\bot _A, \bot _B)$ . Least upper bounds are found by taking the lubs of each component:

\bigsqcup X \; = \; \left (\bigsqcup \{ \pi _0(x) \mid x \in X \}, \bigsqcup \{ \pi _1(x) \mid x \in X \}\right )

TheoremContinuity of projection operations [dt-0022]

Liam O'Connor

The projection functions $\pi _0$ and $\pi _1$ are continuous.

DefinitionThe split function [dt-0023]

Liam O'Connor

Construction of pairs is captured by the split function: If

f : A \rightarrow B

and

g : B \rightarrow C

, then split, written

\langle f , g \rangle

, is defined as:

\begin {array}{lr} \langle f , g \rangle : A \rightarrow B \times C\\ \langle f , g \rangle \ a = (f(a), g(a)) \end {array}

TheoremContinuity of split [dt-0024]

Liam O'Connor

For continuous functions $f$ and $g$ , the split function $\langle f, g \rangle$ is continuous.

Proof.

Liam O'Connor

Using the alternative characterisation of continuity:

$\langle f, g \rangle$ is monotonic. Let $x \sqsubseteq y \in A$ . Then: $\begin {array}{lclr} \langle f , g \rangle \ x & = & (f(x), g(x)) & \text {(def)}\\ & \sqsubseteq & (f(y), g(y)) & \text {(monotonicity of $f$,$g$)}\\ & = & \langle f , g \rangle \ y & \text {(def)} \end {array}$
$\langle f , g \rangle$ preserves lubs of directed sets. Let $X \subseteq A$ be directed. Then:

\begin {array}{lclr} \langle f , g \rangle \ (\bigsqcup X) & = & (f(\bigsqcup X), g(\bigsqcup X)) & \text {(def)}\\ & = & (\bigsqcup \{ f(x) \mid x \in X \}, \bigsqcup \{ g(x) \mid x \in X \}) & \text {(continuity of $f$,$g$)}\\ & = & \bigsqcup \{ \langle f , g \rangle \ x \mid x \in X \} & \text {(def)} \end {array}

These building blocks can be used to make many functions on products (thereby ensuring continuity):

DefinitionThe $\mathit {swap}$ function [dt-0025]

Liam O'Connor

\begin {array}{l}\mathit {swap} : A \times B \rightarrow B \times A \\ \mathit {swap} = \langle \pi _1 , \pi _0 \rangle \end {array}

DefinitionProduct of functions [dt-0026]

Liam O'Connor

Given $f : A \rightarrow C$ and $g : B \rightarrow D$ , we overload the $\times$ operator for products to denote the combined function $f \times g : A \times B \rightarrow C \times D$ , given below:

$\begin {array}{l} f \times g : A \times B \rightarrow C \times D \\ f \times g = \langle f \circ \pi _0 , g \circ \pi _1 \rangle \end {array}$

Exercise [dt-002G]

Liam O'Connor

Express the function $\mathit {juggle} (a, (b,c)) = ((a,b),c)$ using just our primitive combinators for projection and split.

Solution.

Liam O'Connor

$\mathit {juggle} \triangleq \langle \langle \pi _0 , \pi _0 \circ \pi _1 \rangle , \pi _1 \circ \pi _1 \rangle$

Pictorial Properties [dt-0027]

Liam O'Connor

The following properties of our projection and split functions follow from the pictorial reasoning we see on the right:

$\pi _0 \circ \langle f , g \rangle = f$
$\pi _1 \circ \langle f , g \rangle = g$
$\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h$

Exercise [dt-0028]

Liam O'Connor

Prove that the three properties in § [dt-0027] are equivalent to the universal property for products

(\pi _0 \circ h = f \land \pi _1 \circ h = g)\ \text {iff}\ h = \langle f , g \rangle

Solution.

Liam O'Connor

Showing in both directions:

The three properties follow from the universal property: The first two properties follow from the universal property where $h$ is set to $\langle f , g \rangle$ . The third property follows from the universal property where $f$ is set to $\pi _0\circ h$ and $g$ is set to $\pi _1\circ h$ .
The universal property follows from the universal property: In the $\Rightarrow$ direction of the universal property follows from the third property, and the $\Leftarrow$ direction follows from the first two.

DefinitionUniversal property for cpo products [dt-0029]

Liam O'Connor

(\pi _0 \circ h = f \land \pi _1 \circ h = g)\ \text {iff}\ h = \langle f , g \rangle

As commuting diagram on the category $\mathbf {Cpo}$ :

AsideCategory theory [dt-002A]

Liam O'Connor

DefinitionCategory [dm-000G]

Liam O'Connor

A category $C$ consists of a collection of things (objects) and a collection of arrows between these things (morphisms). If there is a morphism $A \xrightarrow {f} B$ and a morphism $B \xrightarrow {g} C$ , we also have the composed morphism $A \xrightarrow {g \circ f} C$ . This composition operator must be associative. Additionally each object $X$ has an identity morphism $X \xrightarrow {\mathsf {id}_X} X$ , such that for an arrow $X \xrightarrow {a} Y$ , $a \circ \mathsf {id}_X = \mathsf {id}_Y \circ a = a$ .

ExampleThe category $\mathbf {Set}$ [dm-000H]

Liam O'Connor

The category $\mathbf {Set}$ is the category where the objects are (small) sets, the morphisms are functions between these sets, composition is function composition ( $(g \circ f)(x) \triangleq g(f(x))$ ) and identity is just the identity function $\lambda x. x$ .

ExampleThe category $\mathbf {Rel}$ [dm-000I]

Liam O'Connor

The category $\mathbf {Rel}$ is the category where the objects are (small) sets, the morphisms are relations between these sets, composition is relational composition: $g \circ f \triangleq \{ (a,b) \mid \exists i.\ (a,i) \in f \land (i,b) \in g \}$ and identity is the diagonal relation (equality).

ExampleThe category $\mathbf {Cpo}$ [dt-002B]

Liam O'Connor

The category $\mathbf {Cpo}$ is the category where the objects are cpos, the morphisms are continuous functions between these cpos, composition is function composition ( $(g \circ f)(x) \triangleq g(f(x))$ ) and identity is just the identity function $\lambda x. x$ .

DefinitionFunctor [dm-000J]

Liam O'Connor

A functor $F$ from a category $\mathbf {C}$ to a category $\mathbf {D}$ consists of an object mapping that maps objects of $\mathbf {C}$ to objects of $\mathbf {D}$ , and a morphism mapping that maps morphisms of $\mathbf {C}$ to morphisms of $\mathbf {D}$ such that:

For each $A \xrightarrow {m} B$ in $\mathbf {C}$ , we have a morphism $F(A) \xrightarrow {F(m)} F(B)$ in $\mathbf {D}$ .
For each object $A$ in $\mathbf {C}$ , the equation $F(\mathsf {id}_A) = \mathsf {id}_{F(A)}$ holds in $\mathbf {D}$ .
For a pair of morphism $A \xrightarrow {f} B \xrightarrow {g} C$ in $\mathbf {C}$ , the equation $F (g \circ f) = F(g) \circ F(f)$ holds in $\mathbf {D}$ .

ExampleThe category $\mathbf {Cat}$ [dm-000K]

Liam O'Connor

The category $\mathbf {Cat}$ is the category where the objects are themselves (small) categories, the morphisms are structure-preserving maps between these categories, i.e., functors.

Commutative diagrams [dm-000L]

Liam O'Connor

When working in a category, we can state many theorems compactly using commutative diagrams, such as this diagram for products:

In these diagrams, the objects are vertices in the diagram, and the morphisms are the arrows in the diagram (we typically omit identity morphisms and morphisms that are just compositions of other morphisms). Looking at the above diagram, we can equate the two paths from

A

B

and the two paths from

A

C

, and produce the equations

\pi _0 \circ \langle f, g \rangle = f

and

\pi _1 \circ \langle f, g \rangle = g

. We adopt the convention that dotted lines indicate uniqueness, meaning that, from the diagram above, we can also infer the law:

\pi _0 \circ h = f \land \pi _1 \circ h = g \implies h = \langle f , g \rangle

CorollaryDerived properties of cpo products [dt-002C]

Liam O'Connor

The universal property is called such because all the familiar properties of products follow from it – thinking in pictures helps to see how (Indeed, the universal property characterises products up to isomorphism):

$\pi _0 \circ (f \times g) = f \circ \pi _0$
$\pi _1 \circ (f \times g) = g \circ \pi _1$
$(f \times g) \circ \langle h , i \rangle = \langle f \circ h, g \circ i \rangle$
$\langle f , g \rangle \circ h = \langle f \circ h, g \circ h \rangle$
$\mathsf {id}_A \times \mathsf {id}_B = \mathsf {id}_{A \times B} \quad (*)$
$(f \circ g) \times (h \circ i) = (f \times h) \circ (g \times i) \quad (**)$

These last two statements $(*)$ and $(**)$ show that $\times$ is a bifunctor on the category $\textbf {Cpo}$ , i.e., a functor $\textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}$ .

Exercise [dt-002I]

Liam O'Connor

Show using the universal property that $\langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle$

Solution.

Liam O'Connor

Instantiating the universal property where

h := \langle f, g \rangle \circ h

f := f \circ h

, and

g := g \circ h

\pi _0 \circ \langle f, g \rangle \circ h = f \circ h \land \pi _1 \circ \langle f, g \rangle \circ h = g \circ h\ \text {iff}\ \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle

Simplifying using the pictorial properties in § [dt-0027] (shown equivalent to the universal property in Exercise [dt-0028]):

f \circ h = f \circ h \land g \circ h = g \circ h\ \text {iff}\ \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle

By logical simplifications, we arrive at

\langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle

as required.

Isomorphisms for cpo products [dt-002D]

Liam O'Connor

DefinitionCpo isomorphism [dt-002E]

Liam O'Connor

An isomorphism between two cpos $A$ and $B$ is a bijection $f$ between $A$ and $B$ such that $f$ preserves the cpo structure, i.e., that $f$ and $f^{-1}$ are continuous.

We say two cpos $A$ and $B$ are isomorphic, written $A \simeq B$ , iff an isomorphism exists between them.

TheoremCommutative monoid structure for cpos [dt-002H]

Liam O'Connor

Cpos form a commutative monoid "up to isomorphism" under $\times$ and $\mathbf {1}$ (the cpo consisting of only one element $\bot$ ). That is, for all cpos $A, B$ and $C$ :

$A \times \mathbf {1} \simeq A$
$A \times (B \times C) \simeq (A \times B) \times C$
$A \times B \simeq B \times A$

Proof.

Liam O'Connor

The isomorphisms required are the projection $\pi _0$ , the $\mathit {juggle}$ function from Exercise [dt-002G], and the swap function.

DefinitionThe set of continuous functions [dt-002F]

Liam O'Connor

Let $A \twoheadrightarrow B$ denote just the continuous functions from cpo $A$ to cpo $B$ : $A \twoheadrightarrow B\; \triangleq \; \{ f : A \rightarrow B \mid f\ \text {is continuous} \}$

Theorem [dt-002J]

Liam O'Connor

There is an isomorphism between pairs of continuous functions and continuous functions that output pairs: $(A \twoheadrightarrow B) \times (A \twoheadrightarrow C)\; \simeq \; (A \twoheadrightarrow (B \times C))$

Proof.

Liam O'Connor

Proof follows from the universal property after setting up the isomorphism with functions

f(g_0,g_1) = \langle g_0 , g_1 \rangle

and

f^{-1}(h) = (\pi _0 \circ h, \pi _1 \circ h)

Upshot.

Liam O'Connor

Because we have the functor $\times$ on $\textbf {Cpo}$ that satisfies the properties of products described above, the category $\textbf {Cpo}$ therefore has binary products.