I'm reading about the category $\mathbf{FinRel}$ on the $n$Lab and it said: "$\mathbf{FinRel}$ is equivalent to $\mathrm{Mat(Bool)}$", without giving any explanation. Does anyone know how to prove it?

$\begingroup$ FWIW a wonderful application of this equivalence is arxiv.org/abs/1609.00061 $\endgroup$ – Steve Huntsman Oct 26 at 14:53

$\begingroup$ @SteveHuntsman Well, a neat application, but there are differences to what this question is about. FinRel and Mat(Bool) are have distinct domain and codomain sides, whereas the boolean arrays of that paper only have a codomain side (although it can be incident with several objects on that side) — it's the difference between a directed graph and an undirected hypergraph. As a result their wiring diagrams ("generalised matrix multiplications") only become an operad, whereas already FinRel and Mat(Bool) are PROPs. $\endgroup$ – Lars H Oct 26 at 17:42

$\begingroup$ Just if you are looking for more references, I believe that the proof of this fact is a slight modification of Proposition 2.6 in one of my go to papers Some algebraic laws for spans (and their connections with multirelations), by Bruni and Gadducci which exhibits an equivalence between spans of (infinite) sets and multirelations. $\endgroup$ – Cole Comfort Nov 2 at 0:04
My comment was misleading, and written in haste. Here's a better version. Recall that the objects of $\mathrm{Mat(Bool)}$ are the natural numbers, and a morphism $n\to m$ is an $m\times n$ matrix of booleans, which we can identify with $0,1$. There is an inclusion functor $$ \mathrm{Mat(Bool)} \hookrightarrow \mathbf{FinRel} $$ sending $n\mapsto \{1,\ldots,n\} =: \mathbf{n}$, and the matrix $A$ to the subset of $\mathbf{m} \times \mathbf{n}$ whose indicator function is given by $A$, which is interpreted as a function $\mathbf{m} \times \mathbf{n} \to \{0,1\}$. Matrix multiplication corresponds to composition of relations. Every relation from $\mathbf{n}$ to $\mathbf{m}$ can be uniquely reconstructed from such a indicator function/matrix. This means the inclusion is fully faithful. The inclusion is essentially surjective since there is a bijection between a finite set and one of the standard finite sets $\mathbf{n}$.

$\begingroup$ thanks for the reply. Your proof of functor from MatBool > FinRel is clear and straightforward. Although I do have another question: in the end you mentioned the inclusion is surjective, to prove equivalence we still need to define the other functor, from FinRel > MatBool, and prove the adjoint exists, correct? Excuse me if the question is juvenile  am a beginner in category theory. $\endgroup$ – GalaxyY Oct 27 at 10:03

$\begingroup$ @GalaxyY this is true, but you can get that from standard theory, see eg Prop 2.2 at ncatlab.org/nlab/show/equivalence+of+categories (one must choose an isomorphism from each finite set $S$ to $\mathbf{n}$, where $S=n$, then the other functor is built algebraically and is an adjoint inverse to the inclusion). Or, to keep it on the SE network, see math.stackexchange.com/questions/657707/… $\endgroup$ – David Roberts Oct 27 at 12:09