Kerodon

Proof. Set $f = \overline{f}|_{K}$. Note that the restriction maps

are right fibrations of simplicial sets (Corollary 4.3.6.12). It follows that we can regard the map

of Remark 7.1.6.8 as a functor between $\infty $-categories which are right-fibered over $\operatorname{\mathcal{C}}$. Combining Remark 7.1.6.8 with the criterion of Corollary 5.1.6.4, we see that $\overline{f}$ is a $U$-colimit diagram if and only if, for every object $C \in \operatorname{\mathcal{C}}$, the induced map

is a homotopy equivalence of Kan complexes.

To complete the proof, it will suffice to show that $U'_{C}$ is a homotopy equivalence if and only if the diagram (7.1) is a homotopy pullback square. To see this, we note that Proposition 4.6.5.10 supplies a levelwise homotopy equivalence of (7.1) with the diagram

It will therefore suffice to show that (7.2) is a homotopy pullback square if and only if $U'_{C}$ is a homotopy equivalence (Corollary 3.4.1.12). This is a special case of Example 3.4.1.3, since the horizontal maps in the diagram (7.2) are Kan fibrations (combine Corollaries 4.3.6.12 and 4.4.3.8). $\square$

Proof. We proceed as in the proof of Corollary 7.1.3.14. Let $\operatorname{Isom}(\operatorname{\mathcal{C}})$ denote the full subcategory of $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ spanned by the isomorphisms in $\operatorname{\mathcal{C}}$, and define $\operatorname{Isom}(\operatorname{\mathcal{D}}) \subseteq \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{D}})$ similarly. For $i \in \{ 0,1\} $, the evaluation functors

are trivial Kan fibrations (Corollary 4.4.5.10), and therefore equivalences of $\infty $-categories (Proposition 4.5.3.11). Our assumption that $\overline{u}$ and $\overline{v}$ are isomorphic guarantees that we can choose a diagram $\overline{w}: K^{\triangleleft } \rightarrow \operatorname{Isom}(\operatorname{\mathcal{C}})$ satisfying $\operatorname{ev}_0 \circ \overline{w} = \overline{u}$ and $\operatorname{ev}_1 \circ \overline{w} = \overline{v}$. Applying Remark 7.1.6.6 to the commutative diagram

we see that $\overline{u}$ is a $U$-limit diagram if and only if $\overline{w}$ is a $U'$-limit diagram. A similar argument shows that this is equivalent to the requirement that $\overline{v}$ is a $U$-limit diagram. $\square$

Proof. Apply Remark 7.1.5.6. $\square$

Proof. Combine Proposition 7.1.6.16 with Example 7.1.6.4. $\square$

Proof. Apply Proposition 7.1.6.16 in the case $\operatorname{\mathcal{E}}= \Delta ^{0}$ (and use Example 7.1.6.3). $\square$

Proof. Assume $U$ is a right fibration; we will show that it creates $K$-indexed limits (the analogous statement for left fibrations follows by a similar argument). Let $f: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram and suppose that $U \circ f$ can be extended to a limit diagram $g: K^{\triangleleft } \rightarrow \operatorname{\mathcal{D}}$. Since the inclusion $K \hookrightarrow K^{\triangleleft }$ is right anodyne (Example 4.3.7.10), our assumption that $U$ is a right fibration guarantees that the lifting problem

has a solution. Since $K$ is weakly contractible, the morphism $\overline{f}$ is automatically a $U$-limit diagram (Example 7.1.6.10). Applying Corollary 7.1.6.18, we see that $\overline{f}$ is a limit diagram. $\square$

Proof. Combine Corollary 7.1.6.19 with Proposition 7.1.4.19. $\square$

Proof. Set $f = \overline{f}|_{K}$. By virtue of Corollary 4.3.6.10 and Proposition 5.1.4.20, we can replace (7.3) by the commutative diagram

and thereby reduce to the special case $K = \emptyset $. In this case, the desired result follows from Proposition 7.1.5.19. $\square$

Proof. Apply Proposition 7.1.6.21 in the special case $\operatorname{\mathcal{E}}= \operatorname{\mathcal{D}}$ and $\operatorname{\mathcal{E}}' = \{ D\} $. $\square$

Proof. Assume that condition $(\ast )$ is satisfied; we will show that $\overline{f}$ is a $U$-colimit diagram (the converse follows from Proposition 7.1.6.21). Set $f = \overline{f}|_{K}$. By virtue of Proposition 7.1.6.12, it will suffice to show that for each vertex $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 (7.4) 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 \overline{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}}$. The desired result now follows from $(\ast )$. $\square$