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.