Let $\mathbf{Rel}$ be the bicategory of sets, relations, and inclusions between relations. The following fact is well-known:
- Any ordinary function $f : X \to Y$ between sets induces a pair of relations $B(1,f) : X \to Y$ and $B(f,1) : Y \to X$ in $\mathbf{Rel}$, defined explicitly by \begin{align*} B(1,f) &= (x,y) \mapsto y = f(x)\\ B(f,1) &= (y,x) \mapsto f(x) = y \end{align*} forming an adjunction $B(1,f) \dashv B(f,1)$. In particular, the unit and the counit of this adjunction correspond to the following logical implications: $$ \eta : x' = x \longrightarrow \exists y. y = f(x) \wedge f(x') = y $$ $$ \epsilon : \exists x. f(x) = y \wedge y' = f(x) \longrightarrow y' = y $$
One way of generalizing this example is by replacing sets with categories and relations by profunctors, considering the bicategory $\mathbf{Prof}$ as a proarrow equipment over $\mathbf{Cat}$.
I'm interested in a different sort of potential generalization. At least in the case of finite sets, a relation $X \to Y$ can be seen as an $X\times Y$ matrix with boolean-valued entries. Suppose we generalize to finite matrices valued in an arbitrary field $k$. Such matrices clearly form a 1-category (call it $\mathbf{FinMat}_k$), with composition defined by matrix multiplication. Moreover, every finite function $f : X \to Y$ induces a pair of matrices $B(1,f) : X \to Y$ and $B(f,1) : Y \to X$, corresponding to the indicator function \begin{align*} B(1,f) &= (x,y) \mapsto [y = f(x)]\\ B(f,1) &= (y,x) \mapsto [f(x) = y] \end{align*} where $[a = b]$ is 1 if $a = b$ and 0 otherwise.
Question: Is there a natural bicategorical structure on $\mathbf{FinMat}_k$ (at least for certain values of $k$), such that for every finite function $f : X \to Y$, we have an adjunction $B(1,f) \dashv B(f,1)$ in $\mathbf{FinMat}_k$? (Perhaps it is necessary to adjust the definition of $B(1,f)$ or $B(f,1)$?)
As a non-example which was my first attempt, in the case of $k = \mathbb{R}$, we could define 2-cells between real-valued matrices $\alpha : f \Rightarrow g : X \to Y$ as a family of inequalities $$ \alpha_{x,y} : f(x,y) \le g(x,y) $$ However, this would not verify the adjunction. In particular, although we do have an $\eta$ inequality \begin{align*} [x' = x] &\le [f(x') = f(x)] \\ &= \sum_y [y = f(x)] \cdot [f(x') = y] \end{align*} for every $x$ and $x'$, the $\epsilon$ inequality $$ \sum_x [f(x) = y] \cdot [y' = f(x)] \le [y' = y] $$ does not necessarily hold (in general, only if $f$ is injective).
