A residuated lattice is an algebra, $L=(L,\wedge,\vee, \cdot, \backslash, /,1)$ such that
$(L,\wedge,\vee)$ is a lattice;
$(L,\cdot,1)$ is a monoid;
for all $a,b,c\in L$,
Let $(M,\cdot, e)$ be a monoid and consider $L=\mathcal{P}(M)$.
If $X, Y\subseteq M$, define
and then $L$ with this structure is a residuated lattice.
For any set, $X$, the relation algebra, $Rel(X)=\mathcal{P}(X\times X)$ of binary relations on $X$ is a residuated lattice.
Writing $R^-$ for the complement of a relation, $R$, and $R;S$ for the relational composition of two relations, $R$ and $S$, we define
$R \backslash S = (R;S^-)^- ,$
$S / R = (S^-;R)^-$
and
$R\to S= (R\cap S^-)^- = R^-\cup S.$
We have
$(Rel(X), \cap,\cup,\to, \emptyset, X^2)$ is a Boolean algebra,
$(Rel(X), ; \Delta)$ is a monad, where $\Delta$ is the diagonal / equality relation;
the residuation relation is satisfied:
Any lattice ordered group gives a residuated lattice. This is described in the entry on lattice ordered groups. It is noteworthy that in this context, the residuals are quotients and, in fact, the inverses in the group are residuals.
Looking at the poset structure of $L$ as a category, one rewrites $a\le b$ as $a\to b$ and $L(a,b)$ for the singleton set consisting just of the morphism $a\to b$.
We have for each element $a$ in $L$, two mappings given by, respectively, left and right multiplication by $a$:
These mappings are order preserving, so give endofunctors on the category $L$. For instance, suppose $x\le y$ and we have $a\cdot y\leq b$. We then have $y\leq a/b$, and hence $x\le a/b$, i.e. $a\cdot x\leq b$. Now take $b= a\cdot y$. We have thus that $a\cdot x\leq a\cdot y$, as required.
In this interpretation, both these functors have right adjoints, namely the two residuals. We have, for instance,
The residual functor, $a\backslash -$, acts like a left exponential object for the left multiplication functor. Likewise $-/a$ acts like a right exponential object functor.
This point of view is explored further in the entry on residuals.
A classical reference is
A set of slides from a modern treatment is
Last revised on September 10, 2021 at 03:19:50. See the history of this page for a list of all contributions to it.