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.

December 18, 2012

Enriched Indexed Categories

Posted by Mike Shulman

Here’s the second of the three papers about generalized category theory that I promised you last time:

This one is about a notion of “category” which simultaneously generalizes enriched categories, internal categories, and indexed categories.

When we first learn about category theory, we usually work with categories that have a set (or class) of objects and a set (or class) of morphisms. Later, we may learn that this can be generalized in several ways:

  1. If VV is a monoidal category, then a VV-enriched category has a set of objects, but hom-objects hom(x,y)hom(x,y) that lie in VV. When V=SetV=Set, we recover the original notion of (locally small) category.

  2. If CC is a category with pullbacks, then a CC-internal category has a CC-object of objects and a CC-object of morphisms. When C=SetC=Set, we recover the original notion of (small) category.

  3. If SS is any category, then an SS-indexed category has, for each object XSX\in S, an ordinary category of “XX-indexed objects”.

Each of these kinds of category has its own “category theory”, with all the usual stuff: limits, colimits, adjunctions, monads, etc. But the three cases are fairly different from each other. Internal categories can be identified with certain indexed ones, but it’s harder to compare the enriched and indexed cases. When I first learned about all of these, I found it unsatisfying that we have two or three useful generalizations of the notion of category, but that they seem to be incomparable.

Often, however, when one important concept can be generalized in seemingly-different ways, there is actually a further generalization which includes them all, and that is the case here. The very general generalization is the notion of category enriched in a bicategory, or even more generally category enriched in a virtual equipment (i.e. fc-multicategory). The former has been studied by various category theorists off and on for years; the latter was first proposed by Tom.

The point of the new paper is that there’s a less general generalization than this, which still includes all three basic examples, and which is worth studying in its own right. In this case, what we enrich in is an indexed monoidal category, a.k.a. a monoidal fibration. If you’ve been following my blog posts for a couple of years (e.g. this one and this one), then you may know that these things are close to my heart.

An indexed monoidal category consists of a category SS (which here we assume to have finite products) and a pseudofunctor V:S opMonCatV:S^{op}\to MonCat. Given such a beast, there is a fairly natural definition of a VV-enriched category: its objects are in, or indexed over, SS, while its homs are objects of the “fiber categories” V(X)V(X). Thus, we can think of it as simultaneously indexed over SS and enriched over VV, hence the name “enriched indexed categories”. When SS has pullbacks and V(X)=S/XV(X) = S/X, then this gives internal and indexed categories (depending on the “size” we choose to use), while when S=SetS=Set and V(X)=V XV(X) = V^X for an ordinary monoidal category VV, this gives classical enriched categories.

An indexed monoidal category also gives rise to a bicategory, or more generally to a (virtual) equipment, as I showed way back in this paper. Thus, the very general theory can be applied. This is nice, because it automatically produces formally well-behaved notions of limit, colimit, presheaf, etc. However, in the special case of an indexed monoidal category, we can reinterpret these formal notions in more explicit and familiar terms, which turn out to combine standard ideas from enriched category theory and indexed category theory in very natural ways.

For instance, one way to think of an enriched indexed category (which is not the one that you get automatically out of the bicategory/equipment setup) is that it consists of a V(X)V(X)-enriched category C(X)C(X) for each object XSX\in S, which we may call the “fiber over XX”, together with appropriately defined “restriction functors”. When we unravel the abstract notion of limit with respect to this description, we get examples like the following:

  • Weighted limits in some fiber category C(X)C(X), in the usual V(X)V(X)-enriched sense, which are moreover preserved by the restriction functors (the common requirement on ordinary “fiberwise” limits in indexed category theory).

  • Left and right adjoints to the restriction functors satisfying the Beck-Chevalley condition (this is the usual notion of “indexed (co)product” from indexed category theory), which moreover lift to “V(X)V(X)-enriched adjunctions” in an appropriate sense.

This is why it’s worth studying the less general notion of category: it includes lots of important examples, and it has interesting and useful structure not present in the more general generalization. I find it very pleasing how the abstract equipment-theoretic context automatically tells us the right way to combine “enriched-ness” with “indexed-ness”.

There’s a list of a bunch of examples in the introduction to the paper, and more specific examples appear throughout. Let me close by mentioning two of the examples that motivated me to write the paper.

  • In May and Sigurdsson’s parametrized homotopy theory, there are categories of parametrized spectra Sp BSp_B over base topological spaces BB. These fit together to form a category which is both indexed over TopTop and enriched over the classical category of spectra. In fact, it is itself a monoidal fibration, and hence we can enrich further over it.

  • In Anna Marie Bohmann’s global equivariant homotopy theory, the category of “global spectra” is both indexed over GrpGrp and enriched over TopTop. Moreover, it is most naturally defined by mimicking the classical construction of orthogonal spectra, but in the world of GrpGrp-indexed TopTop-enriched categories.

Posted at December 18, 2012 1:05 AM UTC

TrackBack URL for this Entry:

5 Comments & 0 Trackbacks

Re: Enriched Indexed Categories

This looks like a really nice way of bringing together enriched, internal and indexed category theory.

One thing I’d like to understand better is your notion of “base” for enrichment, namely, indexed monoidal categories. (To save anyone scrolling upwards: given a category SS with finite products, Mike defines an SS-indexed monoidal category to be a pseudofunctor S opMonCatS^{op} \to MonCat, the codomain being the 2-category with the obvious 0- and 2-cells and strong monoidal functors as 1-cells.)

You’ve shown that taking indexed monoidal categories as the base for enrichment works well, in the sense of doing a good job of unifying the three generalizations of category theory. Also, indexed monoidal categories obviously combine the ideas of “indexing category” and “monoidal category”.

