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 file$\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 \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$

The following lemma is used at allegory.

Proof Lemma

Let If r = \pi_1^\circ f \cap \colon \pi_2^\circ X g \to A . Then and \pi_1 g r \colon = X f \to B and are maps in a unitary pre-tabular allegory, then \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 = \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$.

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$.

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