Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

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 MM and a Reedy category CC, then M CM^C has a model structure in which a map ABA\to B is

  • …a weak equivalence iff A xB xA_x\to B_x is a weak equivalence in MM for all xCx\in C.
  • …a cofibration iff the induced map A x L xAL xBB xA_x \sqcup_{L_x A} L_x B \to B_x is a cofibration in MM for all xCx\in C.
  • …a fibration iff the induced map A xB x× M xBM xAA_x \to B_x \times_{M_x B} M_x A is a fibration in MM for all xCx\in C.

Here L xL_x and M xM_x are the latching object and matching object functors, which are defined in terms of the Reedy structure of CC. However, at the moment all we care about is that if xx has degree nn (part of the structure of a Reedy category is an ordinal-valued degree function on its objects), then L xL_x and M xM_x are functors M C nMM^{C_n} \to M, where C nC_n is the full subcategory of CC on the objects of degree less than nn. In the prototypical example of Δ op\Delta^{op}, where M CM^{C} is the category of simplicial objects in MM, L nAL_n A is the “object of degenerate nn-simplices” whereas M nAM_n A is the “object of simplicial (n1)(n-1)-spheres (potential boundaries for nn-simplices)”.

The fundamental observation which makes the Reedy model structure tick is that if we have a diagram AM C nA\in M^{C_n}, then to extend it to a diagram defined at xx as well, it is necessary and sufficient to give an object A xA_x and a factorization L xAA xM xAL_x A \to A_x \to M_x A of the canonical map L xAM xAL_x A \to M_x A (and similarly for morphisms of diagrams). For Δ op\Delta^{op}, this means that if we have a partially defined simplicial object with objects of kk-simplices for all k<nk\lt n, then to extend it with nn-simplices we have to give an object A nA_n, a map L nAA nL_n A \to A_n including the degeneracies, and a map A nM nAA_n \to M_n A assigning the boundary of every simplex, such that the composite L nAA nM nAL_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 α:FG\alpha : F\to G between parallel functors F,G:MNF,G:M\to N, let us define the bigluing category Gl(α)Gl(\alpha) to be the category of quadruples (M,N,ϕ,γ)(M,N,\phi,\gamma) such that MMM\in M, NinNN\inN, and ϕ:FMN\phi:F M \to N and γ:NGM\gamma : N \to G M are a factorization of α M\alpha_M through NN. (I call this “bigluing” because if FF is constant at the initial object, then it reduces to the comma category (Id/G)(Id/G), which is sometimes called the gluing construction) The above observation is then that M C xGl(α)M^{C_x}\simeq Gl(\alpha), where α:L xM x\alpha: L_x \to M_x is the canonical map between functors M C nMM^{C_n} \to M and C xC_x is the full subcategory of CC on C n{x}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 MM and NN are model categories and FF and GG are left and right Quillen respectively, then Gl(α)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 CMM^C \to M (where CC is a category playing the role of C nC_n previously). This motivates us to ask, given CC, how can we find functors F,G:M CMF,G : M^{C}\to M and a map α:FG\alpha : F \to G such that Gl(α)Gl(\alpha) is of the form M CM^{C'} for some new category CC'?

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

It remains only to specify the hom-set C(x,x)C'(x,x) (and the relevant composition maps), and for this there is a “universal choice”: we take C(x,x)=(W CU){id x}C'(x,x) = (W \otimes_C U) \sqcup \{\id_x\}. That is, we throw in composites of morphisms xyxx\to y \to x, freely subject to the associative law, and also an identity morphism. This CC' 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 CM^{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 CC is almost-Reedy, let C +C_+ (resp. C C_-) be the class of morphisms f:xyf:x\to y such that deg(x)deg(y)\deg(x)\le \deg(y) (resp. deg(y)deg(x)\deg(y)\le \deg(x)) and that do not factor through any object of strictly lesser degree than xx and yy. Then we can show that just as in a Reedy category, every morphism factors uniquely into a C C_--morphism followed by a C +C_+-morphism.

The only thing missing from the usual definition of a Reedy category, therefore, is that C C_- and C +C_+ be subcategories, i.e. closed under composition. And indeed, this can fail to be true; but it is all that can go wrong: CC is a Reedy category if and only if it is an almost-Reedy category such that C C_- and C +C_+ are closed under composition. (In particular, this means that C C_- and C +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_+-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,α)(U,W,\alpha) of the Isbell envelope can also be regarded as a special sort of lax diagram in ProfProf, and the category CC' 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 ProfProf — is precisely what we need in order to conclude that M CM^{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

20 Comments & 0 Trackbacks

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=Hom(*,)W = \mathrm{Hom}(\ast,\cdot) and a set U=Hom(,*)U = \mathrm{Hom}(\cdot,\ast). There is only one function U×WHom(,)=1U \times W \to \mathrm{Hom}(\cdot,\cdot) = 1. Now, in Mike’s formula, we have Hom(*,*)=WU⨿{1 *}\mathrm{Hom}(\ast,\ast) = W\otimes U \amalg \{1_\ast\}, which I think means {}W()×U()⨿{1 *}\int^{\cdot \in \{\cdot\}} W(\cdot) \times U(\cdot) \amalg \{1_\ast\}, which of course is just W×U⨿{1 *}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=W=U=\emptyset, the walking arrow from W=1,U=W=1,U=\emptyset or vice versa, the walking isomorphism from W=U=1W=U=1, the opposite of the site for reflexive graphs / walking reflexive coequalizer comes from W=2,U=1W=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?

Clark Barwick studied some notions of morphism of Reedy category in On Reedy model categories.

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

Re: What is a Reedy Category?

W=U=1W=U=1 actually gives you the walking retraction; 1 *1_\ast is never equal to the composite of a WW-arrow with a UU-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 CC so that M CM^C is a model category, for arbitrary model categories MM? Clearly if MM 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 CC so that every M CM^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