# Kerodon

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

Corollary 5.5.4.2. Let $\operatorname{\mathcal{C}}$ be an $(\infty ,2)$-category, let $f: K \rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets, and let $q: \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}$ denote the projection map. Let $u: X \rightarrow Y$ be a morphism in the $(\infty ,2)$-category $\operatorname{\mathcal{C}}_{/f}$. The following conditions are equivalent:

$(1)$

For every vertex $z \in K$, the composite map

$\Delta ^2 \simeq \Delta ^1 \star \{ z\} \hookrightarrow \Delta ^1 \star K \xrightarrow {u} \operatorname{\mathcal{C}}$

is a thin $2$-simplex of $\operatorname{\mathcal{C}}$.

$(2)$

The morphism $u$ is $q$-cartesian.

$(3)$

The morphism $u$ is locally $q$-cartesian.

Proof. The implication $(1) \Rightarrow (2)$ follows from Proposition 5.5.3.8, and the implication $(2) \Rightarrow (3)$ is immediate (see Remark 5.1.3.3). We will show that $(3) \Rightarrow (1)$. Fix a vertex $z \in K$; we wish to show that the composite map

$\Delta ^2 \simeq \Delta ^1 \star \{ z\} \hookrightarrow \Delta ^1 \star K \xrightarrow {u} \operatorname{\mathcal{C}}$

is a thin $2$-simplex of $\operatorname{\mathcal{C}}$. Set $Z = f(z) \in \operatorname{\mathcal{C}}$, so that $q$ factors as a composition

$\operatorname{\mathcal{C}}_{/f} \xrightarrow {q'} \operatorname{\mathcal{C}}_{/Z} \xrightarrow {q''} \operatorname{\mathcal{C}}.$

By virtue of Theorem 5.5.4.1, it will suffice to show that the $q'( u )$ is a locally $q''$-cartesian morphism of the $(\infty ,2)$-category $\operatorname{\mathcal{C}}_{/Z}$.

Set $\overline{u} = q(u)$, which we regard as a morphism $\overline{q}: \overline{X} \rightarrow \overline{Y}$ in the $(\infty ,2)$-category $\operatorname{\mathcal{C}}$. By virtue of Proposition 5.5.3.9, we can lift $\overline{u}$ to a morphism $u': X' \rightarrow Y$ in $\operatorname{\mathcal{C}}_{/f}$ which satisfies condition $(1)$ (and therefore also satisfies $(3)$). Regard $\overline{u}$ as a $1$-simplex of $\operatorname{\mathcal{C}}$ and let $\operatorname{\mathcal{E}}$ denote the fiber product $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f}$. Since $q$ is an interior fibration (Proposition 5.5.3.1), the projection map $\pi : \operatorname{\mathcal{E}}\rightarrow \Delta ^1$ is also an interior fibration (Remark 5.5.2.4) and therefore an inner fibration (Example 5.5.2.2). Let us abuse notation by identifying $u$ and $u'$ with morphisms in the $\infty$-category $\operatorname{\mathcal{E}}$ lying over the unique nondegenerate edge of $\Delta ^1$. Assumption $(3)$ then guarantees that $u$ and $u'$ are $\pi$-cartesian. Invoking Remark 5.1.3.8, we deduce that there exists a $2$-simplex $\rho : \Delta ^2 \rightarrow \operatorname{\mathcal{E}}$, which we display as a diagram

$\xymatrix@R =50pt@C=50pt{ & X' \ar [dr]^{u'} & \\ X \ar [ur]^{v} \ar [rr]^-{u} & & Y, }$

where $v$ is an isomorphism in the $\infty$-category $\{ 0\} \times _{\Delta ^1} \operatorname{\mathcal{E}}\simeq \{ \overline{X} \} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f}$. It follows that $q'(v)$ is an isomorphism in the $\infty$-category $\{ \overline{X} \} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z}$. Since $u'$ satisfies condition $(1)$, Theorem 5.5.4.1 guarantees that $q'(u')$ is locally $q''$-cartesian. Invoking Remark 5.1.3.8 again, we deduce that $q'(u)$ is locally $q''$-cartesian, as desired. $\square$