NB: even though this question's longish setup gives the impression that it is about the theory of ordered sets, in fact it is really more general than that. The setup here serves only as the immediate motivation for a much more general question (about category theory) at the end.
In what follows, $(P, \leq)$ and $(Q, \leq)$ are always posets.
If $\varphi: (P, \leq) \to (Q, \leq)$, we say that $\varphi$ is monotone iff $(x \leq y) \Rightarrow (\varphi(x) \leq \varphi(y))$. We say that $\varphi$ is an order-embedding iff $\forall x, y \in P: (x \leq y) \Leftrightarrow (\varphi(x) \leq \varphi(y))$.
For any poset $(P,\leq)$, we say that $Y \subseteq P$ is a downset of $(P, \leq)$ iff $((y \in Y)\;\wedge\; (x \leq y)) \Rightarrow (x \in Y)$.
We denote by ${\mathcal O}(P) \subseteq \wp(P)$ the set of all the downsets of $(P, \leq)$.
Claim 1: $\varphi: (P, \leq) \to (Q, \leq)$ is monotone iff $\forall A \in {\mathcal O}(Q): \varphi^{-1}(A) \in {\mathcal O}(P).$
If $\varphi: (P, \leq) \to (Q, \leq)$ is monotone, Claim 1 implies that $\tilde{\varphi}^{-1}(A) = \varphi^{-1}(A)$ specifies a well-defined map $\tilde{\varphi}^{-1}: {\mathcal O}(Q) \to {\mathcal O}(P)$.
For the next two claims, assume that the map $\varphi: (P, \leq) \to (Q, \leq)$ is monotone.
Claim 2: $\varphi: (P, \leq) \to (Q, \leq)$ is an order-embedding iff the corresponding map $\tilde{\varphi}^{-1}: {\mathcal O}(Q) \to {\mathcal O}(P), A \mapsto \varphi^{-1}(A)$ is a surjection.
Claim 3: $\varphi: (P, \leq) \to (Q, \leq)$ is a surjection iff the corresponding map $\tilde{\varphi}^{-1}: {\mathcal O}(Q) \to {\mathcal O}(P), A \mapsto \varphi^{-1}(A)$ is an injection.
OK, so much for setup.
I don't know much category theory, but I know just enough of it to recognize that the first two lines in the setup above are describing the Poset category, whose objects are posets and whose morphisms are the monotone maps.
Question: what, if any, would be the "category-theoretical rendition" of the remainder of this setup?
More specifically, what are the general categorical concepts/terms/theorems for the roles played in this setup by the following?
- the order-embeddings;
- a downset of a poset;
- the set ${\mathcal O}(P)$ of all downsets of a poset $(P, \leq)$;
- the map $\tilde{\varphi}^{-1}: {\mathcal O}(Q) \to {\mathcal O}(P)$ induced by the morphism $\varphi: (P, \leq) \to (Q, \leq)$;
- Claim 1;
- Claim 2;
- Claim 3.