Kerodon

Proof. For each object $D \in \operatorname{\mathcal{D}}$, let $\underline{D} \in \operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleright }, \operatorname{\mathcal{D}})$ denote the constant functor taking the value $D$. By virtue of Proposition 7.1.5.12, the functor $\overline{F}$ is a $U$-colimit diagram if and only if, for each $D \in \operatorname{\mathcal{D}}$, the upper half of the diagram

is a homotopy pullback square. Since $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$, Proposition 7.3.6.7 shows that the right half of the diagram is a homotopy pullback square. It follows that $\overline{F}$ is a $U$-colimit diagram if and only if the outer rectangle of (7.33) is a homotopy pullback square for each $D \in \operatorname{\mathcal{D}}$ (Proposition 3.4.1.11).

Let $v$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$. Let $\operatorname{\mathcal{C}}^{1}$ denote the cone $(\operatorname{\mathcal{C}}^0)^{\triangleright }$, which we regard as a full subcategory of $\operatorname{\mathcal{C}}^{\triangleright }$. Note that the functors $\underline{D}$, $\underline{D}|_{ \operatorname{\mathcal{C}}^{1}}$, $U \circ \underline{D}$ and $U \circ \underline{D}|_{ \operatorname{\mathcal{C}}^{1} }$ are right Kan extended from the cone point, so Corollary 7.3.6.9 implies that the restriction maps

are homotopy equivalences. It follows that the restriction map from the outer rectangle of (7.33) to the diagram

is a levelwise homotopy equivalence. In particular, the outer rectangle of (7.33) is a homotopy pullback square if and only if (7.34) is a homotopy pullback square (Corollary 3.4.1.12). By virtue of Proposition 7.1.5.12, this is satisfied for every object $D \in \operatorname{\mathcal{D}}$ if and only if $F^{1}$ is a $U$-colimit diagram. $\square$

Proof. Apply Proposition 7.3.8.1 in the special case $\operatorname{\mathcal{E}}= \Delta ^0$. $\square$

Proof. Set $C = V(B)$, and let $F_{C}$ denote the composite map

We wish to show that $F_{C}$ is a $U$-colimit diagram if the composite map

is a $U$-colimit diagram. By virtue of Corollary 7.2.2.2, it will suffice to show that the natural map

is right cofinal. By construction, $\theta $ is a pullback of the map $V_{/B}: \operatorname{\mathcal{B}}_{/B} \rightarrow \operatorname{\mathcal{C}}_{ / V(B) }$. Our assumption that $V$ is a right fibration guarantees that $V_{/B}$ is a trivial Kan fibration (Corollary 4.3.7.13). It follows that $\theta $ is also a trivial Kan fibration, and therefore right cofinal by virtue of Corollary 7.2.1.13. $\square$

Proof. Apply Corollary 7.3.8.4 in the special case $\operatorname{\mathcal{E}}= \Delta ^0$. $\square$

Proof of Proposition 7.3.8.6. It follows immediately from the definitions that if $\overline{F}$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^0$, then the functor $F = \overline{F}|_{\operatorname{\mathcal{C}}}$ has the same property. We may therefore assume that condition $(2)$ is satisfied. Fix an object $X \in \overline{\operatorname{\mathcal{C}}}$. We will complete the proof by showing that $\overline{F}$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^0$ at $X$ if and only if it is $U$-left Kan extended from $\operatorname{\mathcal{C}}$ at $X$. Let $\overline{F}_{X}$ denote the composite map

We wish to show that $\overline{F}_{X}$ is a $U$-colimit diagram if and only if its restriction to $(\operatorname{\mathcal{C}}^{0} \times _{\overline{\operatorname{\mathcal{C}}}} \overline{\operatorname{\mathcal{C}}}_{/X})^{\triangleright }$ is a $U$-colimit diagram. Let $F_{X}$ denote the restriction of $\overline{F}_{X}$ to $\operatorname{\mathcal{C}}\times _{\overline{\operatorname{\mathcal{C}}}} \overline{\operatorname{\mathcal{C}}}_{/X}$. By virtue of Proposition 7.3.8.1, it will suffice to show that $F_{X}$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0} \times _{\overline{\operatorname{\mathcal{C}}}} \overline{\operatorname{\mathcal{C}}}_{/X}$. This follows by applying Corollary 7.3.8.4 to the right fibration $\operatorname{\mathcal{C}}\times _{ \overline{\operatorname{\mathcal{C}}} } \overline{\operatorname{\mathcal{C}}}_{/X} \rightarrow \operatorname{\mathcal{C}}$. $\square$

