The first and second corollary below are well-known category theory lemmas. We give a slightly different argument than usual (i.e. we took a trivial result and changed it into something much more complicated).
Here is a lovely little definition:
Definition. Given a small diagram of sets, write
for the small category with
and morphisms
for and
(where
), with composition induced by composition of maps
.
Note that by the Yoneda lemma, this category is isomorphic (not just equivalent!) to , where
is the Yoneda embedding. Indeed,
are in bijection with natural transformations
, and morphisms
correspond to a morphism
rendering commutative the associated diagram
Example 1. If , then a diagram
is a pair of sets
with parallel arrows
. Then
looks like a ‘bipartite preorder’ where every source object has outgoing valence
:
Example 2. Given a set , write
for the discrete category on
, i.e.
and
If is itself a discrete category, then
is just a collection
of sets, and
Remark. Giving a functor is the same thing as giving functors
and natural transformations
of functors for all
in
, such that
for all in
(where
denotes horizontal composition of natural transformations, as in Tag 003G).
Example 3. Let be a small category, and consider the diagram
given by the source and target maps
. Then we have a functor
given on objects by
and on morphisms by
In terms of the remark above, it is given by the functors taking
to
and the natural inclusion
, along with the natural transformations
We can now formulate the main result.
Lemma. Let be a small category. Then the functor
of Example 3 is cofinal.
Recall that a functor is cofinal if for all
, the comma category
is nonemptry and connected. See also Tag 04E6 for a concrete translation of this definition.
Proof. Let . Since
, the identity
gives the object
in
, showing nonemptyness. For connectedness, it suffices to connect any
(i.e.
) to the identity
) (i.e.
). If
, then the commutative diagram
gives a zigzag
of morphisms in connecting
to
. If instead
, we can skip the first step, and the diagram
gives a zigzag
connecting to
.
Corollary 1. Let be a small diagram in a category
with small products. Then there is a canonical isomorphism
provided that either side exists.
Proof. By the lemma, the functor
is initial. Hence by Tag 002R, the natural morphism
is an isomorphism if either side exists. But is a category as in Example 1, and it’s easy to see that the limit over a diagram
is computed as the equaliser of a pair of arrows between the products.
Of course this is not an improvement of the traditional proof, because the “it’s easy to see” step at the end is very close to the same statement as the corollary in the special case where is of the form
for some
. But it’s fun to move the argument almost entirely away from limits and into the index category.
Corollary 2. Let be a category that has small products and equalisers of parallel pairs of arrows. Then
is (small) complete.