allegory

Recall the notion of a *unitary pre-tabular allegory*. Bicategories of relations are equivalent, but this has yet to be shown rigorously and published, as far as I’m aware.

This PDF file gives an explicit argument, which I put at bicategory of relations until Mike Shulman suggested the neater proof that’s there now. But I’ll keep this here anyway.

The following lemma is used at allegory.

If $f \colon X \to A$ and $g \colon X \to B$ are maps in a unitary pre-tabular allegory, then $\langle f, g \rangle = \pi_1^\circ f \cap \pi_2^\circ g$

Let $r = \pi_1^\circ f \cap \pi_2^\circ g$. Then $\pi_1 r = f$ and $\pi_2 r = g$, by the modular law and the fact that projections tabulate top elements. So $r = \langle f, g \rangle$ if and only if it is a map.

$\begin{aligned}
r r^\circ
& = (\pi_1^\circ f \cap \pi_2^\circ g)(f^\circ \pi_1 \cap g^\circ \pi_2^\circ) \\
& \leq \pi_1^\circ f f^\circ \pi_1 \cap \pi_2^\circ g g^\circ \pi_2
& \text{(distrib.)} \\
& \leq \pi_1^\circ \pi_1 \cap \pi_2^\circ \pi_2 \\
& = 1 & \text{(proj'ns tabulate)}
\end{aligned}$

For the unit inequality, we have

$\begin{aligned}
r^\circ r
& = (f^\circ \pi_1 \cap g^\circ \pi_2^\circ) (\pi_1^\circ f \cap \pi_2^\circ g) \\
& = (f^\circ \pi_1 \cap g^\circ \pi_2^\circ) \pi_1^\circ f \cap (f^\circ \pi_1 \cap g^\circ \pi_2^\circ) \pi_2^\circ g\\
& = (f^\circ \cap g^\circ \pi_2^\circ \pi_1) f \cap (f^\circ \pi_1 \pi_2^\circ \cap g^\circ) g
& \text{(mod.)} \\
& = f^\circ f \cap g^\circ g & \text{(dist., proj. tab. top)}\\
& \geq 1 \cap 1 \\
& = 1
\end{aligned}$

The second equality follows from distributivity $(s \cap t) r \leq s r \cap t r$, which is an equality because $r r^\circ \leq 1$.

Revised on November 6, 2012 04:34:14
by Finn Lawler?
(86.41.33.52)