# WR: Calculus of Relations

I first write down the questions. Definitions follow the questions.

It is worth checking whether all the laws I put down here hold for relations and for monotone relations (as well as distributors/profunctors/bimodules).

## Questions

In category theory, one speaks of right and left (Kan) extensions and right and left (Kan) liftings. The right-extension and the right-lifting are residuation. But left-extension and left-lifting also play an important role. Do they show up in work on residuated lattices?

Order enriched categories (= 2-categories in which homsets are partially ordered) are really just many-sorted generalisations of residuated posets. What would be some results on residuated lattices which should be generalised to the many-sorted setting? (And maybe to the full generality of 2-categories?)

Residuation (=right extension/lifting) has nice explicit formulas in the category where arrows are relations. What about the left extension/lifting?

Adjoints are absolute right extensions/liftings of the identity. Does the notion of absoluteness show up in residuated lattices?

## Notation

I write $\cdot$ or $;$ or $\otimes$ for sequential composition of relations. The neutral element (identity relation) is written as 1.

The calculus is quite general. I write it out as if it was about relations $R:A\to B$ between sets $A,B$, but it also works for posets, preorders, categories and categories enriched over a complete and cocomplete monoidal category $\cal V$. In these cases $R:A\to B$ is of type $A\otimes B\to \mathcal V$.

## Definitions

### Residuation

$R:A\to B$, $S:B\to C$, $T:A\to C$.

$$R\subseteq T/S \ \Leftrightarrow \ R \cdot S \subseteq T \ \Leftrightarrow \ S\subseteq R\backslash T$$

$T/S = \bigcup\{ R\mid R\cdot S\subseteq T\} = \{(a,b) \mid \forall (b,c)\in S\,.\, (a,c)\in T \}$

$R\backslash T = \bigcup\{ S\mid R\cdot S\subseteq T\} = \{(b,c) \mid \forall (a,b)\in R\,.\, (a,c)\in T \}$

Remark: Residuation is known in category theory as right-extension and right-lifting (it is easy to see that $R\backslash T$ is the extension and $T/S$ the lifting when drawing the relations as arrows). The dual notions, left-extension and left-lifting are known as dual residuation.

### Extensions

$R:A\to B$, $S:B\to C$, $T:A\to C$.

$$T\subseteq R\cdot S \ \Leftrightarrow \ Lan_RT\subseteq S$$

$$R\cdot S \subseteq T \ \Leftrightarrow \ S\subseteq Ran_RT$$

Remark: The right-extension $Ran_RT$ is $R\backslash T$.

### Liftings

$R:B\to A$, $S:C\to B$, $T:C\to A$. (Note that we dualised the 1-cells $R,S,T$.)

$$T\subseteq S\cdot R \ \Leftrightarrow \ Lift_RT\subseteq S$$

$$S\cdot R \subseteq T \ \Leftrightarrow \ S\subseteq Rift_RT$$

Remark: The right-lifting $Rift_RT$ is $T/R$.

### Duality

Left and right are dual under switching the direction of 2-cells. Extensions and liftings are dual under switching the direction of 1-cells.

### Absoluteness

Extensions and liftings are called **absolute** if they satisfy the following.

\begin{gather}
Ran_RT\cdot H = Ran_R(TH)\\
Lan_RT\cdot H = Lan_R(TH)\\
H\cdot Rift_RT = Rift_R(HT)\\
H\cdot Lift_RT = Lift_R(HT)\\
\end{gather}

### Adjointness

Right and left-adjoints can be characterised as absolute right extensions and right liftings. Recall $Ran_LT= L\backslash T$ and $Rift_R T = T/R$.

$$L\dashv R \ \Longleftrightarrow \ R= 1/L \textrm{ and $R$ is an absolute lifting}$$

$$L\dashv R \ \Longleftrightarrow \ L = R\backslash 1 \textrm{ and $L$ is an absolute extension}$$

*Proof:* Assume $R= 1/L$ is an absolute lifting. We need to show $\ L\dashv R$, that is, $1\subseteq L\cdot R$ and $R\cdot L\subseteq 1$. From adjointness we have $1/L \cdot L\subseteq 1$ and with absolutness we obtain $1\subseteq (1\cdot L)/L=(L\cdot 1)/L=L\cdot 1/L$.

