Embedding-projection pair (source code)

= Embedding-projection pair
{title2=$pe=\operatorname{id},\quad ep\leq\operatorname{id}$}

For <Scott continuous maps> $e:D\to E$, $p:E\to D$, these two identities say that $D$ is embedded in $E$ and that projection followed by embedding approximates from below. Such pairs lift to endomorphism spaces by $f\mapsto efp$ and $g\mapsto pge$. Their composite on the smaller space is the identity, and the other composite is $g\mapsto(ep)g(ep)\leq g$.