Kerodon

Proof. Using Corollary 4.1.3.3, we can choose an inner anodyne morphism $i: K \hookrightarrow \operatorname{\mathcal{K}}$, where $\operatorname{\mathcal{K}}$ is an $\infty $-category. It follows that the induced map $i^{\triangleright }: K^{\triangleright } \hookrightarrow \operatorname{\mathcal{K}}^{\triangleright }$ is also inner anodyne (Example 4.3.6.7), so that the restriction map $\operatorname{Fun}( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}})$ is a trivial Kan fibration of simplicial sets (Proposition 1.5.7.6). We can therefore lift $\alpha $ to a natural transformation $\overline{\alpha }: \overline{F}_0 \rightarrow \overline{F}_1$ between natural transformations $\overline{F}_0, \overline{F}_1: \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$. Since $i^{\triangleright }$ is bijective on vertices, the natural transformation $\overline{\alpha }$ carries each object of $\operatorname{\mathcal{K}}^{\triangleright }$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$. The morphism $i^{\triangleright }$ is right cofinal (Corollary 7.2.1.13), so Corollary 7.2.2.2 guarantees that $F_0$ is a $U$-colimit diagram if and only if $\overline{F}_0$ is a $U$-colimit diagram. Similarly, $F_1$ is a $U$-colimit diagram if and only if $\overline{F}_1$ is a $U$-colimit diagram. We may therefore replace $\alpha $ by $\overline{\alpha }$ in the statement of Proposition 7.3.9.1, and thereby reduce to the case where $K = \operatorname{\mathcal{K}}$ is an $\infty $-category.

Let us identify $\alpha $ with a functor of $\infty $-categories $F: \Delta ^1 \times \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$. For each object $x \in \operatorname{\mathcal{K}}^{\triangleright }$, we can regard $\Delta ^1 \times \{ x\} $ with a morphism $e_{x}: (0,x) \rightarrow (1,x)$ in the $\infty $-category $\Delta ^1 \times \operatorname{\mathcal{K}}^{\triangleright }$. By construction, the functor $F$ carries each $e_{x}$ to the $U$-cocartesian morphism $\alpha _ x$ of $\operatorname{\mathcal{C}}$. By virtue of Proposition 4.6.7.22, $e_{x}$ is final when viewed as an object of the $\infty $-category

so that $F$ is $U$-left Kan extended from $\{ 0\} \times \operatorname{\mathcal{K}}^{\triangleright }$ at $(1,x)$ (Corollary 7.2.2.5). Allowing the object $x$ to vary, we see that the functor $F$ is $U$-left Kan extended from $\{ 0\} \times \operatorname{\mathcal{K}}^{\triangleright }$.

We now prove $(1)$. Suppose that $F_0$ is a $U$-colimit diagram. Then $F_0$ is $U$-left Kan extended from $\operatorname{\mathcal{K}}$ (Example 7.3.3.9). Applying Proposition 7.3.8.6, we see that the functor $F$ is $U$-left Kan extended from $\{ 0\} \times \operatorname{\mathcal{K}}$, and therefore from the larger subcategory $\Delta ^1 \times \operatorname{\mathcal{K}}\subseteq \Delta ^1 \times \operatorname{\mathcal{K}}^{\triangleright }$. It follows that the composite map

is a $U$-colimit diagram. Since the inclusion map $\{ 1\} \times \operatorname{\mathcal{K}}\hookrightarrow \Delta ^1 \times \operatorname{\mathcal{K}}$ is right cofinal (Proposition 7.2.1.3), Corollary 7.2.2.2 guarantees that $F_1 = F|_{ \{ 1\} \times \operatorname{\mathcal{K}}^{\triangleright } }$ is also a $U$-colimit diagram.

We now prove $(2)$. Let $\pi : \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \Delta ^1$ be the functor carrying $\operatorname{\mathcal{K}}$ to the vertex $0 \in \Delta ^1$ and the cone point $v \in \operatorname{\mathcal{K}}^{\triangleright }$ to the vertex $1 \in \Delta ^1$, and let $G: \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ be the functor given by the composition

Note that there is a natural transformation $\beta : F_0 \rightarrow G$ which is the identity when restricted to $\operatorname{\mathcal{K}}$ and which carries the cone point $v$ to the morphism $\alpha _{v}: F_0(v) \rightarrow F_1(v) = G(v)$. If $\alpha _{v}$ is an isomorphism, then the natural transformation $\beta $ is also an isomorphism (Theorem 4.4.4.4). Consequently, to show that $F_0$ is a $U$-colimit diagram, it will suffice to show that $G$ is a $U$-colimit diagram (Proposition 7.1.5.13). Arguing as above, we see that the functor $F|_{ \Delta ^1 \times \operatorname{\mathcal{K}}}$ is $U$-left Kan extended from the full subcategory $\{ 0\} \times \operatorname{\mathcal{K}}\subseteq \Delta ^1 \times \operatorname{\mathcal{K}}$. Applying Proposition 7.3.8.1, we see that $G$ is a $U$-colimit diagram if and only if the composite map

