## June 29, 2015

### What is a Reedy Category?

#### Posted by Mike Shulman I’ve just posted the following preprint, which has apparently quite little to do with homotopy type theory.

The notion of Reedy category is common and useful in homotopy theory; but from a category-theoretic point of view it is odd-looking. This paper suggests a category-theoretic understanding of Reedy categories, which I find more satisfying than any other I’ve seen.

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).

Posted at June 29, 2015 6:33 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2835

### Re: What is a Reedy Category?

If Reedy categories can be built by an iterative process, then is there any hope of completely classifying them? Or at least of classifying the finite ones, or those of finite “rank” (where the degree function takes values in a finite ordinal), or those which can be obtained by finitely many iterations of the building process? It should at least be a good exercise to look at the first few steps of this process.

Let’s see. The empty category is the only Reedy category whose degrees take values in the ordinal 0. Discrete categories are the only Reedy categories whose degrees take values in the ordinal 1.

To adjoin an object $\ast \,\,\,$ to the terminal category $\{\cdot\}$, we pick a set $W = \mathrm{Hom}(\ast,\cdot)$ and a set $U = \mathrm{Hom}(\cdot,\ast)$. There is only one function $U \times W \to \mathrm{Hom}(\cdot,\cdot) = 1$. Now, in Mike’s formula, we have $\mathrm{Hom}(\ast,\ast) = W\otimes U \amalg \{1_\ast\}$, which I think means $\int^{\cdot \in \{\cdot\}} W(\cdot) \times U(\cdot) \amalg \{1_\ast\}$, which of course is just $W \times U \amalg \{1_\ast\}$. This makes sense – every nonidentity arrow $\ast \to \ast$ is named after its factorization through $\cdot\,\,\,$. The two-object discrete category comes from taking $W=U=\emptyset$, the walking arrow from $W=1,U=\emptyset$ or vice versa, the walking isomorphism from $W=U=1$, the opposite of the site for reflexive graphs / walking reflexive coequalizer comes from $W=2,U=1$ (unless I’ve mixed up my opposites), etc.

To go past this rudimentary level in a systematic way seems difficult though. I suppose it might be more fruitful to study the category of Reedy categories. What is a good choice of morphisms? Functors which induce Quillen functors on all diagram categories? If that’s the case, then there are really left and right morphisms, and we probably have a double category.

Posted by: Tim Campion on June 30, 2015 9:58 PM | Permalink | Reply to this

### Re: What is a Reedy Category?

CW complexes are also built up “iteratively” if you like, and we can consider finite complexes and finite-dimensional complexes… and classifying them this way is a remarkably interesting problem!

Posted by: Jesse C. McKeown on June 30, 2015 11:07 PM | Permalink | Reply to this

### Re: What is a Reedy Category?

Posted by: Zhen Lin on June 30, 2015 11:28 PM | Permalink | Reply to this

### Re: What is a Reedy Category?

$W=U=1$ actually gives you the walking retraction; $1_\ast$ is never equal to the composite of a $W$-arrow with a $U$-arrow.

I haven’t thought about morphisms at all. I suppose by analogy with the CW case one could consider “cellular” morphisms. I wonder whether Reedy categories are the algebraically cofibrant objects for some awfs?

Posted by: Mike Shulman on July 1, 2015 4:31 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

Mike, would you say you’ve pinned down the minimal (or a minimal) set of requirements on $C$ so that $M^C$ is a model category, for arbitrary model categories $M$? Clearly if $M$ is particularly nice, less might be required.

Posted by: David Roberts on July 1, 2015 1:25 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

I hope that I’ve pinned down the minimal requirements on $C$ so that every $M^C$ is a model category in a particular way, namely the Reedy way. It’s possible there is some other way to put a model structure on arbitrary diagram categories.

Posted by: Mike Shulman on July 1, 2015 4:33 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

Whoops, that’s what I should have said. Or to put it another way, the requirements such that a Reedy model structure exists…

Posted by: David Roberts on July 1, 2015 5:49 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

What would you estimate the de Bruijn factor of your proof to be?

Posted by: David Roberts on July 7, 2015 4:24 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

Interesting question! It looks like something between 2.2 and 5.6, depending on how much of the paper one considers to be part of a “TeX encoding” of the theorem in question. (E.g. does it include all the general-purpose macro definitions that I \input into all my papers?)

Posted by: Mike Shulman on July 7, 2015 6:42 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

I’ve seen your preamble, but I didn’t think it was that long! I would say leave it out, since it should be a constant factor over future writing on the topic.

I find this a convincing piece of evidence (I would even say hard evidence) that MLTT/Coq is much, much closer to homotopical practice than ZFC/Automath/Mizar, given that the dB factors of the pages and sections of (non-logical) textbook mathematics on the page I linked are in the range 3.1-8.8 (leaving out the elementary computational number theory example).

Posted by: David Roberts on July 7, 2015 8:32 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

How does Mike’s dB factor provide an unequivocally favorable comparison of HoTT/Coq to ZFC/Automath/etc, considering that 2.2-5.8 is very much in the typical range for ZFC/etc that we see on that page?

Posted by: John Huerta on July 7, 2015 3:52 PM | Permalink | Reply to this

