The n-Category Café

So what is a Reedy category anyway? The idea of this paper is to start instead with the question “what is a Reedy model structure?” For a model category $M$ and a Reedy category $C$, then $M^C$ has a model structure in which a map $A\to B$ is

• …a weak equivalence iff $A_x\to B_x$ is a weak equivalence in $M$ for all $x\in C$.
• …a cofibration iff the induced map $A_x \sqcup_{L_x A} L_x B \to B_x$ is a cofibration in $M$ for all $x\in C$.
• …a fibration iff the induced map $A_x \to B_x \times_{M_x B} M_x A$ is a fibration in $M$ for all $x\in C$.

Here $L_x$ and $M_x$ are the latching object and matching object functors, which are defined in terms of the Reedy structure of $C$. However, at the moment all we care about is that if $x$ has degree $n$ (part of the structure of a Reedy category is an ordinal-valued degree function on its objects), then $L_x$ and $M_x$ are functors $M^{C_n} \to M$, where $C_n$ is the full subcategory of $C$ on the objects of degree less than $n$. In the prototypical example of $\Delta^{op}$, where $M^{C}$ is the category of simplicial objects in $M$, $L_n A$ is the “object of degenerate $n$-simplices” whereas $M_n A$ is the “object of simplicial $(n-1)$-spheres (potential boundaries for $n$-simplices)”.

The fundamental observation which makes the Reedy model structure tick is that if we have a diagram $A\in M^{C_n}$, then to extend it to a diagram defined at $x$ as well, it is necessary and sufficient to give an object $A_x$ and a factorization $L_x A \to A_x \to M_x A$ of the canonical map $L_x A \to M_x A$ (and similarly for morphisms of diagrams). For $\Delta^{op}$, this means that if we have a partially defined simplicial object with objects of $k$-simplices for all $k\lt n$, then to extend it with $n$-simplices we have to give an object $A_n$, a map $L_n A \to A_n$ including the degeneracies, and a map $A_n \to M_n A$ assigning the boundary of every simplex, such that the composite $L_n A \to A_n \to M_n A$ assigns the correct boundary to degenerate simplices.

Categorically speaking, this observation can be reformulated as follows. Given a natural transformation $\alpha : F\to G$ between parallel functors $F,G:M\to N$, let us define the bigluing category $Gl(\alpha)$ to be the category of quadruples $(M,N,\phi,\gamma)$ such that $M\in M$, $N\inN$, and $\phi:F M \to N$ and $\gamma : N \to G M$ are a factorization of $\alpha_M$ through $N$. (I call this “bigluing” because if $F$ is constant at the initial object, then it reduces to the comma category $(Id/G)$, which is sometimes called the gluing construction) The above observation is then that $M^{C_x}\simeq Gl(\alpha)$, where $\alpha: L_x \to M_x$ is the canonical map between functors $M^{C_n} \to M$ and $C_x$ is the full subcategory of $C$ on $C_n \cup \{x\}$. Moreover, it is an easy exercise to reformulate the usual construction of the Reedy model structure as a theorem that if $M$ and $N$ are model categories and $F$ and $G$ are left and right Quillen respectively, then $Gl(\alpha)$ inherits a model structure.

Therefore, our answer to the question “what is a Reedy model structure?” is that it is one obtained by repeatedly (perhaps transfinitely) bigluing along a certain kind of transformation between functors $M^C \to M$ (where $C$ is a category playing the role of $C_n$ previously). This motivates us to ask, given $C$, how can we find functors $F,G : M^{C}\to M$ and a map $\alpha : F \to G$ such that $Gl(\alpha)$ is of the form $M^{C'}$ for some new category $C'$?

Of course, we expect $C'$ to be obtained from $C$ by adding one new object “$x$”. Thus, it stands to reason that $F$, $G$, and $\alpha$ will have to specify, among other things, the morphisms from $x$ to objects in $C$, and the morphisms to $x$ from objects of $C$. These two collections of morphisms form diagrams $W:C\to\Set$ and $U:C^{op} \to \Set$, respectively; and given such $U$ and $W$ we do have canonical functors $F$ and $G$, namely the $U$-weighted colimit and the $W$-weighted limit. Moreover, a natural transformation from the $U$-weighted colimit to the $W$-weighted limit can naturally be specified by giving a map $W\times U \to C(-,-)$ in $\Set^{C^{op}\times C}$. In $C'$, this map will supply the composition of morphisms through $x$. (A triple consisting of $U$, $W$, and a map $W\times U \to C(-,-)$ is also known as an object of the Isbell envelope of $C$.)

It remains only to specify the hom-set $C'(x,x)$ (and the relevant composition maps), and for this there is a “universal choice”: we take $C'(x,x) = (W \otimes_C U) \sqcup \{\id_x\}$. That is, we throw in composites of morphisms $x\to y \to x$, freely subject to the associative law, and also an identity morphism. This $C'$ has a universal property (it is a “collage” in the bicategory of profunctors) which ensures that the resulting biglued category is indeed equivalent to $M^{C'}$.

