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 A \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 : X → A f \colon X \to A g : X → B g \colon X \to B ⟨ 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 If r = π 1 ∘ f ∩ : π 2 ∘ X g → A r = \pi_1^\circ f \cap \colon \pi_2^\circ X g \to A . Then and π 1 g r : = X f → B \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 , 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 r r ∘ ≤ 1 r r^\circ \leq 1
Proof
Let r = π 1 ∘ f ∩ π 2 ∘ g r = \pi_1^\circ f \cap \pi_2^\circ g π 1 r = f \pi_1 r = f π 2 r = g \pi_2 r = g r = ⟨ f , g ⟩ r = \langle f, g \rangle
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 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.