nLab displayed category

Displayed categories

Displayed categories

Idea

A displayed category over a category CC is the “classifying map” of a category over CC. That is, it is equivalent to the data of a category DD and a functor F:DCF:D\to C, but organized differently as a “functor” associating to each object or morphism of CC the fiber over it. The operation (which is an equivalence) taking a displayed category to the corresponding functor F:DCF:D\to C is a generalization of the Grothendieck construction.

Displayed categories are particularly useful in type theory (especially internal categories in homotopy type theory) and to preserve the principle of equivalence, since they allow a more “category-theoretic” formulation of various notions (such as identity-on-objects and Grothendieck fibrations and strict creation of limits) that, if stated in terms of a functor F:DCF:D\to C, would involve equality of objects.

Definitions

By components

A dsplayed category DD over a category CC consists of

  • for each object a:Ca:C, a type D(a)D(a)
  • for each object a:Ca:C and b:Cb:C, morphism f:abf:a \to b, and element x:D(a)x:D(a) and y:D(b)y:D(b), a set of morphisms Hom f(x,y)Hom_f(x, y) from xx to yy over ff
  • for each object a:Ca:C and element x:D(a)x:D(a), a morphism id x:Hom id a(x,x)id_x:Hom_{id_a}(x, x)
  • for each object a:Ca:C, b:Cb:C, and c:Cc:C, morphism f:abf:a \to b and g:bcg:b \to c, and elements x:D(a)x:D(a), y:D(b)y:D(b), z:D(c)z:D(c), a function:
    () a,b,c,f,g,x,y,z():Hom g(y,z)×Hom f(x,y)Hom gf(x,z)(-)\circ_{a, b, c, f, g, x, y, z}(-):Hom_g(y, z) \times Hom_f(x, y) \to Hom_{g \circ f}(x, z)

    such that

  • for all morphisms k:Hom f(x,y)k:Hom_f(x, y), there is the dependent identification
    λ(k):id yk= *k\lambda(k):id_y \circ k =_* k
  • for all morphisms k:Hom f(x,y)k:Hom_f(x, y), there is the dependent identification
    ρ(k):kid x= *k\rho(k):k \circ id_x =_* k
  • for all morphisms k:Hom f(x,y)k:Hom_f(x, y), l:Hom f(y,z)l:Hom_f(y, z), m:Hom f(z,w)m:Hom_f(z, w),
    (kl)m= *k(lm)(k \circ l) \circ m =_* k \circ (l \circ m)

Abstract definition

A displayed category over a category CC is a lax functor from CC, regarded as a bicategory with only identity 2-cells, to the bicategory Span.

Better, it is a lax double functor from CC, regarded as a double category “horizontally” with only identity vertical arrows and 2-cells, to the (pseudo) double category SpanSpan with sets as objects, functions as vertical arrows, and spans as horizontal arrows. Although this produces an equivalent notion, it is better because a displayed functor is then a vertical transformation between such lax double functors.

A displayed category may equivalently be described as a normal lax functor from CC to Prof (either the bicategory or the double category, as appropriate), meaning one that strictly preserves identities. Formally, this is because Prof=Mod(Span)Prof = Mod(Span), where Mod()Mod(-) denotes the double category of horizontal monads and modules, and ModMod is a right adjoint to the inclusion of virtual double categories and normal (lax) functors into all (lax) functors; see (CS, Prop. 5.14).

Equivalently, it is a double profunctor between CC and the terminal double category 11, i.e., a double presheaf on CC.

Correspondence to slices

The category over CC corresponding to a displayed category D:CSpanD:C\to Span is the pullback

D Span * C Span \array{ D & \to & Span_* \\ \downarrow & & \downarrow \\ C & \to & Span }

Where Span *=Span(Set *)Span_*=Span(Set_*) is the bicategory (or double category) of pointed sets and pointed spans. This is a strict pullback, which exists in the 2-category of bicategories (or double categories) and lax functors because the projection Span *SpanSpan_* \to Span is not just lax but strong. Equivalently, it is the pullback

