Sums [dt-0030]

ConstructionSum of cpos [dt-0031]

The sum construct on cpo A + B denotes a disjoint union of two cpos with a new, dedicated \bot value: A + B = \{ (0, a) \mid a \in A \} \cup \{ (1, b) \mid b \in B \} \cup \{ \bot _{A+B} \} This construct is a cpo under the ordering: x \sqsubseteq y\;\;\text {iff}\;\;\begin {cases} \text {true} & \text {if}\ x=\bot _{A+B}\\ a \sqsubseteq a' & \text {if}\ x = (0,a)\ \text {and}\ y = (0, a') \\ b \sqsubseteq b' & \text {if}\ x = (1,b)\ \text {and}\ y = (1, b') \\ \text {false} & \text {otherwise} \end {cases} Intuitively, this says that the ordering on A + B is the same as A and B separately, except that \bot _{A+B} is less than anything.

The only directed sets are those that do not contain a mixture of elements from both A and from B, so the least upper bound operator is essentially the same as the least upper bounds for A and for B. Formally: \bigsqcup X \;\; = \;\; \begin {cases} (0,\bigsqcup \{ a \mid (0,a) \in X \}) & \text {if}\ \{ a \mid (0,a) \in X \} \neq \emptyset \\ (1,\bigsqcup \{ b \mid (1,b) \in X \}) & \text {if}\ \{ b \mid (1,b) \in X \} \neq \emptyset \\ \bot _{A+B} & \text {otherwise}\\ \end {cases}

Primitive functions for sums [dt-003D]

DefinitionConstructors for sums [dt-0032]

For constructing sums, we use two primitive constructor functions, \mathit {inl} and \mathit {inr}: \begin {array}{l} \mathit {inl} : A \twoheadrightarrow (A + B)\\ \mathit {inl}(x) = (0,x)\\[1em] \mathit {inr} : B \twoheadrightarrow (A + B)\\ \mathit {inr}(y) = (1,y) \end {array}

TheoremContinuity of sum constructors [dt-0033]

The constructor functions \mathit {inl} and \mathit {inr} are continuous.

DefinitionThe case function [dt-0034]

Elimination of sums is captured by the case function [f,g] : (A + B) \twoheadrightarrow C, made from functions f : A \twoheadrightarrow C and g : B \twoheadrightarrow C. This function is defined by: \begin {array}{l} [f,g] : (A + B) \twoheadrightarrow C\\ [f,g](x) = \begin {cases} f(a) & \text {if}\ x = (0,a) \\ g(b) & \text {if}\ x = (1,b) \\ \bot _C & \text {if}\ x = \bot _{A+B}\end {cases} \end {array}

Exercise [dt-0035]

Prove that the case function [f,g](x) is, given continuous functions f : A \twoheadrightarrow C and g : B \twoheadrightarrow C, continuous on its argument x.

Solution.

Locality of sums [dt-0039]

We can see by the definitions of case and our constructors that [f,g] \circ \mathit {inl} = f and [f,g] \circ \mathit {inr} = g, or, in a commutative diagram:

Note that this diagram is like the dual of the diagram seen in the universal property for products — the arrows are reversed. That is because, generally speaking, sums are dual to products. However, because of our additional \bot value, our cpo sums are only weakly universal — the h arrow is not unique.

ExampleWeak universality of cpo sums [dt-003A]

Consider this scenario with the cpos \textbf {2} = \{ \top , \bot \} and \textbf {1} = \{\bot \}:

In this case, setting the function h = \lambda x.\ \top makes the diagram commute, but (\lambda x.\ \top ) \neq [\lambda x.\ \top , \lambda x.\ \top ] due to the different handling of \bot _{\textbf {1}+\textbf {1}}.

DefinitionWeak universal property for cpo sums [dt-003B]

(h \circ \mathit {inl} = f \land h \circ \mathit {inr} = g)\;\; \text {iff}\;\; [f,g] \sqsubseteq h

This property is called weak because it uses only the information ordering rather than equality on the right hand side.

WarningFailure of sum isomorphisms [dt-003C]

The weakness of the universal property for sums means that many common isomorphisms for sums in other contexts do not hold:

  • A + (B + C) \not \simeq (A + B) + C
  • (A \twoheadrightarrow C) \times (B \twoheadrightarrow C) \not \simeq (A+B) \twoheadrightarrow C

Sums form a bifunctor [dt-0036]

With these, we can define the morphism mapping for the sum bifunctor (+) : \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}. Just as with products and functions, we will overload the + notation for morphisms as well as objects in the category \mathbf {Cpo}.

DefinitionSum of functions [dt-0037]

Given functions f : A \twoheadrightarrow C and g : B \twoheadrightarrow D, we have: \begin {array}{l} f+g : (A + B)\twoheadrightarrow (C + D) \\ f+g = [\mathit {inl} \circ f, \mathit {inr} \circ g] \end {array}

Theorem [dt-0038]

+ : \mathbf {Cpo} \times \mathbf {Cpo} \rightarrow \mathbf {Cpo} is a lawful bifunctor, that is:

  1. (\lambda a. a) \times (\lambda b. b) = (\lambda x.x)
  2. (f_1 \circ g_1) \times (f_2 \circ g_2) = (f_1 \times f_2) \circ (g_1 \times g_2)

Upshot.

Our category \mathbf {Cpo} has only local sums.

Context

    Lecture. Domain theory › Constructions on cpos and PCF [dt-001Z]

    Related

      Locality of sums [dt-0039]

      Example. The category \mathbf {Cpo} [dt-002B]