nLab
internal diagram

Idea

Given a finitely complete category $E$, one can consider the bicategory $\mathrm{Cat}(E)$ of internal categories in $E$, and thus internal functors, which are the morphisms in $\mathrm{Cat}(E)$. If $E=\mathrm{Set}$ then one can consider not only functors among small categories but also functors of the type $F:C\to \mathrm{Set}$ from a small category $C$ to a large category of sets. In that case one can describe $F$ as consisting of a $C_0$-indexed family of objects and an action of $C_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 $C$ is the same thing as an internal profunctor $C⇸1$, which is the same thing as a discrete opfibration in $\mathrm{Cat}(E)$. The three generalize the basic idea in different ways.

Definition

In category theory

Given an internal category $C\in \mathrm{Cat}(E)$, with the usual structure maps $s,t,i,c$, an internal diagram $F$ on $C$ (or, of type $C$) is given by

• a morphism $d:F_0\to C_0$ in $E$ together with
• a morphism $e:F_1=F_0{\times }_{C_0}{C}_1\to F_0$

where $F_1$ is the pullback

(1)$$\begin{array}{ccc}{F}_0{\times }_{C_0}{C}_1& \to & F_0\\ s^{*}d\downarrow & & \downarrow d\\ C_1& \underset{s}{\to }& C_0\end{array}$$\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:

• $e$ respects the source and target maps of $C$, in that $d\circ e=t\circ s^{*}d$. Equivalently, $e$ is a morphism from $s^{*}d$ to $t^{*}d$ in $E/C_1$.

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

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

An internal diagram on $C^{\mathrm{op}}$ is sometimes called an internal presheaf on $C$.

In dependent type theory

Using the language of dependent types, the map $d:F_0\to C_0$ can be seen as the interpretation of a dependent type $(X:C_0)⊢(F(X):\mathrm{Type})$. The action of $C_1$ on $F_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_1$ to depend on $C_0\times C_0$ by the canonical morphism $C_1\to C_0\times C_0$ induced by $s$ and $t$, as in the type-theoretic definition of category.

If the ambient category $E$ 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:{\Pi }_{X,Y:C_0}{\Pi }_{f:C_1(X,Y)}(F(X)\to 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 $E$:

• $(X:C_0),(a:F(X))⊢p(X,X,{\mathrm{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,g\circ f,a)=p(Y,Z,g,p(X,Y,f,a))$

Properties

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

There is a composite forgetful functor $U:E^C\to \mathrm{Cat}(E)/C\to E/C_0$. This functor $U$ is monadic — its left adjoint takes $p:X\to C_0$ to $t\circ s^{*}p: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 $E$. Given a fibration in the guise of an indexed category $F:S^{\mathrm{op}}\to \mathrm{Cat}$, a $C$-diagram in $F$ is given by

• an object $P\in F(C_0)$, together with
• a morphism $\varphi :s^{*}P\to t^{*}P$ in $F(C_1)$

satisfying ‘cocycle equations’

• $i^{*}\varphi =1_P$
• $c^{*}\varphi =p_1^{*}\varphi \circ p_2^{*}\varphi$

modulo coherent isos, where the $p_i$ are the projections out of $C_2$.

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

Examples

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

• If $E$ is equipped with a coverage and $C$ is the Cech nerve associated to a cover $p:U\to X$ in $E$, then the category of $C$-diagrams in $F$ is the descent category ${\mathrm{Des}}_p(F)$.

Related concepts

• diagram, internal presheaf, internal sheaf

References

• P. T. Johnstone, Topos theory, 1977, chapter 2