residuated
Let $P,Q$ be two posets. Recall that a function $f:P\to Q$ is order preserving iff $x\le y$ implies $f(x)\le f(y)$. This is equivalent^{} to saying that the preimage^{} of any down set under $f$ is a down set.
Definition A function $f:P\to Q$ between ordered sets $P,Q$ is said to be residuated if the preimage of any principal down set is a principal down set. In other words, for any $y\in Q$, there is some $x\in P$ such that
$${f}^{1}(\downarrow y)=\downarrow x,$$ 
where ${f}^{1}(A)$ for any $A\subseteq Q$ is the set $\{a\in X\mid f(a)\in A\}$, and $\downarrow b=\{c\mid c\le b\}$.
Let us make some observations on a residuated function $f:P\to Q$:

1.
$f$ is order preserving.
Proof.
Suppose $a\le b$ in $P$. Then there is some $c\in P$ such that $\downarrow c={f}^{1}\phantom{\rule{veryverythickmathspace}{0ex}}(\downarrow f(b))$. Since $f(b)\in \downarrow f(b)$, $b\in \downarrow c$, or $b\le c$, which means $a\le c$, or $a\in \downarrow c$. But this implies $a\in {f}^{1}\phantom{\rule{veryverythickmathspace}{0ex}}(\downarrow f(b))$, so that $f(a)\in \downarrow f(b)$, or $f(a)\le f(b)$. ∎

2.
The $x$ in the definition above is unique.
Proof.
If $\downarrow x=\downarrow z$, then $x\in \downarrow z$, or $x\le z$. Similarly, $z\le x$, so that $x=z$. ∎

3.
$g:Q\to P$ given by $g(y)=x$ is a welldefined function, with the following properties:

(a)
$g$ is order preserving,

(b)
${1}_{P}\le g\circ f$,

(c)
$f\circ g\le {1}_{Q}$.
Proof.
$g$ is order preserving: if $r\le s$ in $Q$, then $\downarrow r\subseteq \downarrow s$, so that $\downarrow u={f}^{1}(\downarrow r)\subseteq {f}^{1}(\downarrow s)=\downarrow v$, where $u=g(r)$ and $v=g(s)$. But $\downarrow u\subseteq \downarrow v$ implies $u\le v$, or $g(r)\le g(s)$.
${1}_{P}\le g\circ f$: let $x\in P$, $y=f(x)$, and $z=g(y)$. Then $x\in {f}^{1}(y)\subseteq {f}^{1}(\downarrow y)=\downarrow z$, which implies $x\le z=g(f(x))$ as desired.
$f\circ g\le {1}_{Q}$: pick $y\in Q$ and let $x=g(y)$. Then ${f}^{1}(\downarrow y)=\downarrow x$, so that $f(x)\in f(\downarrow x)=f({f}^{1}(\downarrow y))=\downarrow y$, or $f(x)\le y$, or $f(g(y))=f(x)\le y$ as a result. ∎

(a)
Actually, the third observation above characterizes $f$ being residuated:
Proposition 1.
If $f$ is order preserving, and $g$ satisfies $\mathrm{3}\mathit{}\mathrm{(}a\mathrm{)}$ through $\mathrm{3}\mathit{}\mathrm{(}c\mathrm{)}$, then $f$ is residuated. In fact, such a $g$ is unique.
Proof.
Suppose $y\in Q$, and let $x=g(y)$. We want to show that $\downarrow x={f}^{1}\phantom{\rule{veryverythickmathspace}{0ex}}(\downarrow y)$. First, suppose $a\in {f}^{1}\phantom{\rule{veryverythickmathspace}{0ex}}(\downarrow y)$. Then $f(a)\le y$, which means $g(f(a))\le g(y)=x$. But then $a\le g(f(a))$, and we get $a\le x$, or $a\in \downarrow x$. Next, suppose $a\le x=g(y)$. Then $f(a)\le f(x)=f(g(y))\le y$, so $a\in {f}^{1}(f(a))\subseteq {f}^{1}\phantom{\rule{veryverythickmathspace}{0ex}}(\downarrow y)$.
To see uniqueness, suppose $h:Q\to P$ is order preserving such that ${1}_{P}\le h\circ f$ and $f\circ h\le {1}_{Q}$. Then $g={1}_{P}\circ g\le (h\circ f)\circ g=h\circ (f\circ g)\le =h\circ {1}_{Q}=h$ and $h={1}_{P}\circ h\le (g\circ f)\circ h=g\circ (f\circ h)\le g\circ {1}_{Q}=g$. ∎
Definition. Given a residuated function $f:P\to Q$, the unique function $g:Q\to P$ defined above is called the residual of $f$, and is denoted by ${f}^{+}$.
For example, given any function $f:A\to B$, the induced function $f:P(A)\to P(B)$ (by abuse of notation, we use the same notation as original function $f$), given by $f(S)=\{f(a)\mid a\in S\}$ is residuated. Its residual is the function ${f}^{1}:P(B)\to P(A)$, given by ${f}^{1}(T)=\{a\in A\mid f(a)\in T\}$.
Here are some properties of residuated functions and their residuals:

•
A bijective^{} residuated function is an order isomorphism, and conversely. Furthermore, the residual is residuated, and is its inverse^{}.

•
If $f:P\to Q$ is residuated, then $f\circ {f}^{+}\circ f=f$ and ${f}^{+}\circ f\circ {f}^{+}={f}^{+}$.

•
If $f:P\to Q$ and $g:Q\to R$ are residuated, so is $g\circ f$ and ${(g\circ f)}^{+}={f}^{+}\circ {g}^{+}$.

•
If $f:P\to Q$ is residuated, then ${f}^{+}\circ f:P\to P$ is a closure map on $P$. Conversely, any closure function can be decomposed as the functional^{} composition^{} of a residuated function and its residual.
Remark. Residuated functions and their residuals are closely related to Galois connections. If $f:P\to Q$ is residuated, then $(f,{f}^{+})$ forms a Galois connection between $P$ and $Q$. On the other hand, if $(f,g)$ is a Galois connection between $P$ and $Q$, then $f:P\to Q$ is residuated, and $g:Q\to P$ is ${f}^{+}$. Note that PM defines a Galois connection as a pair of orderpreserving maps, where as in Blyth, they are order reversing.
References
 1 T.S. Blyth, Lattices and Ordered Algebraic Structures^{}, Springer, New York (2005).
 2 G. Grätzer, General Lattice Theory, 2nd Edition, Birkhäuser (1998)
Title  residuated 

Canonical name  Residuated 
Date of creation  20130322 18:53:22 
Last modified on  20130322 18:53:22 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  12 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 06A99 
Classification  msc 06A15 
Defines  residual 