### Re: What is a Reedy Category?

Hi John,

if you look at the level of mathematics formalised in that page of examples, they are a long way from serious homotopy theory or category theory. I have no idea what it would take to formalise what Mike did in Mizar/etc, but I would guess it would be much more difficult.

As I said on the fom mailing list some months back, I’d like to see the comparison between a formal proof in Mizar/etc of the version of Blaker-Massey that works for all $\infty$-toposes, and the one in Coq. This is much more HoTT than Mike’s theorem…

Posted by: David Roberts on July 8, 2015 6:28 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

Actually, it’s not clear to me that formalizing this theorem would be much harder in any other proof assistant. I haven’t actually used Mizar, but as I said, this theorem is really quite elementary. I suppose I did benefit a little from the theory of well-founded induction in the Coq standard library, but Mizar has a very extensive library too, which might have an analogous theory that could be used.

I’d like to see the comparison between a formal proof in Mizar/etc of the version of Blaker-Massey that works for all ∞-toposes, and the one in Coq.

If by that you mean to formalize in Mizar/etc. a theorem like “Blaker-Massey holds in all ∞-toposes”, then that would be an unfair comparison. To make it fair you’d have to also include on the Coq side a formal proof that all ∞-toposes model HoTT — which isn’t really even known at an informal level yet!

Posted by: Mike Shulman on July 8, 2015 8:21 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

Hmm, ok. Getting a bit overzealous there :-)

Even a formal proof of ordinary B-M would be good to see, for comparison’s sake. Though I guess you’d say one would have to also formally prove that simplicial sets and/or spaces give a model of UF/HoTT to make a proper comparison. This would be where, I hope, VV’s recent work on the mathematics of type theory comes to the rescue.

Posted by: David Roberts on July 9, 2015 5:57 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

There I do think it gets a bit more questionable as to what exactly should be compared to what. It’s hard to compare apples to apples if apples only exist on one side of the equation.

Posted by: Mike Shulman on July 9, 2015 7:57 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

It’s hard to compare apples to apples if apples only exist on one side of the equation.

I agree with that. At some point, once will hopefully be able to say “well, I proved it in HoTT/UF/etc, the onus is on you ZFC-theorists, to model my foundational theory, not the other way around”. However, this smacks of mathematicians “adopting a new foundation” as Michael Harris keeps mentioning (I just finished his book, phew…), which I don’t think is going to happen in practice, because they are, IRL, like, mumblemumbleZFCmumble.

Posted by: David Roberts on July 9, 2015 1:46 PM | Permalink | Reply to this

### Re: What is a Reedy Category?

While I sympathize to some extent, I do think it is remarks like that which unnecessarily damage the image of HoTT/UF among the Michael Harrises of the world.

Posted by: Mike Shulman on July 9, 2015 5:47 PM | Permalink | Reply to this

### Re: What is a Reedy Category?

remarks like that

sorry, which remark? The not so subtle slur on mathematicians’ general blindness to foundations? It’s something that eg Friedman and others on the fom list mention regularly, albeit usually complaining that people don’t realise how pervasive undecidability is among what he claims is ‘ordinary mathematics’ (graphs internal to ordered sets with vertices the rationals, anyone?) Or the ‘onus is on you’ bit? (a bit blunt, yes)

I would be happy if mathematicians as a whole realised that what most of them do is foundations agnostic, as far as mere provability/encodability goes, but there are are foundations closer or further to what they do – and that one can pick the most convenient. Clearly a set theorist isn’t going to work with well-founded trees in a model of ETCS, and an algebraic geometer might as well work over a base topos modelling a structural set theory. I’m not sure what Harris envisages when he discusses the potential for everyone to adopt HoTT or similar new foundational system.

Posted by: David Roberts on July 10, 2015 5:29 AM | Permalink | Reply to this

### Re: What is a Reedy Category?

I meant to refer to your whole comment, but particularly the “onus” part. I definitely agree with

I would be happy if mathematicians as a whole realised that what most of them do is foundations agnostic, as far as mere provability/encodability goes, but there are are foundations closer or further to what they do – and that one can pick the most convenient.

but in that case I think there’s no reason that establishing the connenction between HoTT/UF and ZFC should be the job of ZFC-theorists rather than HoTT-theorists.

Posted by: Mike Shulman on July 10, 2015 6:09 PM | Permalink | Reply to this

### Re: What is a Reedy Category?

It’s not so much that the preamble is long, as that the excerpt in question from the paper is quite short. It’s probably not really a correct calculation anyway, because if I were writing a paper only about that theorem, I’d still need some of the introductory material that I cut out. Feel free to get the TeX source from the arXiv and decide for yourself how much should be included. (-:

Leaving out the preamble leads to the calculation of 5.6, which is squarely in the range 3.1-8.8 you quoted, and greater than most of them which are in the 3–4.5 range. So I don’t see why this is any evidence in favor of MLTT/Coq. And, as I said, there’s nothing very particularly HoTT about this formalization. I’d be more interested in computing the dB factor of the HoTT Book, once it’s completely formalized.

Posted by: Mike Shulman on July 7, 2015 2:31 PM | Permalink | Reply to this

Post a New Comment