A category with degrees assigned to its objects can be obtained by iterating this construction if and only if any nonidentity morphism between objects of the same degree factors uniquely-up-to-zigzags through an object of strictly lesser degree (i.e. the category of such factorizations is connected). What remains is to ensure that the resulting latching and matching objects are left and right Quillen. It turns out that this is equivalent to requiring that morphisms between objects of different degrees also have connected or empty categories of factorizations through objects of strictly lesser degree.

I call a category satisfying these conditions almost-Reedy. This doesn’t look much like the usual definition of Reedy category, but it turns out to be very close to it. If $C$ is almost-Reedy, let $C_+$ (resp. $C_-$) be the class of morphisms $f:x\to y$ such that $\deg(x)\le \deg(y)$ (resp. $\deg(y)\le \deg(x)$) and that do not factor through any object of strictly lesser degree than $x$ and $y$. Then we can show that just as in a Reedy category, every morphism factors uniquely into a $C_-$-morphism followed by a $C_+$-morphism.

The only thing missing from the usual definition of a Reedy category, therefore, is that $C_-$ and $C_+$ be subcategories, i.e. closed under composition. And indeed, this can fail to be true; but it is all that can go wrong: $C$ is a Reedy category if and only if it is an almost-Reedy category such that $C_-$ and $C_+$ are closed under composition. (In particular, this means that $C_-$ and $C_+$ don’t have to be given as data in the definition of a Reedy category; they are recoverable from the degree function. This was also noticed by Riehl and Verity.)

In other words, the notion of Reedy category (very slightly generalized) is essentially inevitable. Moreover, as often happens, once we understand a definition more conceptually, it is easier to generalize further. The same analysis can be repeated in other contexts, yielding the existing notions of generalized Reedy category and enriched Reedy category, as well as new generalizations such as a combined notion of “enriched generalized Reedy category”.

(I should note that some of the ideas in this paper were noticed independently, and somewhat earlier, by Richard Garner. He also pointed out that the bigluing model structure is a special case of the “Grothendieck construction” for model categories.)

This paper is, I think, slightly unusual, for a paper in category theory, in that one of its main results (unique $C_+$-$C_-$-factorization in an almost-Reedy category) depends on a sequence of technical lemmas, and as far as I know there is no particular reason to expect it to be true. This made me worry that I’d made a mistake somewhere in one of the technical lemmas that might bring the whole theorem crashing down. After I finished writing the paper, I thought this made it a good candidate for an experiment in computer formalization of some non-HoTT mathematics.

Verifying all the results of the paper would have required a substantial library of basic category theory, but fortunately the proof in question (including the technical lemmas) is largely elementary, requiring little more than the definition of a category. However, formalizing it nevertheless turned out to be much more time-consuming that I had hoped, and as a result I’m posting this paper quite some months later than I might otherwise have. But the result I was worried about turned out to be correct (here is the Coq code, which unlike the HoTT Coq library requires only a standard Coq v8.4 install), and now I’m much more confident in it. So was it worth it? Would I choose to do it again if I knew how much work it would turn out to be? I’m not sure.

Having this formalization does provide an opportunity for another interesting experiment. As I said, the theorem turned out to be correct; but the process of formalization did uncover a few minor errors, which I corrected before posting the paper. I wonder, would those errors have been caught by a human referee? And you can help answer that question! I’ve posted a version without these corrections, so you can read it yourself and look for the mistakes. The place to look is Theorem 7.16, its generalization Theorem 8.26, and the sequences of lemmas leading up to them (starting with Lemmas 7.12 and 8.15). The corrected version that I linked to up top mentions all the errors at the end, so you can see how many of them you caught — then post your results in the comments! You do, of course, have the advantage over an ordinary referee that I’m telling you there is at least one error to find.

Of course, you can also try to think of an easier proof, or a conceptual reason why this theorem ought to be true. If you find one (or both), I will be both happy (for obvious reasons) and sad (because of all the time I wasted…).

Let me end by mentioning one other thing I particularly enjoyed about this paper: it uses two bits of very pure category theory in its attempt to explain an apparently ad hoc definition from homotopy theory.

The first of these bits is “tight lax colimits of diagrams of profunctors”. It so happens that an object $(U,W,\alpha)$ of the Isbell envelope can also be regarded as a special sort of lax diagram in $Prof$, and the category $C'$ constructed from it is its lax colimit. Moreover, the universal property of this lax colimit — or more precisely, its stronger universal property as a “tight colimit” in the equipment $Prof$ — is precisely what we need in order to conclude that $M^{C'}$ is the desired bigluing category.

The second of these bits is an absolute coequalizer that is not split. The characterization of non-split absolute coequalizers seemed like a fairly esoteric and very pure bit of category theory when I first learned it. I don’t, of course, mean this in any derogatory way; I just didn’t expect to ever need to use it in an application to, say, homotopy theory. But it turned out to be exactly what I needed at one point in this paper, to “enrich” an argument involving a two-step zigzag (whose unenriched version I learned from Riehl-Verity).