5. Small fibrations and internal categories [000N]

The purpose of this section is to develop the relationship between internal categories (categories defined in the internal language of a category $B$) and cartesian fibrations over $B$, generalizing the relationship between categories internal to $\SET$ (i.e. small categories) and their family fibrations over $\SET$.

[001Q] Definition 5·a (Small fibration).

A cartesian fibration is called small when it is both locally small [000I] and globally small [000J].

We have already seen in Section 4.1.1 [000G] and Theorem 4.2.1·b [000L] that smallness in the sense of the definition above appropriately generalizes the ordinary notion of smallness for categories over $\SET$. Another perspective on smallness is given by the internal language, in which a category is viewed as an algebra for the “theory of categories” computed in another category with enough structure. The notion of internal categories is credited (independently) to Alexander Grothendieck and Charles Ehresmann.

5.1. Internal categories [000O]

The notion of a (meta-)category is an essentially algebraic theory. As such it is possible to compute models of this theory in any category that has finite limits.

[001A] Definition 5.1·a (Internal category).

Let $E$ be a category with finite limits; then an internal category in $E$ is defined by the following data:

  1. an object of objects $C\Sub{0}\in E$,
  2. an object of morphisms $C\Sub{1}\in E$,
  3. source and target morphisms $s,t:C\Sub{1}\to C\Sub{0}$,
  4. a generic identity morphism $C\Sub{0}\to C\Sub{1}$,
  5. a generic composition morphism $C\Sub{1}\times\Sub{C\Sub{0}}C\Sub{1}\to C\Sub{1}$,
  6. satisfying a number of laws corresponding to those of a category.

For the details of these laws, we refer to the nLab (internal category).

5.2. The externalization of an internal category [000V]

[001R] Construction 5.2·a.

Let $C$ be an internal category in $E$. We may define a fibered category $\brk{C}$ over $E$ called the externalization of $C$.

  1. Given $x\in E$, an object of $\brk{C}\Sub{x}$ is defined to be a morphism $x\to C\Sub{0}$ in $E$.

  2. Given $x,y\in E$ and $f:x\to y$ and $u \in \brk{C}\Sub{x}$ and $v\in \brk{C}\Sub{y}$, a morphism $u\to\Sub{f} v$ is defined to be a morphism $h : x\to C\Sub{1}$ in $E$ such that the following diagram commutes:

[000W] Lemma 5.2·b.

The externalization [000V] is a cartesian fibration.

Proof. Given an object $v\in \brk{C}\Sub{y}$ and a morphism $f:x\to y$ in $E$, we may define a cartesian lift $\InvImg{f}v\to\Sub{f} v$ by setting $\InvImg{f}v = v\circ f : x \to C\Sub{0}$.

[000X] Lemma 5.2·c.

The externalization [000V] is globally small

Proof. We may choose a generic object [000K] for $\brk{C}$, namely the identity element $(C\Sub{0},\Idn{C\Sub{0}})\in \TotCat{\brk{C}}$. Given any object $(x,u)\in \TotCat{\brk{C}}$ the cartesian map $(x,u)\to (C\Sub{0},\Idn{C\Sub{0}})$ is given as follows:

[000Y] Lemma 5.2·d.

The externalization [000V] is locally small

Proof. Fix $x\in E$ and $u,v\in \brk{C}\Sub{x}$, we must exhibit a terminal object to the (total) category $\TotCat{\CandHom{x}{u}{v}}$ of “hom candidates” defined in [000I]. First we define $\brk{u,v}$ to be the following pullback in $E$:

We define $\overline{p}:\InvImg{\brk{u,v}}{u}\to\Sub{p} u\in \brk{C}\Sub{\brk{u,v}}$ to be the cartesian lift of $u\in \brk{C}\Sub{x}$ along $p:\brk{u,v}\to x$:

We need to define a displayed evaluation map $\epsilon : \InvImg{\brk{u,v}}u\to\Sub{p} v$; unraveling the definition of a displayed morphism in the externalization of $C$, we choose the following diagram:

Putting all this together, we assert that the terminal object of $\TotCat{\CandHom{x}{u}{v}}$ is the following span in $\brk{C}$:

Fixing another such candidate hom span $\brc{u \leftarrow \bar{h}\rightarrow v}\in\TotCat{\CandHom{x}{u}{v}}$, according to [000I] we must exhibit a unique cartesian morphism $\bar\alpha : \bar{h}\to \InvImg{\brk{u,v}}{u}$ making the following diagram commute:

First we note that the evaluation map $\epsilon\Sub{h} : \bar{h}\to v$ amounts to an internal morphism $h\to C\Sub{1}$ satisfying the appropriate compatibility conditions. Therefore we may define the base $\alpha:h\to \brk{u,v}$ of the universal map using the universal property of the pullback that defines $\brk{u,v}$:

