Previously we were exploring universal constructions for products, coproducts, and exponentials. In particular, we were able to prove the distributive law:

The power of this law is that it relates the mapping-in universal construction (product on the left) with the mapping-out one (coproduct on the right). If you take into account that products and coproducts are just special cases of limits and colimits, you may ask a more general question: under what conditions limits commute with colimits. In a cartesian closed category a product of sums is not equal to the sum of products:

So, in general, products don’t commute with coproducts. But if you replace coproducts with a special kind of colimits, then it can be shown that:

**Theorem.**

In , filtered colimits commute with finite limits.

In this post I’ll try to explain these terms and provide some intuition why it works and how filtered colimits are related to the more traditional notion of limits that we know from calculus.

# Limits

Let’s start with limits. They are like products, except that, instead of just two objects at the bottom, you have any number of objects plus a bunch of morphisms between them. That’s called a diagram. Then you have an apex with arrows going down to all the objects in the diagram; and you get what is called a cone. If you have morphisms in your diagram, they form triangles. These triangles must commute. For instance, in Fig 1, we have:

This means that not all projections are independent–that you may obtain one projection from another by post-composing it with a morphism from the diagram. In Fig 1, for instance, you may extract a value of either directly using or by applying to the result of .

A limit is defined as the universal cone with the apex . It means that, if you have any other cone with some apex , built over the same diagram, there is a unique morphism from to that makes all the triangles commute. For instance, in Fig 2, one of the commuting conditions is:

and so on. We’ve seen similar commuting conditions in the definition of the product.

If you think of in this example as a data structure, you would implement it as a product of , , and , together with two functions:

But because of the commuting conditions, the three values stored in cannot be independent. If you pick a value for , then the values for and are uniquely determined.

A limit, just like a product, is defined by a mapping-in property. If you want to define a morphism from some to , you need to provide three morphisms , , and . However, unlike in the case of a product, these morphisms must satisfy some commuting conditions. Here, must be equal to and . So, really, you only need to define , and that uniquely determines . This is why the cones in Fig 2 can be simplified, as shown in Fig 3.

Notice that the diagram essentially forms a subcategory inside the category , even if we don’t explicitly draw all the identity morphisms or all the compositions. This is because triangles built by composing commuting triangles are again commuting. It therefore makes sense to define a diagram as a functor from an (often much smaller) index category to . In our case it would be a category with just three objects, , , , and two non-identity morphisms. (The diagram category for the product is even simpler: just two objects, no non-trivial morphisms.)

The properties of the diagram category determine the nature of cones and the nature of the limits. For instance, functors from a finite category will produce *finite limits*.

The diagram category in our example has a very peculiar property: it has a cone for every pair of objects (it’s a cone inside , not to be confused with the cone in ). For instance, the pair , is part of the cone with the apex . This is also the apex for the (somewhat degenerate) cone based on and (with or without the connecting morphism). A category in which there is a cone for every finite subdiagram is called *cofiltered*. Limits defined by functors from cofiltered categories are called *cofiltered limits*.

The intuition is that cofiltered categories exhibit some kind of ordering. You may think of as a lower bound of and . Following these bounds, you might eventually get to some kind of roots–here it’s the object –and these roots will dictate the behavior of cones and the behavior of limits. Things get really interesting when the diagram category is infinite, because then there is no guarantee that you’ll ever reach a root. There is, for instance, no smallest (negative) integer, even though integers are ordered. You can begin to see parallels with traditional limits, like:

That’s where these ideas originally came from.

Limits in the category of sets have a particularly simple interpretation. In , we can use functions from the terminal object–the singleton set–to pick individual set elements.

For every selection in Fig 5. of , , there is a unique that picks an element in . But a selection of , , is nothing but a cone with the apex . So there is a one-to-one correspondence between elements of and such cones. In other words, is a *set of apex-1 cones*.

# Colimits

Colimits are dual to limits–you get them by inverting all the arrows. So, instead of projections, you get injections, and the universal condition defines a *mapping out* of a colimit (see Fig 6).

If you look at the colimit as a data structure, it is similar to a coproduct, except that not all the injections are independent. In the example in Fig 6, and are determined by pre-composing with and , respectively. It’s not clear how to implement a colimit in Haskell, so here’s a pseudo-Haskell attempt using imaginary dependent-type syntax:

data Colim a1 a2 a3 (g2 :: a2 -> a1) (g3 :: a3 -> a1) = = A1 a1 | A2 a2 | A3 a3

To deconstruct this colimit, you only need to provide one function .

