Finn Lawler allegory (Rev #3, changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Recall the notion of a unitary pre-tabular allegory. Bicategories of relations are equivalent, but this has yet to be shown ~~rigorously,~~ 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.