Finn Lawler allegory (Rev #3)

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 makes precise the argument at bicategory of relations.

Let $\mathbf{A}$ be a unitary pre-tabular allegory.

Lemma

If $f \colon X \to A$ and $g \colon X \to B$ are maps, then $\langle f, g \rangle = \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 = \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$ .

Revision on November 4, 2012 at 03:56:29 by Finn Lawler?. See the history of this page for a list of all contributions to it.