The morphism $\alpha:h\to \brk{u,v}$ defined above is the unique map in $E$ satisfying the conditions required of the base for $\bar\alpha$; therefore, it suffices to show that there exists a cartesian morphism $\bar\alpha:\bar{h}\to\Sub{\alpha}\InvImg{\brk{u,v}}u$ since it will be unique if it exists. We define $\bar\alpha$ using the universal property of the cartesian lift:

That $\bar{\alpha}:\bar{h}\to\Sub{\alpha}\InvImg{\brk{u,v}}u$ is cartesian follows from the “generalized pullback lemma” for cartesian morphisms [0014]: it suffices to observe that both $\bar{p}\Sub{h}:\bar{h}\to u$ and its second factor $\bar{p}:\InvImg{\brk{u,v}}u\to u$ are cartesian.

5.3. The full internal subcategory associated to a displayed object [0011]

The full internal subfibration (Construction 2.9·a [0010]) associated to a displayed object $\bar{u}$ of a locally small cartesian fibration $E$ over $B$ can be seen to be equivalent to the externalization of an internal category $\gl{\bar{u}}$ in $B$. In particular, we let the object of objects $\gl{\bar{u}}\Sub{0}$ be $u$ itself; defining the object of arrows $\gl{\bar{u}}\Sub{1}$ is more complex, making critical use of the local smalness of $E$ over $B$.

We will think of the fiber $E\Sub{u\times u}$ as the category of objects indexed in the boundary (source and target) of a morphism. Restricting $\bar{u}$ along the source and target projections, we obtain the displayed objects of “points of the source” and “points of the target” respectively:

Because $E$ is locally small, there is an object $\brk{\bar\partial\Sub{1},\bar\partial\Sub{2}}\in \Sl{B}{u\times u}$ that behaves as the “generic hom set”. We define $\gl{\bar{u}}\Sub{1}\in B$ and its source and target projections to be this very object.

[001S] Theorem 5.3·a.

The externalization $\brk{\gl{\bar{u}}}$ of the internal category $\gl{\bar{u}}$ is equivalent to $\FullSubfib{\bar{u}}$.

Proof. We will define a fibred equivalence $F : \brk{\gl{\bar{u}}}\to \FullSubfib{\bar{u}}$ over $B$.

  1. Fix $x\in B$ and $\chi\Sub{x} \in \brk{\gl{\bar{u}}}\Sub{x}$, i.e. $\chi\Sub{x} : x\to u$; we define $F\prn{\chi\Sub{x}}$ to be an arbitrary cartesian map $\phi\Sub{x} : \bar{x}\to\Sub{\chi\Sub{x}} \bar{u}$. (Here we have used the axiom of choice for collections [000R].)

  2. Fix $f : x\to y\in B$ and $\chi\Sub{x} :x\to u$ and $\chi\Sub{y}:y\to u$ and a diagram representing a displayed morphism $h$ from $\chi\Sub{x}$ to $\chi\Sub{y}$ over $f$ as below:

    We must define $F\prn{h}:\bar{x}\to\Sub{f} \bar{y}$, fixing arbitrary cartesian maps $\bar\chi\Sub{x}:\bar{x}\to\Sub{\chi\Sub{x}}\bar{u}$ and $\bar\chi\Sub{y}:\bar{y}\to\Sub{\chi\Sub{y}}\bar{u}$. First we lift $h:x\to \brk{\bar\partial\Sub{1},\bar\partial\Sub{2}}$ into $E$ using the universal property of the cartesian lift:

    By composition with the “evaluation map” for our hom object, we have a map $\bar{x}\to\Sub{f;\chi\Sub{y}}\bar{u}$:

    Next we define $F\prn{h}:\bar{x}\to\Sub{f}\bar{y}$ using the universal property of (another) cartesian lift:

5.4. The internalization of a small fibration [000Z]

Let $C$ be a small cartesian fibration (Definition 5·a [001Q]) over $B$ a category with finite limits, i.e. a cartesian fibration that is both locally small (Definition 4.1.3·b [001B]) and globally small (Definition 4.2·b [000P]). We will show that $C$ is equivalent to the externalization [000V] of an internal category [000O] $\underline{C}$ in $B$, namely the full internal subcategory [0011] associated to the generic object $\bar{u}\in C$.

By Theorem 5.3·a [001S] we know that the externalization of $\underline{C}$ so-defined is equivalent to the full subfibration $\FullSubfib{\bar{u}}$ of $C$ spanned by objects that are “classified” by $\bar{u}$. Because $\bar{u}$ is generic, we know that every object of $C$ is classified by $\bar{u}$, so we are done.