I stumbled across a cute result about order-reflecting functions.
A couple of questions:
Is the following result well-known?
I know lots of place to learn about order-preserving functions, but is there anywhere can I learn about order-reflecting functions (article, book etc.)?
Its easy to see that they form a category. Has this point of view been developed anywhere?
Here's the good stuff.
Definition. If $P$ and $Q$ are prosets and $f : P \rightarrow Q$ is an arbitrary function (not necessarily order-preserving), we say that $f$ is order-reflecting iff
$$\forall xy \in P : f(x) \leq f(y) \implies x \leq y.$$
Proposition. If $P$ and $Q$ are prosets and $f : P \rightarrow Q$ is an order-reflecting function with downward-closed image, then $f$ preserves downward-closedness.
Proof. Suppose $P$ and $Q$ are prosets and that $f : P \rightarrow Q$ is an order-reflecting function with the property that $f(P)$ is downward-closed.
Now assume for a contradiction that some downward-closed $P' \subseteq P$ has the property that $f(P')$ is not downward-closed. Find $q \in Q$ and $q' \in f(P')$ such that $q \leq q'$, but $q \notin f(P').$ We will contradict this last statement.
Since $q' \in f(P'),$ thus $q' \in f(P).$ Thus we have written down all of the following:
$$q' \in f(P), \quad q \leq q',\quad f(P) \mbox{ is downward closed}.$$
Deduce that $q \in f(P)$. So in summary:
$$q \in f(P), \quad q' \in f(P'),\quad q \leq q'$$
Thus we can find $p \in P$ and $p' \in P'$ such that $f(p) = q$ and $f(p')=q'$. But since $q \leq q'$, thus $p \leq p'$ (by the order-reflecting property of $f$). So in summary
$$p \in P, \quad p' \in P',\quad p \leq p'$$
Now recall that $P'$ is downward-closed. Thus $p \in P'$. So $q \in f(P')$, which is a contradiction.
Your proof of the Proposition is unnecessarily complicated. You don't have to write it as a contradiction.
Let $P' \subseteq P$ be downward-closed. In order to show that $f(P') \subseteq Q$ is downward-closed, let $q' \in f(P')$ and $q \leq q'$. Then $q'=f(p')$ and $q=f(p)$ for some $p \in P, p' \in P'$. Since $f$ is order-reflecting, we have $p \leq p'$, hence $p \in P'$ and therefore $q \in f(P')$.
The proof is entirely obvious. In research papers such a Proposition would be regarded as trivial and used without proof. Also remark that the proof doesn't use the properties of $\leq$. It could be any relation whatsoever.
I'm afraid that I cannot offer any literature about order-reflecting maps, but this notion is well-known. When we regard posets as thin categories, order-preserving maps correspond to functors (and order-embeddings to fully faithful functors). Order-reflecting maps correspond to "op-functors" which I define as follows: If $\mathcal{C},\,\mathcal{D}$ are categories, an "op-functor" $F : \mathcal{C} \to \mathcal{D}$ associates to every object $C \in \mathcal{C}$ and object $F(C) \in \mathcal{D}$ and to every morphism $\phi : F(C) \to F(D)$ a morphism $F^{-1}(\phi) : C \to D$, such that the following holds: $F^{-1}(\mathrm{id}_{F(C)})=\mathrm{id}_C$ and for $F(C) \xrightarrow{\phi} F(D) \xrightarrow{\psi} F(E)$ we have $F^{-1}(\psi \phi) = F^{-1}(\psi) F^{-1}(\phi)$. There is an identity op-functor and op-functors can be composed in the obvious way. Thus, we get the category of (small) categories and op-funtors.
The terminology "op-functor" is not perfect and it could easily get confused with "oplax functor" which are defined in higher category theory. I don't know if these things already have a name.
Obviously every fully faithful functor $\mathcal{C} \to \mathcal{D}$ induces an op-functor $\mathcal{C} \to \mathcal{D}$. More generally, every full functor in which the preimages can be chosen in a coherent way induces an op-functor. If $\mathcal{C}$ and $\mathcal{D}$ have only one object, i.e. they correspond to monoids, then an op-functor is just a homomorphism of monoids in the other direction. It would be interesting to see a natural example of an op-functor (not between posets or monoids) which doesn't arise this way.