For the other direction, assume $\ L\dashv R$. The counit $R\cdot L\subseteq 1$ implies $R\subseteq 1/L$. To show the converse, we calculate $1/L = 1/L\cdot 1 \subseteq 1/L\cdot L \cdot R \subseteq 1 \cdot R = R$ and conclude $R = 1/L$. To show absoluteness, we note that $H\cdot 1/L \cdot L\subseteq H\cdot 1 = H$ implies $H\cdot 1/L \subseteq H/L$ and observe $H/L = H/L\cdot 1 \subseteq H/L\cdot L\cdot 1/L\subseteq H\cdot 1/L$, concluding $H\cdot 1/L = H/L$.

The second statment, about $R\backslash 1$, is dual. QED

### Maps and Relations

So far, we treated categories of relations as abstract order-enriched categories. Often, categories of relations arise from categories of maps. There are several ways to set up a calculus of maps plus relations. One can work with embeddings of maps into relations and axiomatise their properties. Or one can assemble maps and relations into a particular kind of double category (aka framed bicategories) with relations as horizontal arrows and maps as vertical arrows.

I am currently not sure about the slickest way to do this. So the following is preliminary.

Moreover, one can start from an order-regular category of maps and add relations. Or one can start from a regular category of maps, go to the category of [internal orders](https://hackmd.io/@alexhkurz/H1mRJ1Mxw) and then to relations.

In the following I start from an [order-regular category](https://hackmd.io/@alexhkurz/HJe-GE9zI).

#### Notation
- A *relation* $R:A\to B$ is a map $A^{op}\otimes B\to 2$.
- Composition of relations $R:A\to B,S:B\to C$ is written as $R\cdot S$ or sometimes $RS$.
- Composition of maps $f:A\to B,g:B\to C$ is written as $gf$ or $g\circ f$.
- For maps $f:X\to Y$, we define $xf_\diamond y =Y(f(x),y)$ and $yf^\diamond x =Y(y,f(x))$. We have $f_\diamond\dashv f^\diamond$.

#### Laws of the Embeddings

$f_\diamond\dashv f^\diamond$ means

$$ 1\le f_\diamond\cdot f^\diamond
\quad\quad\quad\quad
f^\diamond\cdot f_\diamond \le 1$$

Consequently,

$$R\cdot f_\diamond \le S\ \Leftrightarrow \ R\le S\cdot f^\diamond
\quad\quad\quad\quad
f^\diamond \cdot R \le S\ \Leftrightarrow \ R\le f_\diamond \cdot S$$

$(-)_\diamond$ is covariant on 1-cells and contravariant on 2-cells, while $(-)^\diamond$ is contravariant on 1-cells and covariant on 2-cells. To emphasise this we write here $f\,;g$ instead of $g\circ f$.

$$(f\,;g)_\diamond= f_\diamond\cdot g_\diamond
\quad\quad\quad\quad
(f\,; g)^\diamond = g^\diamond\cdot f^\diamond$$

$$f\le g \ \Rightarrow \ g_\diamond \le f_\diamond
\quad\quad\quad\quad
f\le g \ \Rightarrow \ f^\diamond \le g^\diamond$$

#### Generalised Elements

Writing small letters for maps and capital letter for relations:

$$a\,R\,b
\quad \Longleftrightarrow \quad b_\diamond \le a_\diamond\cdot R
\quad \Longleftrightarrow \quad a^\diamond\cdot b_\diamond \le R
\quad \Longleftrightarrow \quad a^\diamond\le R \cdot b^\diamond$$

#### Tabulating Relations

$R$ can be tabulated as $(f,g)$ if
$$R=f^\diamond\cdot g_\diamond$$

We write $R=(dR,cR)$ if $(dR,cR)$ tabulates $R$ and is a mono span.

... tbc ...

## Examples

## Further Reading

An excellent resource for the 2-categorical point of view is

- Lack: [A 2-categories companion](https://arxiv.org/pdf/math/0702535.pdf),

see Section 2.2 for extensions and liftings.

As always, the nLab is worth a look as well:

- nLab: [Kan extension](https://ncatlab.org/nlab/show/Kan+extension), [Kan lift](https://ncatlab.org/nlab/show/Kan+lift)