Proof. Apply Proposition 7.3.8.6 in the special case $\operatorname{\mathcal{E}}= \Delta ^0$. $\square$

Proof. Let $\operatorname{\mathcal{C}}^{1} \subseteq \operatorname{\mathcal{C}}$ be the full subcategory spanned by the objects of $\operatorname{\mathcal{C}}^{0}$ together with the object $C$, and let $\operatorname{\mathcal{C}}^{2} \subseteq \operatorname{\mathcal{C}}$ be the full subcategory spanned by the objects of $\operatorname{\mathcal{C}}$ together with the objects $C$ and $C'$. If $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ at $C$, then the functor $F|_{ \operatorname{\mathcal{C}}^{1}}$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$. Since every object of $\operatorname{\mathcal{C}}^{2}$ is isomorphic to an object of $\operatorname{\mathcal{C}}^{1}$. the functor $F|_{ \operatorname{\mathcal{C}}^{2} }$ is automatically $U$-left Kan extended from $\operatorname{\mathcal{C}}^{1}$ (Proposition 7.3.3.7). Applying Proposition 7.3.8.6, we see that $F|_{ \operatorname{\mathcal{C}}^{2} }$ is also $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$. In particular, $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ at the object $C' \in \operatorname{\mathcal{C}}^{2}$. $\square$

Proof. Note that the restriction maps

are left fibrations of simplicial sets (Corollary 4.3.6.11). It follows that we can regard $\theta $ as a functor of $\infty $-categories which are left-fibered over $\operatorname{\mathcal{D}}$. Consequently, to show that $\theta $ is an equivalence of $\infty $-categories, it will suffice to show that for every object $D \in \operatorname{\mathcal{D}}$, the commutative diagram

induces a homotopy equivalence of Kan complexes

Note that the horizontal maps in the diagram (7.35) are left fibrations between Kan complexes (Corollary 4.3.6.11), and therefore Kan fibrations (Corollary 4.4.3.8). We are therefore reduced to showing that the diagram (7.35) is a homotopy pullback square (Example 3.4.1.3).

Let $\underline{D} \in \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ denote the constant functor taking the value $D$. Using Theorem 4.6.4.17, we obtain a (termwise) homotopy equivalence from (7.35) to the diagram of morphism spaces

Using Corollary 3.4.1.12, we are reduced to showing that the diagram (7.36) is a homotopy pullback square, which is a special case of Proposition 7.3.6.7. $\square$

Proof. It follows from Proposition 4.3.6.8 that $\theta $ is a left fibration, and therefore an isofibration (Example 4.4.1.11). By virtue of Proposition 4.5.5.20, it will suffice to show that $\theta $ is an equivalence of $\infty $-categories, which follows from Proposition 7.3.8.10. $\square$

Proof. Apply Corollary 7.3.8.11 in the special case $\operatorname{\mathcal{E}}= \Delta ^{0}$. $\square$

Proof. The implication $(1) \Rightarrow (2)$ follows immediately from Proposition 7.3.8.1. For the converse, suppose that $\overline{F}_0: ( \operatorname{\mathcal{C}}^{0} )^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ is a $U$-colimit diagram which solves the lifting problem (7.38). Applying Corollary 7.3.8.11, we see that $\overline{F}_0$ can be extended to a functor $\overline{F}: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ which solves the lifting problem (7.37). It then follows from Proposition 7.3.8.1 that $\overline{F}$ is a $U$-colimit diagram. $\square$

Proof. Apply Corollary 7.3.8.13 in the special case $\operatorname{\mathcal{E}}= \Delta ^0$. $\square$

Proof. The implication $(1) \Rightarrow (2)$ follows immediately from Proposition 7.3.8.6. For the converse, assume that $(2)$ is satisfied. To prove $(1)$, it will suffice to show that for each object $C \in \overline{\operatorname{\mathcal{C}}}$, the induced lifting problem

admits a solution $\overline{F}_{C}: ( \operatorname{\mathcal{C}}_{/C})^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ which is a $U$-colimit diagram (Proposition 7.3.5.5). Arguing as in the proof of Proposition 7.3.8.6, we see that $F_{C}$ is $U$-left Kan extended from the full subcategory $\operatorname{\mathcal{C}}^{0}_{/C} \subseteq \operatorname{\mathcal{C}}_{/C}$. Let $F_{C}^{0}$ denote the restriction of $F_{C}$ to the subcategory $\operatorname{\mathcal{C}}^{0}_{/C} \subseteq \operatorname{\mathcal{C}}_{/C}$. By virtue of Corollary 7.3.8.13, it will suffice to show that the induced lifting problem

