Coincidence of Products and Coproducts in Rel
I've seen a lot of times that categorical products and coproducts coincide in Rel, and it seems that I should formally work it out at least once. The exercise description below is taken from Bird, Gibbons, and Mu, adapted to the style of AoP:
A straightforward interpretation in Rel of the standard theory of datatypes from Chapter 5 (about functional derivation) is inappropriate: products and coproducts coincide, whereas we intend them to be different constructions. Technically, this is because Rel is its own dual, whereas Set and Cpo are not self-dual.
Categorically speaking, bifunctor
⊗
is a product if arrowsf : B ← A
andg : C ← A
uniquely determine a morphismh : B ⊗ C ← A
withoutl . h = f
andoutr . h = g
. Dually, bifunctor⊕
is a coproduct if arrowsf : C ← A
andg : C ← B
uniquely determine a morphismh : C ← A ⊕ B
withh . inl = f
andh . inr = g
.(a) Show that cartesian product is not a categorical product in Rel.
(b) Show that disjoint sum is a categorical coproduct in Rel.
(c) Show that disjoint sum is in fact also a categorical product in Rel.
(d) Show, using converses, that any categorical product in Rel is necessarily a coproduct, and vice versa.
Cartesian product is not a categorical product since partiality emerges in Rel. For example, taking f = ∅
and g = id
, we have
split f g = ∅and now the cancellation law fails to hold:
outl . split f g = ∅ ≠ id = gDisjoint sum is, however, still a categorical coproduct, which can be easily verified by the definitions of relation composition and join.
Now we have coproducts in Rel. To show that products and coproducts coincide, we define <f, g> = [fº, gº]º
, outl = inlº
, outr = inrº
and reason:
(The proof actually starts in the middle and goes dually towards the top and the bottom.) The arrow <fº, gº>
has type B + C ← A
if fº : B ← A
and gº : C ← A
and is unique since [f, g]
is. Therefore a coproduct in Rel is also a product and vice versa. In particular, disjoint sum is both a product and a coproduct. One can easily see that it is converse which makes Rel dual to itself and causes the coincidence.
--
Why am I feeling that the logic is a bit strange...?
<< 回到主頁