is a $U$-colimit diagram. By virtue of Corollary 7.2.2.2, this is equivalent to the requirement that $F_1$ is a $U$-colimit diagram. $\square$

Proof of Proposition 7.3.9.2. For every morphism $e: D \rightarrow D'$ in $\operatorname{\mathcal{D}}$, we can choose a natural transformation $\alpha : f \rightarrow e_{!} \circ f$ carrying each vertex of $K^{\triangleright }$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$. It follows from Proposition 7.3.9.1 that if $f$ is a $U$-colimit diagram, then $e_{!} \circ f$ is also a $U$-colimit diagram, and therefore a colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}_{D'}$ (Corollary 7.1.5.20). This proves the necessity of condition $(\ast )$. For the converse, suppose that $f$ satisfies condition $(\ast )$; we wish to show that $f$ is a $U$-colimit diagram. By virtue of Proposition 7.1.5.12, this is equivalent to the assertion that for every object $C \in \operatorname{\mathcal{C}}$, the diagram of Kan complexes

is a homotopy pullback square, where $\underline{C} \in \operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}})$ is the constant diagram taking the value $C$. Since $U$ is an inner fibration, the vertical maps in this diagram are Kan fibrations (Proposition 4.6.1.21 and Corollary 4.1.4.3). Using the criterion of Example 3.4.1.4, it will suffice to show that for every vertex $u \in \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}}) }( U \circ f, U \circ \underline{C} )$, the induced map

is a homotopy equivalence of Kan complexes. Set $D' = U(C)$, so that $u$ can be identified with a morphism of simplicial sets $K^{\triangleright } \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( D, D' )$, and the condition that $\theta _ u$ is a homotopy equivalence depends only on the homotopy class of $u$. Since the simplicial set $K^{\triangleright }$ is weakly contractible (Example 4.3.7.11), we may assume without loss of generality that $u: K^{\triangleright } \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( D, D' )$ is the constant map taking the value $e$, for some morphism $e: D \rightarrow D'$ in $\operatorname{\mathcal{D}}$. In this case, we can use Proposition 5.1.3.11 to replace $\theta _{u}$ by the restriction map

which is a homotopy equivalence by virtue of assumption $(\ast )$ (see Proposition 7.1.5.12). $\square$

Proof. Without loss of generality, we may assume that $f$ carries each edge of $K$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$. Let $\pi : \Delta ^1 \times K^{\triangleright } \rightarrow K^{\triangleright }$ be the morphism which is the identity on $\{ 0\} \times K^{\triangleright }$ and which carries $\{ 1\} \times K^{\triangleright }$ to the cone point $v \in K^{\triangleright }$. Set $C = f(v) \in \operatorname{\mathcal{C}}$ and $D = U(C) \in \operatorname{\mathcal{D}}$. Proposition 5.2.1.3 guarantees that the lifting problem

admits a solution $\alpha : \Delta ^1 \times K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ which carries $\Delta ^1 \times \{ x\} $ to a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$, for each vertex $x \in K^{\triangleright }$. Set $\overline{g} = \alpha |_{ \{ 1\} \times K^{\triangleright }}$, which we regard as a morphism from $K^{\triangleright }$ to the $\infty $-category $\operatorname{\mathcal{C}}_{D}$, and let us identify $\alpha $ with a natural transformation from $\overline{f}$ to $\overline{g}$. Note that $\alpha _{v}: \overline{f}(v) \rightarrow \overline{g}(v)$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$ satisfying $U(\alpha _ v) = \operatorname{id}_{D}$, and is therefore an isomorphism (Proposition 5.1.1.8). Applying Proposition 7.3.9.1, we can reformulate $(2)$ as follows:

$(2')$

The morphism $\overline{g}: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D}$ is a $U$-colimit diagram in $\operatorname{\mathcal{C}}$.

Set $g = \overline{g}|_{K}$. For every edge $u: x \rightarrow y$ of $K$, we have a commutative diagram

where $f(u)$, $\alpha _ x$, and $\alpha _ y$ are $U$-cocartesian. Applying Corollary 5.1.2.4, we deduce that $g(u)$ is $U$-cocartesian when viewed as a morphism of $\operatorname{\mathcal{C}}$, and is therefore an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{D}$ (Proposition 5.1.1.8). Similarly, for every vertex $x \in K$, the unique edge $c_{x}: x \rightarrow v$ of $K^{\triangleright }$ determines a commutative diagram

where $\alpha _{x}$ is $U$-cocartesian and $\alpha _{v}$ is an isomorphism. Combining Corollary 5.1.2.4, Corollary 5.1.2.5, and Proposition 5.1.1.8, we see that $\overline{f}(c_ x)$ is $U$-cocartesian if and only if $\overline{g}(c_ x)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{D}$. We can therefore reformulate condition $(1)$ as follows:

$(1')$

The diagram $\overline{g}$ carries each edge of $K^{\triangleright }$ to an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{D}$.

By virtue of Corollary 7.2.3.5, $(1')$ is equivalent to the requirement that $\overline{g}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}_{D}$. In particular, the implication $(2') \Rightarrow (1')$ follows from Corollary 7.1.5.20. To prove the converse, it will suffice to show that condition $(1')$ is satisfied, then for every morphism $e: D \rightarrow D'$ in $\operatorname{\mathcal{D}}$, the covariant transport functor $e_{!}: \operatorname{\mathcal{C}}_{D} \rightarrow \operatorname{\mathcal{C}}_{D'}$ carries $\overline{g}$ to a colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}_{D'}$ (Proposition 7.3.9.2). This follows immediately from Corollary 7.2.3.5 (applied to the composite diagram $K^{\triangleleft } \xrightarrow { \overline{g} } \operatorname{\mathcal{C}}_{D} \xrightarrow { e_{!} } \operatorname{\mathcal{C}}_{D'}$). $\square$

