9. Syntax and semantics adjunction $Re\dashv Ex$ [0033]

There exists a “syntax and semantics” adjunction between the theory of exactness and the theory of relations.

In order to make this precise, let’s work in a category $C$ (the generalization to 2-categories is straightforward) and let’s consider:

  1. The category $P(C^\square)$ whose objects are subsets of the set of commutative squares of $C$, and where morphisms are inclusions;
  2. The category $PMI(C)$ of involutive promonads $(L,I)$ on $C$ whose objects are bijective-on-objects functors $L : C\to R$ coupled with involutions on $R$, i.e. functors $I : R\to R^\op$ that are the identity on objects and such that $I^\op\circ I=1_R$, and where morphisms $H : (L,I)\to (L’,I’)$ are functors $H : R\to R’$ such that $H\circ L = L’$ and $I’\circ H = H\circ I$.

From this we can define a functor

$$ \Ex : PMI(C)\to P(C^\square) $$

sending an involutive promonad $(L,I)$ to the set of commutative squares

$$ \begin{CD} \bullet @>t>> \bullet \\ @VsVV @VVvV \\ \bullet @>>u> \bullet \end{CD} $$

which moreover are “anticommutative in $R$”, meaning that $Ls\circ ILt = ILu\circ Lv$.

Such a functor admits a left adjoint

$$ Re : P(C^\square) \to PMI(C) $$

that we can describe as follows:

  • Denote by $\Ch(C)$ the free category of paths in $C$, whose objects are those of $C$ and where morphisms from $A$to $B$ are tuples $(X_1,\dots,X_n;f_1,\dots,f_n)$ for which $X_1=A, X_n=B$ and for each $i\le n$, each $X_i$ is an object of $C$ and $f_i = X_i\to X_{i+1}$ or $f_i : X_{i+1}\to X_i$ (the composition of such morphisms is then defined by mere juxtaposition).
  • Denote by $ZZ(C)$ the free category with involution over $C$, whose objects are the same of $C$ and whose morphisms from $A$ to $B$ are zig-zags (or paths) such that fo each $i\le n$, $f_i$ and $f_{i+1}$ are not composable (composition is then juxtaposition, followed if necessary by reduction, if $f_1’$ and $f_n$ are composable; so, $ZZ(C)$ is a certain quotient of $\Ch(C)$).
  • Finally, for any given $E\subseteq C^\square$, define $Re(E)$ to be the category obtained quotienting $\Ch(C)$ by the equivalence relation induced by the following rules:
    1. In every given path we can replace a pair $X \xto{f_i} Y \xto{f_{i+1}} Z$ with $f_{i+1}f_i : X\to Z$;
    2. In any given path we can replace $_i : X\to Y$ with a pair $X \xto{u} K \xto{v} Y$ if $f_i=v\circ u$;
    3. In any given path we can replace a span $X \xot{f_i} Y \xto{f_{i+1}} Z$ with a cospan $X \xto{u} K \xot{v} Z$ provided that the square belongs to $E$;
    4. In any given path we can replace a cospan $X \xto{f_i} Y \xot{f_{i+1}} Z$ with a span $X \xot{u} K \xto{v} Z$ provided that the square belongs to $E$;

Given this, two paths are equivalent if and only if there exists a sequence of transformations of type 1,2,3,4 such that, applied to one, leads to the other. Such a sequence is called an $E$-exact modification (observe that $Re(E)$ always arises as a quozient of $ZZ(C)$: starting from $ZZ(C)$, condition 1 becomes redundant but one never forget to apply condition 2).

The involution n $Re(E)$ is induced by the one on $\Ch(C)$. The verification of the adjunction $Re\dashv Ex$ (i.e. of the equivalence $E\subseteq Ex(R,I)$ if and only if $Re(E)\to (R,I)$, or in other words of the fact that the set of morphisms $Re(E)\to (R,I)$ is nonempty if and only if $E\subseteq Ex(R,I)$, and in such case it has a single element), is immediate.

[003A] Translator’s Note 9·a.

The proof is completely elementary, but I judge it far from being immediate… I might decide to write it up someday!

We see then that $Re(E)$-algebras are precisely $E$-extensors.