internal diagram

Internal diagrams


Given a finitely complete category EE, one can consider the bicategory Cat(E)Cat(E) of internal categories in EE, and thus internal functors, which are the morphisms in Cat(E)Cat(E). If E=SetE = Set then one can consider not only functors among small categories but also functors of the type F:CSetF: C\to Set from a small category CC to a large category of sets. In that case one can describe FF as consisting of a C 0C_0-indexed family of objects and an action of C 1C_1 on the diagram.

Compare the ideas discussed on this page with those at internal profunctor and discrete fibration. All three notions intersect — an internal diagram on CC is the same thing as an internal profunctor C1C ⇸ 1, which is the same thing as a discrete opfibration in Cat(E)Cat(E). The three generalize the basic idea in different ways.


In category theory

Given an internal category CCat(E)C\in Cat(E), with the usual structure maps s,t,i,cs,t,i,c, an internal diagram FF on CC (or, of type CC) is given by

  • a morphism d:F 0C 0d : F_0\to C_0 in EE together with
  • a morphism e:F 1=F 0× C 0C 1F 0e : F_1= F_0\times_{C_0} C_1 \to F_0

where F 1F_1 is the pullback

(1)F 0× C 0C 1 F 0 s *d d C 1 s C 0 \array{ F_0 \times_{C_0} C_1 & \to & F_0 \\ \mathllap{s^* d} \downarrow & & \downarrow \mathrlap{d} \\ C_1 & \underset{s}{\to} & C_0 }

These data must satisfy the following conditions:

  • ee respects the source and target maps of CC, in that de=ts *dd \circ e = t \circ s^* d. Equivalently, ee is a morphism from s *ds^* d to t *dt^* d in E/C 1E/C_1.

  • ee is an action in the sense that e(1×i)=1e \circ (1 \times i) = 1 and e(e×1)=e(1×c)e(e \times 1) = e(1 \times c).

It is clear how to define homomorphisms of internal diagrams: a morphism FGF \to G is given by an E/C 0E/C_0-morphism F 0G 0F_0 \to G_0 that commutes with the actions ee. Internal diagrams on CC in EE form a category denoted by E CE^C.

An internal diagram on C opC^{op} is sometimes called an internal presheaf on CC.

In dependent type theory

Using the language of dependent types, the map d:F 0C 0d: F_0 \to C_0 can be seen as the interpretation of a dependent type (X:C 0)(F(X):Type)(X:C_0) \,\vdash\, (F(X):Type). The action of C 1C_1 on F 0F_0 can equivalently be given by the interpretation of a term in context:

(X:C 0),(Y:C 0),(f:C 1(X,Y)),(a:F(X))(p(X,Y,f,a):F(Y)). (X:C_0), (Y:C_0), (f:C_1(X,Y)), (a:F(X)) \;\vdash\; (p(X,Y,f,a) : F(Y)).

Here we consider C 1C_1 to depend on C 0×C 0C_0 \times C_0 by the canonical morphism C 1C 0×C 0C_1 \to C_0 \times C_0 induced by ss and tt, as in the type-theoretic definition of category.

If the ambient category EE is a locally cartesian closed category, so that its internal type theory has dependent product types, then this can be interpreted instead as a closed term

p:Π X,Y:C 0Π f:C 1(X,Y)(F(X)F(Y)). p : \Pi_{X,Y:C_0} \Pi_{f:C_1(X,Y)} (F(X) \to F(Y)).

The axioms then take a particularly familiar form, also to be interpreted in the internal language of EE:

  • (X:C 0),(a:F(X))p(X,X,id X,a)=a(X:C_0), (a:F(X)) \;\vdash\; p(X,X,id_X,a) = a
  • (X,Y,Z:C 0),(f:C 1(X,Y)),(g:C 1(Y,Z)),(a:F(X))p(X,Z,gf,a)=p(Y,Z,g,p(X,Y,f,a))(X,Y,Z:C_0), (f:C_1(X,Y)), (g:C_1(Y,Z)), (a:F(X)) \;\vdash\; p(X,Z,g \circ f,a) = p(Y,Z,g,p(X,Y,f,a))


From an internal diagram (F,C,λ,e)(F,C,\lambda,e) one can equip F=(F 0,F 1)F =(F_0,F_1) with a structure of an internal category over CC. In other words, there is a forgetful functor E CCat(E)/CE^C\to Cat(E)/C (where Cat(E)/CCat(E)/C is the corresponding slice category). This functor is fully faithful and its essential image consists precisely of all objects in Cat(E)/CCat(E)/C which are discrete opfibrations. Similarly, the objects of E C opE^{C^{op}} are the discrete fibrations in Cat(E)/CCat(E)/C.

There is a composite forgetful functor U:E CCat(E)/CE/C 0U \colon E^C \to Cat(E)/C \to E/C_0. This functor UU is monadic — its left adjoint takes p:XC 0p \colon X \to C_0 to ts *p:X× C 0C 1C 1C 0t \circ s^* p \colon X \times_{C_0} C_1 \to C_1 \to C_0.

Diagrams in an indexed category

An internal diagram as above may take values in any Grothendieck fibration over EE. Given a fibration in the guise of an indexed category F:S opCatF : S^{op} \to Cat, a CC-diagram in FF is given by

  • an object PF(C 0)P \in F(C_0), together with
  • a morphism ϕ:s *Pt *P\phi : s^* P \to t^* P in F(C 1)F(C_1)

satisfying ‘cocycle equations’

  • i *ϕ=1 Pi^*\phi = 1_P
  • c *ϕ=p 1 *ϕp 2 *ϕc^*\phi = p_1^* \phi \circ p_2^* \phi

modulo coherent isos, where the p ip_i are the projections out of C 2C_2.

By the Yoneda lemma for bicategories, the object PP determines (up to canonical isomorphism) a pseudonatural α 0:E(,C 0)F 0\alpha^0 : E(-,C_0) \to F_0 in [E op,Cat][E^{op},Cat], where EE is considered as a locally discrete bicategory, and F 0(X)=obFXF_0(X) = ob F X considered as a discrete category, such that α 0(f)f *P\alpha^0(f) \cong f^* P. Similarly, ϕ\phi determines α 1:E(,C 1)F 1=arrF\alpha^1 : E(-,C_1) \to F_1 = arr \circ F, and α 1(g)g *ϕ\alpha^1(g) \cong g^* \phi. It is not hard to check that the conditions above correspond to requiring that the α X i\alpha^i_X form a functor E(X,C)FXE(X,C) \to F X for each XX, and pseudonaturality then makes the CC-diagram (P,ϕ)(P,\phi) equivalent to an indexed functor E(,C)FE(-,C) \to F. The category of CC-diagrams in FF is then simply the hom-category [E op,Cat](E(,C),F)[E^{op},Cat](E(-,C),F).


  • An internal diagram on CC in the sense above is a CC-diagram in the codomain fibration of EE, that is the pseudofunctor XE/XX \mapsto E/X.

  • If EE is equipped with a coverage and CC is the Cech nerve associated to a cover p:UXp : U \to X in EE, then the category of CC-diagrams in FF is the descent category Des p(F)Des_p(F).


Revised on August 30, 2012 02:07:03 by Urs Schreiber (