Proof. The existence (and essential uniqueness) of the diagram $f_1$ and the natural transformation $\alpha : f_0 \rightarrow f_1$ follow from Proposition 5.2.1.3. Let us first show that conditions $(1)$ and $(2)$ are necessary. Suppose that the lifting problem (7.44) admits a solution $\overline{f}_0: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ which is a $U$-colimit diagram. Using Proposition 5.2.1.3, we can extend $f_1$ to a diagram $\overline{f}_1: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D}$ and $\alpha $ to a natural transformation $\overline{\alpha }: \overline{f}_0 \rightarrow \overline{f}_1$ which carries each vertex $x \in K^{\triangleright }$ to a $U$-cocartesian morphism $\overline{\alpha }_ x: \overline{f}_0(x) \rightarrow \overline{f}_1(x)$. Proposition 7.3.9.1 guarantees that $\overline{f}_{1}$ is a $U$-colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}$, and therefore satisfies conditions $(1)$ and $(2)$ by virtue of Proposition 7.3.9.2.

Now suppose that conditions $(1)$ and $(2)$ are satisfied. Let $\overline{f}_1: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D}$ be a colimit diagram extending $f_1$. It follows from $(2)$ that $\overline{f}_1$ is a $U$-colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}$. Let $\pi : ( \Delta ^1 \times K )^{\triangleright } \rightarrow K^{\triangleright }$ denote the morphism which is the identity when restricted to $\{ 0\} \times K$, and which carries $(\{ 1\} \times K)^{\triangleright }$ to the cone point of $K^{\triangleright }$. Since the inclusion map $\{ 1 \} \times K \hookrightarrow \Delta ^1 \times K$ is right cofinal (Proposition 7.2.1.3), Proposition 7.2.2.9 guarantees that the lifting problem

admits a solution $\overline{\alpha }: (\Delta ^1 \times K)^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ which is a $U$-colimit diagram. Note that in this case $\overline{f}'_1 = \overline{\alpha }|_{ (\{ 1\} \times K)^{\triangleright } }$ is also a $U$-colimit diagram (Corollary 7.2.2.2). Setting $\overline{f}_0 = \overline{\alpha }|_{ (\{ 0\} \times K)^{\triangleright } }$, we note that $\overline{\alpha }$ determines a natural transformation of functors $\overline{f}_0 \rightarrow \overline{f}'_1$ which carries each vertex of $x$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$ and carries the cone point to an identity morphism of $\operatorname{\mathcal{C}}$. Applying the criterion of Proposition 7.3.9.1, we conclude that $\overline{f}_0$ is a $U$-colimit diagram which solves the lifting problem (7.44). $\square$

Proof. The implication $(1) \Rightarrow (2)$ follows immediately from Proposition 7.3.9.5. Conversely, suppose that $(2)$ is satisfied. For each object $D \in \operatorname{\mathcal{D}}$, condition $(2)$ guarantees that every diagram $f: K \rightarrow \operatorname{\mathcal{C}}_{D}$ admits an extension $\overline{f}: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D}$ which is a $U$-colimit diagram in $\operatorname{\mathcal{C}}$. In particular, $\overline{f}$ is a colimit diagram in $\operatorname{\mathcal{C}}_{D}$ (Corollary 7.1.5.20) having the property that for every morphism $e: D \rightarrow D'$ in $\operatorname{\mathcal{D}}$, the composition $e_{!} \circ \overline{f}$ is a colimit diagram in $\operatorname{\mathcal{C}}_{D'}$ (Proposition 7.3.9.2). To complete the proof, we observe that if $\overline{f}': K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D}$ is any other colimit diagram satisfying $\overline{f}'|_{K} = f$, then $\overline{f}'$ is isomorphic to $\overline{f}$ as an object of the $\infty $-category $\operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}}_{D} )$, so that $e_{!} \circ \overline{f}'$ is also a colimit diagram in $\operatorname{\mathcal{C}}_{D'}$ (Corollary 7.1.2.14). $\square$

Proof. Combine Proposition 7.3.5.5 with Corollary 7.3.9.6. $\square$