has a solution $\overline{F}^{0}_{C}: (\operatorname{\mathcal{C}}^{0}_{/C})^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ which is a $U$-colimit diagram, which follows immediately from assumption $(2)$. $\square$

Proof. Apply Proposition 7.3.8.16 in the special case $\operatorname{\mathcal{E}}= \Delta ^0$. $\square$

Proof. Let $\operatorname{\mathcal{C}}$ denote the iterated relative join $(\operatorname{\mathcal{C}}_0 \star _{\operatorname{\mathcal{C}}_1} \operatorname{\mathcal{C}}_1) \star _{\operatorname{\mathcal{C}}_2} \operatorname{\mathcal{C}}_2$, so that we have a cocartesian fibration of $\infty $-categories $\pi : \operatorname{\mathcal{C}}\rightarrow \Delta ^2$ having fibers $\pi ^{-1} \{ i\} = \operatorname{\mathcal{C}}_ i$ for $0 \leq i \leq 2$ (see Lemma 5.2.3.17). For $0 \leq i < j \leq 2$, let $\operatorname{\mathcal{C}}_{ij}$ denote the fiber product $\operatorname{N}_{\bullet }( \{ i < j \} ) \times _{\Delta ^2} \operatorname{\mathcal{C}}$, which we will identify with $\operatorname{\mathcal{C}}_{i} \star _{\operatorname{\mathcal{C}}_ j} \operatorname{\mathcal{C}}_ j$. By virtue of Remark 7.3.1.9, we are free to replace $\alpha $ and $\beta $ by homotopic natural transformations. We can therefore assume that there exist functors

satisfying $F_{01}|_{\operatorname{\mathcal{C}}_0} = F_0$, $F_{01}|_{\operatorname{\mathcal{C}}_1} = F_1 = F_{12}|_{\operatorname{\mathcal{C}}_1}$, and $F_{12}|_{\operatorname{\mathcal{C}}_2} = F_2$, where $\alpha $ and $\beta $ are given by the composite maps

(see Warning 7.3.2.12). Note that $F_{01}$ and $F_{12}$ can be amalgamated to a morphism of simplicial sets $F': \Lambda ^{2}_{1} \times _{\Delta ^1} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. Since $\pi $ is a cocartesian fibration, the inclusion map $\Lambda ^{2}_{1} \times _{\Delta ^1} \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}$ is a categorical equivalence (Proposition 5.3.6.1). Applying Lemma 4.5.5.2, we can extend $F'$ to a functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$.

Let $F_{02}$ denote the restriction of $F$ to $\operatorname{\mathcal{C}}_{02}$, and let $\gamma : F_0 \rightarrow F_2 \circ H \circ G$ denote the natural transformation given by the composite map

Note that the composite map

can be regarded as a $2$-simplex of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{D}})$, which witnesses $\gamma $ as a composition of $\alpha $ with $\beta |_{\operatorname{\mathcal{C}}_0}$. Applying Proposition 7.3.2.11, we see that $(1)$ and $(2)$ can be reformulated as follows:

$(1')$

The functor $F_{12}: \operatorname{\mathcal{C}}_{12} \rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{C}}_1$.

$(2')$

The functor $F_{02}: \operatorname{\mathcal{C}}_{02} \rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{C}}_0$.

By assumption, the natural transformation $\alpha $ exhibits $F_1$ as a left Kan extension of $F_0$ along $G$. Applying Proposition 7.3.2.11, we see that the functor $F_{01}$ is left Kan extended from $\operatorname{\mathcal{C}}_0$. In particular, $F$ is left Kan extended from $\operatorname{\mathcal{C}}^0$ at every object of the full subcategory $\operatorname{\mathcal{C}}_1 \subseteq \operatorname{\mathcal{C}}$. It follows that $(2')$ is equivalent to the following:

$(2'')$

The functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{C}}_0$.

Using Corollary 7.3.8.8, we see that $(2'')$ is equivalent to the following:

$(1'')$

The functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{C}}_{01}$.