D Prof * C Prof \array{ D & \to & Prof_* \\ \downarrow & & \downarrow \\ C & \to & Prof }

where Prof *Prof_* consists of pointed categories and pointed profunctors, a pointed profunctor H:(A,a 0)(B,b 0)H:(A,a_0)⇸(B,b_0) being equipped with an element of H(a 0,b 0)H(a_0,b_0).

This construction induces an equivalence of categories Disp(C)Cat/CDisp(C) \to Cat/C, which restricts to the following equivalences:

  • A displayed category factors through the inclusion SetSpanSet \hookrightarrow Span (or equivalently SetProfSet \hookrightarrow Prof) if and only if F:DCF:D\to C is a discrete opfibration. Similarly, it factors through Set opSet^{op} if and only if FF is a discrete fibration.

  • A factorization of a displayed category CProfC\to Prof through the inclusion Cat opProfCat^{op} \hookrightarrow Prof (as corepresentable profunctors) is equivalent to giving F:DCF:D\to C the structure of a cloven prefibred category, i.e. equipped with a choice of weakly cartesian liftings. The factorization is a pseudofunctor precisely when F:DCF:D\to C is a Grothendieck fibration; in this case we see the usual Grothendieck construction of a pseudofunctor.

  • Similarly, factorizations through CatProfCat\hookrightarrow Prof corresponds to cloven Grothendieck (pre)opfibrations.

  • An arbitrary displayed category CProfC\to Prof is a pseudofunctor if and only if F:DCF:D\to C is a Conduché functor, i.e. an exponentiable morphism in CatCat.

The construction, explicitly

As mentioned above, there is a construction \int turning a normal lax functor F:CProfF:C \to Prof into a functor π F:FC\pi_F : \int F \to C. Here we spell it out.

But first, let us explictly remark how the opposite construction works. Using notation from Benaboù’s lectures, the normal lax functor dP:CProfdP : C \to Prof associated to a functor P:ECP:E \to C is obtained by ‘taking fibers’. On objects, it maps x:Cx:C to the category P 1xP^{-1}x of objects and maps of EE mapping to xx and its identity arrow, respectively. On morphisms, it maps an arrow f:xyf:x \to y to the profunctor P 1y op×P 1xSetP^{-1}y^{op} \times P^{-1}x \to Set mapping a choice of objects yy' and xx' ‘lifting’ yy and xx respectively to the set of maps f :xyf^\sharp : x'\to y' that project down to ff, i.e.~the ‘fiber over ff’ of the arrow part of PP (which is defined given two objects).

The generalized Grothendieck construction

