A study of adjunctions: An isomorphic perspective on products
This is the first of a series of posts with which I attempt to organise and interpret the basic definitions and constructions about adjunctions in a way that hopefully tells a story about (some of) the concepts that the definitions and constructions intend to capture.
We start with products, which generalise greatest lower bounds in order theory.
Like other categorical diagrams, the completed diagram above merely captures the typing and equational information in the universal property of products, but the logical interplay of the elements in the diagram is lost. To convey the full meaning of a diagram, it has to be drawn like casting a spell, with the precise statement of the universal property as the incantation — the spell-caster should say the statement/incantation and draw the corresponding parts of the diagram as they’re mentioned. Proficient category theory users should be able to recall the incantation/statement upon seeing the diagram: given two objects $A$ and $B$ in a category $\mathbb C$, an object $A \times B$ together with projection morphisms $\pi_\ell$ and $\pi_r$ is a product of $A$ and $B$ exactly when given every pair of morphisms $f$ and $g$ we can find a unique morphism $\langle f, g \rangle$ such that the diagram above commutes. The $\forall \exists$ pattern gives us a construction packing a pair of morphisms into a single morphism:
$$ \langle \text_ , \text_ \rangle : \forall C.\ \mathbb C (C, A) \times \mathbb C (C, B) \to \mathbb C (C, A \times B) $$
There is another construction in the opposite direction hidden in the final commutativity part of the universal property, namely
$$ \pi \defeq \lambda m.\ (\pi_\ell \cdot m, \pi_r \cdot m) : \forall C.\ \mathbb C (C, A \times B) \to \mathbb C (C, A) \times \mathbb C (C, B) $$
The commutativity part can be seen as saying that $\pi$ is a right inverse of $\langle \text_ , \text_ \rangle$ — we can use $\langle \text_ , \text_ \rangle$ to pack two morphisms into one, which can later be unpacked by $\pi$. The reverse is also true: we can unpack a morphism that goes into a product object, and pack up the resulting pair of morphisms to get back to where we started, because the universal property of products actually says exactly that $\pi$ is bijective (once we spot the presence of $\pi$ in the universal property). This can be seen more clearly in terms of a more abstract lemma.
Lemma. A function $f : X \to Y$ is bijective if and only if for every $y : Y$ there exists a unique $x : X$ such that $f\ x = y$.
The $\forall y.\ \exists x.\ f\ x = y$ part is exactly surjectivity, and the unique existence means that $f\ x = f\ x'$ implies $x = x'$, which is exactly injectivity. Substituting $\pi$ for $f$ (and correspondingly $\mathbb C (C, A \times B)$ for $X$ and $\mathbb C (C, A) \times \mathbb C (C, B)$ for $Y$), the right-hand side of the lemma becomes exactly the universal property of products, and the left-hand side of the lemma gives us a family of isomorphisms
$$ \forall C.\ \mathbb C (C, A) \times \mathbb C (C, B) \cong \mathbb C (C, A \times B) $$
whose forward and backward directions are $\langle \text_ , \text_ \rangle$ and $\pi$ respectively.
The family of isomorphisms tells us that morphisms going into $A \times B$ are interconvertible with pairs of morphisms going into $A$ and $B$, and this is very useful because
- in the forward direction, pairs of morphisms with the same source object can be packed into single morphisms and expressed within the category $\mathbb C$ (and consequently, when we need to represent such pairs of morphisms, we can stay within $\mathbb C$ and don’t necessarily have to move to a different category, namely $\mathbb C \times \mathbb C$), and
- in the backward direction, to reason about morphisms targeting a product object in $\mathbb C$, we can unpack them to pairs of morphisms and reason about these pairs instead, using the richer structure of $\mathbb C \times \mathbb C$.
Notably, the isomorphism formulation helps to explain why there is the uniqueness requirement in the universal property formulation, as the role of the uniqueness requirement is clear when establishing the isomorphisms.
Together with the technique of indirect reasoning (an instance of Yoneda lemma), i.e.,
$$ X \cong Y \quad\Leftrightarrow\quad \forall Z.\ \mathbb C (Z, X) \cong \mathbb C (Z, Y) $$
we can use the family of isomorphisms to establish a range of other isomorphisms about products. For example, to show that $A \times B \cong B \times A$, we can simply reason as follows:
\begin{align*} & \mathbb C (Z, A \times B) \\ \cong~& \reason{product isomorphism} \\ & \mathbb C (Z, A) \times \mathbb C (Z, B) \\ \cong~& \reason{cartesian product} \\ & \mathbb C (Z, B) \times \mathbb C (Z, A) \\ \cong~& \reason{product isomorphism} \\ & \mathbb C (Z, B \times A) \end{align*}
That is, (categorical) products are commutative up to isomorphism simply because cartesian products (on sets) are, and it is because of the isomorphism that we are able to port the property from $\mathbb C \times \mathbb C$ into $\mathbb C$. For larger examples, see Ralf Hinze and Daniel James’s paper ‘Reason isomorphically!’.
In the above I’ve been hinting that the family of isomorphisms is really a bridge between the two categories $\mathbb C \times \mathbb C$ (about pairs of objects and morphisms) and $\mathbb C$ (about single objects and morphisms). Indeed, in the usual formulation that involves the diagonal functor $\Delta : \mathbb C \to \mathbb C \times \mathbb C$ (defined by $\Delta X \defeq (X, X)$ on objects and $\Delta f \defeq (f, f)$ on morphisms) the connection between the two categories becomes more explicit:
$$ \forall C.\ \mathbb C \times \mathbb C (\Delta C, (A, B)) \cong \mathbb C (C, A \times B) $$
Dually, $(\times) : \mathbb C \times \mathbb C \to \mathbb C$ can also be made a functor, and we start to see a general and symmetric form of isomorphisms $\mathbb D (\mathsf F X, Y) \cong \mathbb C (X, \mathsf G Y)$ where $\mathsf F : \mathbb C \to \mathbb D$ and $\mathsf G : \mathbb D \to \mathbb C$. But we’ll save this generalisation for later posts.
Next: 0016 (A study of adjunctions: Galois connections)
