Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 8.2.1.8. Let $\lambda = (\lambda _{-}, \lambda _{+}): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ be a corepresentable coupling and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}_{+}$ be a cocartesian fibration of $\infty $-categories. Suppose that, for every object $Y \in \operatorname{\mathcal{C}}_{+}$, the fiber $\{ Y \} \times _{ \operatorname{\mathcal{C}}_{+} } \operatorname{\mathcal{E}}$ has an initial object. Then the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ has an initial object. Moreover, an object $F \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is initial if and only if it satisfies the following pair of conditions:

$(1)$

For every couniversal object $C \in \operatorname{\mathcal{C}}$, the image $F(C)$ is initial when viewed as an object of the $\infty $-category $\{ \lambda _{+}(C) \} \times _{ \operatorname{\mathcal{C}}_{+} } \operatorname{\mathcal{E}}$.

$(2)$

The functor $F$ carries $\lambda _{+}$-cocartesian morphisms of $\operatorname{\mathcal{C}}$ to $U$-cocartesian morphisms of $\operatorname{\mathcal{E}}$.

Proof of Proposition 8.2.1.8. The functor $\lambda _{-}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$ is a cocartesian fibration (Proposition 8.2.1.7) and is therefore exponentiable (Proposition 5.3.6.1). Let $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ and $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{C}}_{+} )$ be the relative exponentials introduced in Construction 4.5.9.1. Composition with $U$ induces a functor $V: \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{C}}_{+} )$, which is an isofibration by virtue of Proposition 4.5.9.17. Let us identify the functor $\lambda _{+}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{+}$ with a section $s$ of the projection map $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{C}}_{+} ) \rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$, and form a pullback diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{D}}\ar [r] \ar [d]^{V'} & \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \ar [d]^{V} \\ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \ar [r]^-{s} & \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{C}}_{+} ). } \]

Since $V'$ is a pullback of $V$, it is also an isofibration (Remark 4.5.5.11). Moreover, the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ can be identified with the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} }( \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{D}})$ of sections of $V'$.

For each object $X \in \operatorname{\mathcal{C}}_{-}$, let $\operatorname{\mathcal{C}}_{X}$ denote the fiber $\{ X\} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{C}}$. Unwinding the definitions, we can identify objects of $\operatorname{\mathcal{D}}$ with pairs $(X, F_ X)$, where $X$ is an object of $\operatorname{\mathcal{C}}_{-}$ and $F_ X: \operatorname{\mathcal{C}}_{X} \rightarrow \operatorname{\mathcal{E}}$ is a functor satisfying $U \circ f = \lambda _{+}|_{ \operatorname{\mathcal{C}}_{X} }$. For fixed $X \in \operatorname{\mathcal{C}}_{-}$, our assumption that $\lambda $ is corepresentable guarantees that the $\infty $-category $\operatorname{\mathcal{C}}_{X}$ has an initial object $C$. Set $Y = \lambda _{+}(C)$. By assumption, the $\infty $-category $\{ Y \} \times _{ \operatorname{\mathcal{C}}_{+} } \operatorname{\mathcal{E}}$ also has an initial object. Invoking the criterion of Corollary 7.3.6.11, we see that the $\infty $-category $\{ X\} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}\simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}_{X}, \operatorname{\mathcal{E}})$ also has an initial object. Moreover, an object $F_ X \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}_{X}, \operatorname{\mathcal{E}})$ is initial if and only if it satisfies the following pair of conditions:

$(1_{X})$

For every initial object $C \in \operatorname{\mathcal{C}}_{X}$, the image $F_ X(C)$ is an initial object of the $\infty $-category $\{ Y\} \times _{\operatorname{\mathcal{C}}_{+}} \operatorname{\mathcal{E}}$.

$(2_{X})$

The functor $F_ X$ carries each morphism in $\operatorname{\mathcal{C}}_{X}$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$.

