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 : X → A f \colon X \to A and g : X → B g \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 ∘ g r = \pi_1^\circ f \cap \pi_2^\circ g . Then π 1 r = f \pi_1 r = f and π 2 r = g \pi_2 r = g , by the modular law and the fact that projections tabulate top elements. So r = ⟨ f , g ⟩ r = \langle f, g \rangle if and only if it is a map.
r r ∘ = ( π 1 ∘ f ∩ π 2 ∘ g ) ( f ∘ π 1 ∩ g ∘ π 2 ∘ ) ≤ π 1 ∘ f f ∘ π 1 ∩ π 2 ∘ g g ∘ π 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 ∘ π 1 ∩ g ∘ π 2 ∘ ) ( π 1 ∘ f ∩ π 2 ∘ g ) = ( f ∘ π 1 ∩ g ∘ π 2 ∘ ) π 1 ∘ f ∩ ( f ∘ π 1 ∩ g ∘ π 2 ∘ ) π 2 ∘ g = ( f ∘ ∩ g ∘ π 2 ∘ π 1 ) f ∩ ( f ∘ π 1 π 2 ∘ ∩ g ∘ ) g (mod.) = f ∘ f ∩ g ∘ g (dist., proj. tab. top) ≥ 1 ∩ 1 = 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 ( s ∩ t ) r ≤ s r ∩ t r (s \cap t) r \leq s r \cap t r , which is an equality because r r ∘ ≤ 1 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.