h :: (a1 -> c) -> Colim a1 a2 a3 g2 g3 -> c h f1 (A1 a1) = f1 a1 h f1 (A2 a2) = f1 (g2 a2) h f1 (A3 a3) = f1 (g3 a3)

Granted, in a lazy language like Haskell, this would be an overkill way to store essentially just one value.

A colimit in the category of sets simplifies to a disjoint union of sets, in which some elements are identified. Suppose that the colimit is defined by some diagram category and a functor . Each object in produces a set .

The disjoint union of all these sets is a set whose elements are the pairs where . (Notice that the sets may overlap, but each element from the overlap will be counted as many times as the number of sets it belongs to.) Coproduct injections are then functions that take an element and map it into an element . But that doesn’t take into account the presence of morphisms in the diagram. These morphisms are mapped to functions between corresponding sets. For instance, in Fig 7, we can take an element . It is injected, using , as an element . But there is another path from that uses followed by . That produces . If the triangle is to commute, these two must be equal. So in the actual colimit, they must be identified. In general, any two elements of the disjoint union that satisfy this relation:

must be identified. This is not an equivalence relation, but it can be extended to one (by first symmetrizing it, and then making it transitive again). A colimit is then a quotient of the disjoint union by this equivalence.

As before, I chose this example to illustrate a special type of a diagram. This is a diagram that can be obtained using a functor from a *filtered* category. A filtered category has this property that for any finite subdiagram, there is a cocone under it. Here, for instance, the subdiagram formed by and has a cocone with the apex . Again, you may think of as a kind of upper bound of and . If the filtered category is finite, following upper bounds will eventually lead you to some roots. And in Set, the equivalence relation will allow you shift all the elements down to those roots. But in an infinite case (think natural numbers) there may be no largest element–no root. And that brings filtered colimits closer to the intuition we have for limits in calculus. In fact, all the interesting filtered colimits are based on infinite diagrams.

# Commuting Limits and Colimits

What does it mean for a limit to commute with a colimit? A single colimit is generated by a functor from some index category . What we need is a bunch of such colimits so that we can take a limit over those. Therefore we need a bunch of functors . Moreover, those colimits have to form a diagram. So we need another index category to parameterize those functors. Altogether, we need a functor of two arguments:

It follows that, for any given in we have a functor . We can take a colimit of that. Then we gather those colimits into a diagram whose shape is defined by , and then take its limit. We get:

Alternatively, when we fix some in , we get a functor . We can take a limit of that. Then we can gather all those limits and form a diagram whose shape is defined by . Finally we can take a colimit of that:

It’s not difficult to construct the mapping:

using the universal property, since the colimit has the mapping-out property. It’s the other way around that’s tricky. But it always works in the special case when is filtered, is finite, and is .

Here’s the sketch of this amazing proof, which you can find in Saunders Mac Lane’s *Categories for the Working Mathematician*.

Since the target of the functor is Set, it might help to visualize its image as a rectangular array of sets. A fixed picks up a row of such sets, whereas a fixed picks up a column. Because we are dealing with sets, we can try to define the mapping:

pointwise. Let’s pick an element of the limit on the left. As we’ve established earlier, a limit in Set is a set of apex-1 cones. So let’s pick one such cone. It’s just a selection of elements from a bunch of colimits.

As we’ve seen before, a colimit in Set is a discriminated union with some identifications. So our apex-1 cone will pick a set of representatives, one per colimit, say . Any time there is a morphism , we can replace one representative with another . The intuition is that we can slide the representatives horizontally within each row along morphisms.

If is a filtered category, then for any finite number of objects , we can always find a common root (it will be the apex of a cocone formed by in ). So we can slide all the representatives to a single column. In other words, our cone can be brought to a set of representatives , with a common .

But that’s just a cone over . It’s an element of . And we can inject it into a colimit over to get an element of . We have thus defined our mapping.

# Conclusion

If you didn’t get the proof the first time, don’t get discouraged. Take a break, sleep over it, and then read it slowly again. Make sure you have internalized all the definitions. Draw your own pictures. The two major tricks are: (1) visualizing an element of a limit as a cone originating from the singleton set, and (2) the idea of sliding the elements of multiple colimits to a common column.

The importance of this theorem is that it tells you when and how you can define mappings out of limits. For instance, how to define functions from a product or from an end.

# Acknowledgment

I’m grateful to Derek Elkins for correcting mistakes in the original version of this post.

December 10, 2019 at 7:58 am

[…] Перевод статьи Бартоша Милевски «Filtered Colimits» (исходный текст расположен по адресу — Текст оригинальной статьи). […]