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 ← Aandg : C ← Auniquely determine a morphismh : B ⊗ C ← Awithoutl . h = fandoutr . h = g. Dually, bifunctor⊕is a coproduct if arrowsf : C ← Aandg : C ← Buniquely determine a morphismh : C ← A ⊕ Bwithh . inl = fandh . 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...?



<< 回到主頁