Finn Lawler
allegory (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

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 This PDF fileA\mathbf{A} gives an explicit argument, which I put at be a unitary pre-tabular allegory.bicategory of relations until Mike Shulman suggested the neater proof that’s there now. But I’ll keep this here anyway.

Lemma

If f:XAf \colon X \to A and g:XBg \colon X \to B are maps, then f,g=π 1 fπ 2 g\langle f, g \rangle = \pi_1^\circ f \cap \pi_2^\circ g

The following lemma is used at allegory.

Proof Lemma

Let Ifr=π 1 f :π 2 XgA r = \pi_1^\circ f \cap \colon \pi_2^\circ X g \to A . Then andπ 1gr:=XfB \pi_1 g r \colon = X f \to B and are maps in a unitary pre-tabular allegory, thenπ 2 r f,g=π 1 fπ 2 g \pi_2 \langle r f, g \rangle = \pi_1^\circ f \cap \pi_2^\circ 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.

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.

Last revised on November 6, 2012 at 04:34:14. See the history of this page for a list of all contributions to it.