Let f : D \twoheadrightarrow E be a continuous function between algebraic cpos. Define: G_f = \{ (a,b) \in \mathsf {K}(D) \times \mathsf {K}(E) \mid b \sqsubseteq f(a) \} Then for all x \in D, prove that: f(x) = \bigsqcup \ \{ b \mid (a,b) \in G_f \land a \sqsubseteq x \}

Solution.

• Liam O'Connor

\begin {array}{lclr} f(x) & = & f(\bigsqcup \mathop {\downarrow }(x)) & \text {($D$ is {algebraic})}\\ &=&\bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \} & \text {($f$ is continuous)}\\ &=&\bigsqcup \ \left \{ \bigsqcup \mathop {\downarrow }(f(a)) \mid a \in \mathop {\downarrow }(x) \right \} & \text {($E$ is {algebraic})}\\ &=&\bigsqcup \ \{ b \in \mathsf {K}(E) \mid b \sqsubseteq f(a) \land a \in \mathop {\downarrow }(x)\} & \text {(lubs and defn of $\downarrow $)}\\ &=&\bigsqcup \ \{ b \mid (a,b) \in G_f \land a \sqsubseteq x \}&\text {(defn of $G_f$)} \end {array}

This is powerful. For example, the continuous function f : \mathcal {P}(\mathbb {N}) \twoheadrightarrow \mathcal {P}(\mathbb {N}) on an uncountable cpo \mathcal {P}(\mathbb {N}) is completely determined by the countable relation G_f.