# Kerodon

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

Proposition 7.2.2.9. Suppose we are given a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ B \ar [r]^-{ f } \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{U} \\ B^{\triangleleft } \ar [r]^-{ \overline{g} } & \operatorname{\mathcal{D}}, }$

where $U$ is an inner fibration of $\infty$-categories. Let $e: A \rightarrow B$ be a left cofinal morphism of simplicial sets. The following conditions are equivalent:

$(1)$

There exists a $U$-limit diagram $\overline{f}: B^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ satisfying $\overline{f}|_{B} = f$ and $U \circ \overline{f} = \overline{g}$.

$(2)$

There exists a $U$-limit diagram $\overline{f}_0: A^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ satisfying $\overline{f}_0|_{A} = f \circ e$ and $U \circ \overline{f}_0 = \overline{g} \circ e^{\triangleleft }$.

Proof. The implication $(1) \Rightarrow (2)$ follows by observing that if $\overline{f}: B^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ is a $U$-limit diagram, then the left cofinality of $e$ guarantees that $\overline{f} \circ e^{\triangleleft }$ is also a $U$-limit diagram (Corollary 7.2.2.2). We will complete the proof by showing that $(2)$ implies $(1)$. By virtue of Corollary 7.2.1.15, we can assume that the morphism $e$ is either left anodyne or a trivial Kan fibration. We first treat the case where $e$ is a trivial Kan fibration. Let $s: B \rightarrow A$ be a section of $e$, and let $\overline{f}_0: A^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ satisfy the requirements of $(2)$. Let $\overline{f}$ denote the composite map

$B^{\triangleleft } \xrightarrow { s^{\triangleleft } } A^{\triangleleft } \xrightarrow { \overline{f}_0 } \operatorname{\mathcal{C}}.$

It follows immediately from the construction that $\overline{f}|_{B} = f$ and $U \circ \overline{f} = \overline{g}$. Moreover, the composition $\overline{f} \circ e^{\triangleleft }$ is isomorphic to $\overline{f}_0$ (as an object of the $\infty$-category $\operatorname{Fun}( B^{\triangleleft }, \operatorname{\mathcal{C}})$), and is therefore also a $U$-limit diagram (Proposition 7.1.5.13). Since $e$ is left cofinal, it follows that $\overline{f}$ is also a $U$-limit diagram (Corollary 7.2.2.2).

We now treat the case where $e$ is left anodyne. In this case, the induced map $A^{\triangleleft } \coprod _{A} B \hookrightarrow B^{\triangleleft }$ is inner anodyne. Since $U$ is an inner fibration, we can extend $f$ to a morphism $\overline{f}: B^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ satisfying $U \circ \overline{f} = \overline{g}$ and $\overline{f} \circ e^{\triangleleft } = \overline{f}_0$. Since $e$ is left cofinal, the morphism $\overline{f}$ is automatically a $U$-limit diagram (Corollary 7.2.2.2). $\square$