But can you give any other insight into the importance of this particular structure? E.g. why is it important that we use pseudofunctors rather than colax functors (which, after all, still have categories of elements)? Why is it important that we take strong monoidal functors as the 1-cells in MonCatMonCat?

Posted by: Tom Leinster on December 18, 2012 2:46 AM | Permalink | Reply to this

Re: Enriched Indexed Categories

Interesting questions!

I might begin with a pragmatic answer: all the most interesting examples I know of are pseudofunctors into monoidal categories with strong monoidal functors, and the theory would be more difficult to develop if we weakened those assumptions. But I know better than to expect that to satisfy you!

So I might then move on to a more philosophical answer. Namely, if you believe in indexed categories, where the way to do everything is to do it in each fiber in a way which is stable under pullback/restriction, then these are the obvious notion of indexed monoidal category: you have a monoidal structure on each fiber, which is stable under pullback. More 2-categorically, these are the pseudomonoids in the 2-category of indexed categories.

However, even the philosophical answer misses something, because there is something even more general that we might consider enriching in. Classically, we know that we can enrich not only in monoidal categories but it multicategories. That suggests that we should certainly also be able to enrich in indexed multicategories. The obvious notion of indexed multicategory would be a pseudofunctor S opMulticatS^op \to Multicat, and I’m pretty sure this would be good enough for all the basic definitions in my paper (although, as usual, you get stuck at some point down the line without tensor products). Moreover, if we regard monoidal categories as multicategories in the usual way, multifunctors correspond to lax monoidal functors. So a pseudofunctor S opMonCat laxS^op \to MonCat_{lax} should arguably be regarded, not as an indexed monoidal category, but as an indexed multicategory, with the additional property that its fibers are representable (but not stably).

I doubt you could get much of anywhere with a pseudofunctor landing in MonCat colaxMonCat_{colax}. Colax functors landing in MonCatMonCat or MonCat laxMonCat_{lax} might work, though, but I don’t really have any intuition for why that should or shouldn’t be.

This does suggest something else, though: since classically we can actually enrich, not only in a multicategory, but in any virtual double category (fc-multicategory), is there a notion of “indexed virtual double category” that we can also enrich in? Is the construction of a (virtual) double category from an indexed monoidal category (or indexed multicategory) a special case of a sort of “Grothendieck construction” for diagrams of indexed virtual double categories?

Posted by: Mike Shulman on December 18, 2012 4:13 AM | Permalink | Reply to this

Re: Enriched Indexed Categories

Could the diagrams you found for indexed monoidal categories play a role when enriching?

Has anyone thought of enrichment in the predicate calculus? Hmm, like a metric space, you could have a formula as the shortest ‘distance’ between points. Maybe each object is a collection of formulae and the hom space is the ‘weakest’ formula you need to add to allow deduction, the conditional from the conjunction of the domain to the conjunction of the codomain.

Posted by: David Corfield on December 18, 2012 9:49 AM | Permalink | Reply to this

Re: Enriched Indexed Categories

You can certainly express the defining morphisms of enrichment using string diagrams. I didn’t feel any need for string diagrams in the theory of enrichment, though, not having any very complicated diagrams to commute. (Although some of the long chains of isomorphisms of profunctors might naturally be expressed in a string diagram notation for double categories.)

I’ve never heard of enriching in the predicate calculus. The usual hyperdoctrine I think of has types as objects, in which case a small enriched category would be some kind of ‘poset’: a type equipped with a binary relation and proofs of its reflexivity and transitivity. A more general enriched category would be a many-object version of that. But you might be able to build a different indexed monoidal category that would give your example.

Posted by: Mike Shulman on December 18, 2012 12:19 PM | Permalink | Reply to this

Re: Enriched Indexed Categories

Returning after a few years to this thought of a kind of logical enrichment (with enrichment in the air at the moment), I just came across some comments by somone called Adam on the Existential Type blog:

Are you aware of anybody noticing that the context category (contexts are objects, open terms are morphisms — the one you’ve been writing about) of a type theory is enriched in the judgment category (tuples-of-judgments are objects, natural deductions are morphisms from their hypotheses-as-a-tuple to their conclusion) of the same type theory?

Sequents ABA\vdash B become hom-objects Hom(A,B)Hom(A,B), and so on. Just about the only requirement is that the cut rule be derivable (not just admissible); this nothing more than the typing rule for “let” in a pure functional language:

Γ 1e 1:τ 1\Gamma_1 \vdash e_1:\tau_1 Γ 2,x:τ 1e 2:τ 2\Gamma_2,x:\tau_1 \vdash e_2:\tau_2

Γ 1,Γ 2letx=e 1ine 2:τ 2\Gamma_1,\Gamma_2 \vdash \;let\; x=e_1\; in\; e_2:\tau_2

The enrichment relationship above isn’t anything particularly earth-shattering (and in hindsight it’s sort of obvious), but it’s been remarkably hard to figure out who to cite.

I suppose I ought to add that the framework above leads to very concise statements of some of the big ideas in type theory.

For example, the “compositional bijection” part of the LF adequacy theorem amounts to saying that there is a full and faithful monoidal functor from the judgments category (i.e. enriching category) of the theory being formalized to the context category (i.e. enriched category) of λΠ\lambda\Pi. From this perspective, HOAS works because LF’s context category is cartesian closed.

Moving from cartesian monoidal structure to non-symmetric monoidal structure may yield insight on what an ordered logic analogue of LF ought to look like (IIRC ordered logic was one of the few cases which couldn’t be handled by the technique in Crary’s 2009 paper).

Posted by: David Corfield on September 8, 2016 1:21 PM | Permalink | Reply to this

Post a New Comment