Finn Lawler 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.

Lemma

If $f:X\to A$ and $g:X\to B$ are maps in a unitary pre-tabular allegory, then $⟨f,g⟩={\pi }_{1}^{\circ }f\cap {\pi }_{2}^{\circ }g$

Proof

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=⟨f,g⟩$ if and only if it is a map.

$\begin{array}{rl}r{r}^{\circ }& =\left({\pi }_{1}^{\circ }f\cap {\pi }_{2}^{\circ }g\right)\left({f}^{\circ }{\pi }_{1}\cap {g}^{\circ }{\pi }_{2}^{\circ }\right)\\ & \le {\pi }_{1}^{\circ }f{f}^{\circ }{\pi }_{1}\cap {\pi }_{2}^{\circ }g{g}^{\circ }{\pi }_{2}& \text{(distrib.)}\\ & \le {\pi }_{1}^{\circ }{\pi }_{1}\cap {\pi }_{2}^{\circ }{\pi }_{2}\\ & =1& \text{(proj'ns tabulate)}\end{array}$\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{array}{rl}{r}^{\circ }r& =\left({f}^{\circ }{\pi }_{1}\cap {g}^{\circ }{\pi }_{2}^{\circ }\right)\left({\pi }_{1}^{\circ }f\cap {\pi }_{2}^{\circ }g\right)\\ & =\left({f}^{\circ }{\pi }_{1}\cap {g}^{\circ }{\pi }_{2}^{\circ }\right){\pi }_{1}^{\circ }f\cap \left({f}^{\circ }{\pi }_{1}\cap {g}^{\circ }{\pi }_{2}^{\circ }\right){\pi }_{2}^{\circ }g\\ & =\left({f}^{\circ }\cap {g}^{\circ }{\pi }_{2}^{\circ }{\pi }_{1}\right)f\cap \left({f}^{\circ }{\pi }_{1}{\pi }_{2}^{\circ }\cap {g}^{\circ }\right)g& \text{(mod.)}\\ & ={f}^{\circ }f\cap {g}^{\circ }g& \text{(dist., proj. tab. top)}\\ & \ge 1\cap 1\\ & =1\end{array}$\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 $\left(s\cap t\right)r\le sr\cap tr$, which is an equality because $r{r}^{\circ }\le 1$.

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