Is there an (order-theoretic) version of bijectivity? But appropriate for lower adjoints.

Question

Let $f : X \rightarrow Y$ denote a function. Then the following are equivalent.

1. ($f$ is an isomorphism) There exists a function $g : Y \rightarrow X$ such that $$\forall x \in X, y \in Y \;\;\; f(x) = y \;\leftrightarrow\; x=g(y).$$

2. ($f$ is a bijection). For all $y \in Y$, there is unique $x \in X$ with $f(x)=y$.

Now let $f : X \rightarrow Y$ denote a poset arrow. Then we have the following definition.

1. ($f$ is a lower adjoint) There exists an arrow $g : Y \rightarrow X$ such that $$\forall x \in X, y \in Y \;\;\; f(x) \leq y \;\leftrightarrow\; x \leq g(y).$$

2. ??? Question. Is there something like bijectivity, but for lower adjoints?

Answer 1

The obvious condition to try is: "for all $y\in Y$ there is a unique $x\in X$ satisfying $f(x)\leq y$". But (as you are probably aware) this is too strong, because if we define $g(y)$ to be this unique element then we have $f(x)\leq y\rightarrow x=g(y)$. We therefore have to weaken 'unique' to something that still allows us to uniquely identify an element (so that we can define a function $g$) without forcing $f(x)\leq y\rightarrow x=g(y)$.

The correct condition is: "for all $y\in Y$ there is a maximum $x\in X$ satisfying $f(x)\leq y$".

If we define $g(y)$ to be this maximum element then we immediately have $f(x)\leq y\rightarrow x\leq g(y)$. We also have $$x\leq g(y)\quad\rightarrow\quad f(x)\leq f(g(y))\leq y$$ because $f$ is a poset arrow and because $g(y)$ itself satisfies $f(g(y))\leq y$.

Answer 2

Its called residuated. From wikipedia:

If $A,B$ are posets, a function $f : A \rightarrow B$ is residuated if and only if the preimage under $f$ of every principal down-set of $B$ is a principal down-set of $A$.