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
for and (where ), with composition induced by composition of maps .
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. hen 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.