Definition. Retraction pair [dt-0054]

A retraction pair (f,g) on cpos A to B consists of two continuous functions A \xtofrom [g]{f} B such that:

  1. g \circ f = \mathsf {id}_A\quad (i.e. \forall x \in A.\ g(f(x)) = x )
  2. f \circ g \sqsubseteq \mathsf {id}_B\quad (i.e. \forall y \in B.\ f(g(y)) \sqsubseteq y )
In this retraction pair, f is called a embedding and g is called a projection.

Retraction pairs are weakenings of isomorphisms. Intuitively, going A \twoheadrightarrow B\twoheadrightarrow A, all information is preserved due to requirement 1, but going B\twoheadrightarrow A\twoheadrightarrow B, we may lose some information (hence the use of \sqsubseteq in requirement 2).