Kerodon

Proof. Combine Propositions 7.3.5.5 and 7.3.9.1. $\square$

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{D}}) \rightarrow \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{E}})$ 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.3, 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{D}}$. 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{D}}$. By virtue of Proposition 4.7.3.20, $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.12, 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{D}}$ 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.6.9). 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. Without loss of generality, we may assume that $f$ carries each edge of $K$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{D}}$. 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 $D = f(v) \in \operatorname{\mathcal{D}}$ and $E = U(D) \in \operatorname{\mathcal{E}}$. Proposition 5.2.1.3 guarantees that the lifting problem

admits a solution $\alpha : \Delta ^1 \times K^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ which carries $\Delta ^1 \times \{ x\} $ to a $U$-cocartesian morphism of $\operatorname{\mathcal{D}}$, 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{D}}_{E}$, 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}_{E}$, and is therefore an isomorphism (Proposition 5.1.1.9). Applying Proposition 7.3.9.3, we can reformulate $(2)$ as follows:

$(2')$

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

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

in the $\infty $-category $\operatorname{\mathcal{D}}$ where the morphisms $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{D}}$, and is therefore an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}_{E}$ (Proposition 5.1.1.9). 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.9, 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{D}}_{E}$. 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{D}}_{E}$.

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{D}}_{E}$. In particular, the implication $(2') \Rightarrow (1')$ follows from Corollary 7.1.7.8. To prove the converse, it will suffice to show that condition $(1')$ is satisfied, then for every morphism $u: E \rightarrow E'$ in $\operatorname{\mathcal{E}}$, the covariant transport functor $u_{!}: \operatorname{\mathcal{D}}_{E} \rightarrow \operatorname{\mathcal{D}}_{E'}$ carries $\overline{g}$ to a colimit diagram in the $\infty $-category $\operatorname{\mathcal{D}}_{E'}$ (Corollary 7.1.7.16). This follows immediately from Corollary 7.2.3.5 (applied to the composite diagram $K^{\triangleleft } \xrightarrow { \overline{g} } \operatorname{\mathcal{D}}_{E} \xrightarrow { u_{!} } \operatorname{\mathcal{D}}_{E'}$). $\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.52) admits a solution $\overline{f}_0: K^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ 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{D}}_{E}$ 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.3 guarantees that $\overline{f}_{1}$ is a $U$-colimit diagram in the $\infty $-category $\operatorname{\mathcal{D}}$, and therefore satisfies conditions $(1)$ and $(2)$ by virtue of Corollary 7.1.7.16.

Now suppose that conditions $(1)$ and $(2)$ are satisfied. Let $\overline{f}_1: K^{\triangleright } \rightarrow \operatorname{\mathcal{D}}_{E}$ 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{D}}$. 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{D}}$ 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{D}}$ and carries the cone point to an identity morphism of $\operatorname{\mathcal{D}}$. Applying the criterion of Proposition 7.3.9.3, we conclude that $\overline{f}_0$ is a $U$-colimit diagram which solves the lifting problem (7.52). $\square$