Theorem. Continuity of sum constructors [dt-0033]

Liam O'Connor

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

Context

Primitive functions for sums [dt-003D]

Liam O'Connor

Definition. Constructors for sums [dt-0032]

Liam O'Connor

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}$

Theorem. Continuity of sum constructors [dt-0033]

Liam O'Connor

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

Definition. The case function [dt-0034]

Liam O'Connor

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]

Liam O'Connor

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.

Liam O'Connor

As mentioned in Construction [dt-0031], the only directed subsets of $A + B$ are those that contain entirely values of the format $(0,\_)$ and optionally $\bot _{A+B}$ , or those that contain entirely values of the format $(1,\_)$ and optionally $\bot _{A+B}$ . Call this directed subset $X$ .

When $\bigsqcup X = \bot _{A+B}$ : This means that $X = \{\bot _{A+B}\}$ as $\bot$ is always the least element. From Definition [dt-0034], we have: $\begin {array}{lcl} [f,g](\bigsqcup X) &=& [f,g](\bot _{A+B}) \\ &=& \bot _C \\ &=& \bigsqcup \{\bot _C\} \\ &=& \bigsqcup \{[f,g](\bot _{A+B})\} \\ &=& \bigsqcup \{[f,g](x) \mid x \in X\}\end {array}$ This discharges both requirements in Definition [dt-001J] for this case.
When $\bigsqcup X = (0,\_)$ : This means that $X$ consists of at least one $(0,\_)$ value plus possibly $\bot _{A+B}$ , that is $X \setminus \{\bot _{A+B}\} = \{ (0,a) \mid a \in Y\}$ for some nonempty $Y \subseteq A$ . We have the following, using the continuity of $f$ : $\begin {array}{lcl} [f,g](\bigsqcup X) &=& [f,g](\bigsqcup (X \setminus \{\bot _{A+B}\})) \\ &=& [f,g](\bigsqcup \{ (0,a) \mid a \in Y\} )\\ &=& [f,g](0,\bigsqcup Y) \\ &=& f(\bigsqcup Y) \\ &=& \bigsqcup \{ f(a) \mid a \in Y \} \\ &=& \bigsqcup \{ [f,g](0,a) \mid a \in Y\} \\ &=& \bigsqcup \{ [f,g](x) \mid x \in X \setminus \{\bot _{A+B}\} \} \\ &=& \bigsqcup (\{ [f,g](x) \mid x \in X \setminus \{\bot _{A+B}\} \} \cup \{\bot _C\}) \\ &=& \bigsqcup \{ [f,g](x) \mid x \in X \} \\ \end {array}$
When $\bigsqcup X = (1,\_)$ : Similar to the $(0,\_)$ case but using $g$ rather than $f$ .

Related

Definition. Constructors for sums [dt-0032]

Liam O'Connor

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}$

Definition. Continuity [dt-001J]

Liam O'Connor

A function $f : A \rightarrow B$ on cpos $A$ and $B$ is continuous iff for all directed $X \subseteq A$ ,

$\bigsqcup \{ f(x) \mid x \in X \}$ exists, and
$f(\bigsqcup X) = \bigsqcup \{ f(x) \mid x \in X \}$ , i.e., $f$ preserves lubs.

The intuition behind continuity is that "nothing is suddenly invented at infinity": our function will behave analogously at the limit as it does for each element in our chain.