To complete the proof, it will suffice to show that conditions $(1')$ and $(1'')$ are equivalent. We will prove something slightly more precise: for every object $X \in \operatorname{\mathcal{C}}_2$, the conditions are equivalent:

$(1'_ X)$

The functor $F_{12}: \operatorname{\mathcal{C}}_{12} \rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{C}}_1$ at $X$.

$(1''_{X})$

The functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{C}}_{01}$ at $X$.

Let us regard the object $X$ as fixed, and let $F_{X}$ denote the composite map

We wish to show that $F_{X}$ is a colimit diagram in $\operatorname{\mathcal{D}}$ if and only if its restriction to $( \operatorname{\mathcal{C}}_1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/X} )^{\triangleright }$ is a colimit diagram in $\operatorname{\mathcal{D}}$. By virtue of Corollary 7.2.2.3, it will suffice to show that the inclusion map $\operatorname{\mathcal{C}}_1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/X} \hookrightarrow \operatorname{\mathcal{C}}_{01} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/X}$ is right cofinal. This follows by applying Proposition 7.2.3.12 to the upper square of the pullback diagram

where $\pi '$ denotes the composite map $\operatorname{\mathcal{C}}_{/X} \rightarrow \operatorname{\mathcal{C}}\rightarrow \Delta ^2$ (which is a cocartesian fibration by virtue of Proposition 5.1.4.19). $\square$

Proof. The implication $(1) \Rightarrow (2)$ is immediate from Proposition 7.3.8.18. To prove the converse, assume that $(2)$ is satisfied. Define $\operatorname{\mathcal{C}}$ as in the proof of Proposition 7.3.8.18. Using the criterion of Corollary 7.3.5.8, we see that $F_0$ admits a left Kan extension $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. It follows from Proposition 7.3.2.11 that $F|_{ \operatorname{\mathcal{C}}_1 }$ is a left Kan extension of $F_0$ along $G$, and is therefore isomorphic to $F_1$ (Remark 7.3.6.6). We may therefore assume without loss of generality that $F_1 = F|_{\operatorname{\mathcal{C}}_1}$ (Remark 7.3.1.10). We will complete the proof by showing that $F_{12} = F|_{\operatorname{\mathcal{C}}_{12}}$ is left Kan extended from $\operatorname{\mathcal{C}}_{1}$, and therefore exhibits $F|_{\operatorname{\mathcal{C}}_2}$ as a left Kan extension of $F_1$ along $H$ (Proposition 7.3.2.11).

Fix an object $X \in \operatorname{\mathcal{C}}_2$, and let $F_{X}$ denote the composite map

We wish to show that the composite map

is a colimit diagram in $\operatorname{\mathcal{D}}$. As in the proof of Proposition 7.3.8.18, the inclusion map $\operatorname{\mathcal{C}}_1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/X} \hookrightarrow \operatorname{\mathcal{C}}_{01} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/X}$ is right cofinal. It will therefore suffice to show that $F_{X}$ is a colimit diagram in $\operatorname{\mathcal{D}}$ (Corollary 7.2.2.3). This is clear: by construction, the functor $F$ is left Kan extended from the full subcategory $\operatorname{\mathcal{C}}_0 \subseteq \operatorname{\mathcal{C}}$, and is therefore also left Kan extended from the larger subcategory $\operatorname{\mathcal{C}}_{01} \subseteq \operatorname{\mathcal{C}}$ (Proposition 7.3.8.6). $\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. Since $\operatorname{\mathcal{C}}$ is an $\infty $-category, we extend $\delta $ and $F_0$ to functors $\overline{\delta }: \operatorname{\mathcal{K}}\rightarrow \operatorname{\mathcal{C}}$ and $\overline{F}_0: \operatorname{\mathcal{K}}\rightarrow \operatorname{\mathcal{D}}$, respectively. Similarly, we can extend $\alpha $ to a natural transformation $\overline{\alpha }: \overline{F}_0 \rightarrow F \circ \overline{\delta }$. It follows from Proposition 7.3.1.14 that we $\overline{\alpha }$ exhibits $F$ as a left Kan extension of $\overline{F}_0$ along $\overline{\delta }$. We may therefore replace $K$ by $\operatorname{\mathcal{K}}$ and thereby reduce to proving Corollary 7.3.8.20 in the special case where $K$ is an $\infty $-category. In this case, assertion $(1)$ is a special case of Proposition 7.3.8.19, and assertion $(2)$ is a special case of Proposition 7.3.8.18 (see Example 7.3.1.7). $\square$