The category F\int F is built as follows:

  • objects are pairs (x:C,x:Fx)(x:C, x' : Fx)

  • a morphism (x,x)(y,y)(x,x') \to (y,y') is given by a pair of morphisms (f,f )(f,f^\sharp) where f:xyf:x \to y is an arrow in CC and f Ff(y,x)f^\sharp \in Ff(y',x')

  • identities are given by picking 1 x:xx1_x : x \to x and 1 x =1 xF(1 x)(x,x)=Hom Fx(x,x)1_x^\sharp = 1_x' \in F(1_x)(x',x') = \mathrm{Hom}_{Fx}(x',x')

  • composition is defined componentwise: given (f,f ):(x,x)(y,y)(f,f^\sharp) : (x,x') \to (y,y') and (g,g ):(y,y)(z,z)(g,g^\sharp):(y,y') \to (z,z'), the composite is the pair (gf, f,g(y,f ,g ))(gf, \ell_{f,g}(y', f^\sharp, g^\sharp)), where (y,f ,g )(y', f^\sharp, g^\sharp) is the equivalence class of the coend defining the composition FgFfFg \circ Ff (see profunctor) and f,g\ell_{f,g} is the laxator of FF.

Finally, the functor π F\pi_F simply discards the second component on objects and morphisms.

One can readily observe how this construction reduces to the usual Grothendieck construction when FF factors through CatCat.

On morphisms

The above construction is functorial and turns ‘morphisms of normal lax functors into ProfProf’ into morphisms in Cat/CCat/C. To describe this, is useful to notice the category of normal lax functors into Prof is given by Dbl normal,lax vertical(hC,Cat)Dbl_{normal,lax}^{vertical}(hC, Cat), where hChC is the casting of CC, a category, as a double category whose vertical and 2-cells are all trivial.

This category has as objects normal lax double functors CCatC \to Cat, where CatCat is the proarrow equipment of categories, functors (in the vertical/tight direction), profunctors (in the horizontal/loose direction) and suitable natural transformations as 2-cells. The morphisms are then vertical natural transformations between them.

Let’s spell out the definition of one of these vertical natural transformations ϕ:FG\phi : F \Rightarrow G. Its components are given by functors (i.e. vertical cells in CatCat) ϕ x:FxGx\phi_x : Fx \to Gx, indexed by objects x:Cx:C, and squares

indexed by morphisms f:xyf:x\to y in CC. These have, moreover, to satisfy various ‘natural’ conditions of compatibility with horizontal composition of squares in CatCat and so on.

The equivalence \int converts this data back to a commutative triangle

The crucial thing to notice here is that, fundamentally, such a functor over CC is defined ‘fiberwise’, in the sense that, choosen an object x:Cx:C, ϕ\int \phi has to restrict to a functor ϕ x:π F 1xπ G 1x\int\phi_x : \pi_F^{-1}x \to \pi_G^{-1}x. But these categories are, by definition, FxFx and GxGx, so that ϕ x\int \phi_x can be naturally defined to be ϕ x\phi_x itself.

Now what’s left to define is the action of ϕ\int \phi on those arrows that cross fibers (in a sense, all the arrows except those that map to identities in CC – or, put differently again, the above discussion pinned down the object part of ϕ\int \phi).

Thus let (f,f ):(x,x)(y,y)(f,f^\sharp):(x,x') \to (y,y') be a morphism in F\int F. We know how to map (x,x)(x,x') and (y,y)(y,y') using ϕ x\phi_x and ϕ y\phi_y respectively, so that ϕ(f,f )\int \phi(f,f^\sharp) has to be an arrow (x,ϕ x(x))(y,ϕ y(y))(x,\phi_x(x')) \to (y,\phi_y(y')). The exact arrow is picked by the last piece of data from the vertical transformation ϕ\phi, the ‘strength’ st ϕ\mathrm{st}^{\phi}. In fact this is a natural transformation whose components are st x,y ϕ:Ff(x,y)Gf(ϕ x(x),ϕ y(y))\mathrm{st}^{\phi}_{x',y'} : Ff(x',y') \to Gf(\phi_x(x'),\phi_y(y')), which is exactly the data needed to define the arrow part of ϕ\int \phi.

Functoriality of ϕ\int \phi is a direct consequence of the properties required to ϕ\phi, which are spelled out at vertical natural transformation.

References

The correspondence between categories over CC and normal lax functors CProfC\to Prof was observed by Bénabou already in 1972:

  • Jean Bénabou, 2-dimensional limits and colimits of distributors (or how to glue together categories), Oberwolfach ‘Tagungsbericht’, 1972, (web)

A more detailed account of Benaobou’s work on this topic can be found at:

  • Jean Bénabou, Distributors at work, Notes by Thomas Streicher from lectures given at TU Darmstadt, 2000, pdf

The term “displayed category”, and the applications to type theory, are due to:

An unpacking of the definition as lax functors into Span is in 2.2 of

Also cited above:

Last revised on October 27, 2022 at 07:38:57. See the history of this page for a list of all contributions to it.