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:XAf \colon X \to A and g:XBg \colon X \to B are maps in a unitary pre-tabular allegory, then f,g=π 1 fπ 2 g\langle f, g \rangle = \pi_1^\circ f \cap \pi_2^\circ g

Proof

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

rr =(π 1 fπ 2 g)(f π 1g π 2 ) π 1 ff π 1π 2 gg π 2 (distrib.) π 1 π 1π 2 π 2 =1 (proj'ns tabulate) \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

r r =(f π 1g π 2 )(π 1 fπ 2 g) =(f π 1g π 2 )π 1 f(f π 1g π 2 )π 2 g =(f g π 2 π 1)f(f π 1π 2 g )g (mod.) =f fg g (dist., proj. tab. top) 11 =1 \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 (st)rsrtr(s \cap t) r \leq s r \cap t r, which is an equality because rr 1r r^\circ \leq 1.

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