We will prove below that the functor $V'$ is a cartesian fibration. Assuming this Corollary 7.3.5.7, we guarantees that the $\infty $-category

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}}( \operatorname{\mathcal{C}}_{-}^{\operatorname{op}},\operatorname{\mathcal{D}}) \]

has an initial object. Moreover, an object $F \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is initial if and only if, for every object $X \in \operatorname{\mathcal{C}}_{-}$, the restriction $F_{X} = F|_{ \operatorname{\mathcal{C}}_{X} }$ satisfies conditions $(1_{X} )$ and $(2_{X} )$ above. Unwinding the definitions, this is equivalent to the requirement that $F$ satisfies condition $(1)$ and the following variant of condition $(2')$ of Remark 8.2.1.9:

$(2'')$

If $e$ is a morphism of $\operatorname{\mathcal{C}}$ such that $\lambda _{-}(e)$ is an identity morphism of $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$, then $F(e)$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$.

The implication $(2') \Rightarrow (2'')$ is immediate. The reverse implication follows from the observation that if $\lambda _{-}(e)$ is an isomorphism in $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$, then $e$ is isomorphic (as an object of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$) to a morphism $e'$ such that $\lambda _{-}(e')$ is an identity morphism of $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$.

We now complete the proof by showing that $V'$ is a cartesian fibration. Fix an object $(X, F_ X) \in \operatorname{\mathcal{D}}$, and a morphism $u: X' \rightarrow X$ in the $\infty $-category $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$. We wish to show that $u$ can be lifted to a $V'$-cartesian morphism $\widetilde{u}: (X', F_{X'}) \rightarrow (X, F_{X} )$ in the $\infty $-category $\operatorname{\mathcal{D}}$. We will prove a slightly stronger assertion: we can arrange that the image of $\widetilde{u}$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ is $V$-cartesian. Let us identify $u$ with a morphism $\Delta ^1 \rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$ and set $\operatorname{\mathcal{C}}_{u} = \Delta ^1 \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{C}}$, so that $\operatorname{\mathcal{C}}_{X}$ can be identified with the fiber $\{ 1\} \times _{ \Delta ^1} \operatorname{\mathcal{C}}_{u}$. By virtue of Corollary 7.3.7.6, it will suffice to show that the lifting problem

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{X} \ar [r]^-{F_ X} & \operatorname{\mathcal{E}}\ar [d]^{U} \ar [d] \\ \operatorname{\mathcal{C}}_{u} \ar@ {-->}[ur]^{ F_{u} } \ar [r] & \operatorname{\mathcal{C}}_{+} } \]

admits a solution having the property that $F_{u}$ is $U$-right Kan extended from $\operatorname{\mathcal{C}}_ X$.

Let $\pi : \operatorname{\mathcal{C}}_{u} \rightarrow \Delta ^1$ denote the projection map. Since $\pi $ is a pullback of $\lambda _{-}$, it is a cocartesian fibration of $\infty $-categories (Proposition 8.2.1.7). In particular, $\operatorname{\mathcal{C}}_{X}$ is a reflective subcategory of $\operatorname{\mathcal{C}}_{u}$. Moreover, if $C$ is an object of $\operatorname{\mathcal{C}}_{X}$, then a morphism $v: C' \rightarrow C$ in $\operatorname{\mathcal{C}}_{u}$ is $\pi $-cocartesian if and only if it exhibits $C$ as a $\operatorname{\mathcal{C}}_{X}$-reflection of $C'$ (see Proposition 6.2.2.22). By virtue of Corollary 7.3.5.9, it will suffice to show that if this condition is satisfied, then $\lambda _{+}(v)$ can be lifted to a $U$-cartesian morphism $E \rightarrow F_{X}(C)$ in $\operatorname{\mathcal{E}}$. This is clear: our assumption that $v$ is $\pi $-cocartesian guarantees that $\lambda _{+}(v)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{+}$ (Proposition 8.2.1.7), and can therefore be lifted to an isomorphism in $\operatorname{\mathcal{E}}$ by virtue of the fact that $U$ is an isofibration (Proposition 5.1.4.8). $\square$