# Lawvere-Cauchy Completeness

This is a commentary on the proposition on page 163 of Lawvere's [Metric spaces,generalized logic, and closed categories](https://raw.githubusercontent.com/mattearnshaw/lawvere/master/pdfs/1973-metric-spaces-generalized-logic-closed-categories.pdf).

[More examples](https://hackmd.io/@alexhkurz/S1ehYwQ1v) and a less technical account.

A review of [monotone relations](https://alexhkurz.github.io/papers/kv-relation-lifting.pdf).

## Relations induced by maps are adjoint

Let $f:X\to Y$. Define

$$f_\diamond(x,y)= Y(f(x),y)$$

$$f^\diamond(x,y) = Y(y,f(x))$$

**Proposition:** $\ f_\diamond \dashv f^\diamond.$

*Proof:* $f_\diamond\,;f^\diamond = \bigvee_y Y(f(x),y) \otimes Y(y,f(x'))\ge Y(f(x),f(x)) \otimes Y(f(x),f(x'))\ge X(x,x')$ and $f^\diamond\,;f_\diamond = \bigvee_x Y(y,f(x))\otimes Y(f(x),y') \le Y(y,y')$.

## Adjoints are almost induced by maps

Let $L:X\to Y$ and $R:Y\to X$ be two relations. Suppose $L\dashv R$. That is

$$X(x,x') \ \le \ \bigvee_y xLy \otimes yRx'$$

$$\bigvee_x yRx \otimes xLy' \ \le \
Y(y,y')$$

**Definition:** $Y$ is ***Cauchy complete*** if every left-adjoint relation $X\to Y$ is of the form $Y(f(x),y)$.

To explain the terminology, specialise to the case where $\mathcal V= [0,\infty]$ and $X=1$ and $Y$ a Lawvere metric space and $\bigvee = \inf$ and $\otimes = +$. Due to $X=1$ both $L$ and $R$ are now $[0,\infty]$-valued functions. Note that we switch now to the order on the reals wich is the converse of the order on $\mathcal V$.

We obtain

$$0 \ = \ \inf_y\, \{ L(y) + R(y) \}$$

$$ R(y) + L(y') \ \ge \ Y(y,y')$$

$L$ is induced by a map iff there is $a\in Y$ such that $Ly = Y(a,y)$.

- If $Y$ is Cauchy-complete, we can find $a$ by a Cauchy sequence as follows.

Due to the first equation, for each $n\in\mathbb N$, there must be a $y_n$ such that $L(y_n) + R(y_n)\le 1/n$. The second inequation then guarantees that $Y(y_n,y_m)\le 1/n + 1/m$. So we found a Cauchy-sequence, the limit of which we call $a$.

It remains to show that $Ly = Y(a,y)$ ...

- On the other hand, if $(y_n)_{n\in\mathbb N}$ is a Cauchy sequence, then we can find $L$ such that $Ly = Y(a,y)$.