Definition. The $\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}

Context

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:

Definition. Projection 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}

Construction. Product 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 )

Theorem. Continuity of projection operations [dt-0022]

Liam O'Connor

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

Definition. The 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}

Theorem. Continuity 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):

Definition. The $\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}

Definition. Product 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.

Definition. Universal 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}$ :

Aside. Category theory [dt-002A]

Liam O'Connor

Definition. Category [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$ .

Example. The 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$ .

Example. The 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).

Example. The 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$ .

Definition. Functor [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}$ .

Example. The 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

to

B

and the two paths from

A

to

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

Corollary. Derived 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

Definition. Cpo 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.

Theorem. Commutative 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.

Definition. The 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.

Backlinks

Theorem. Commutative 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.