Kerodon

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

Remark 7.7.1.11. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $K$ be a simplicial set, and suppose we are given a diagram $\sigma :$

\[ \xymatrix { \mathscr {F} \ar [d]^{\gamma } \ar [d] & \mathscr {F}' \ar [d]^{\gamma '} \\ \mathscr {G} \ar [r] & \mathscr {G}' } \]

in the $\infty $-category $\operatorname{Fun}(K, \operatorname{\mathcal{C}})$ which is a levelwise pullback square: that is, for each vertex $x \in K$, the induced diagram $\sigma _{x}:$

\[ \xymatrix { \mathscr {F}(x) \ar [d]^{\gamma _ x} \ar [r] & \mathscr {F}'(x) \ar [d]^{\gamma '_{x}} \\ \mathscr {G}(x) \ar [r] & \mathscr {G}'(x) } \]

is a pullback square in the $\infty $-category $\operatorname{\mathcal{C}}$. If the natural transformation $\gamma '$ is cartesian, then the natural transformation $\gamma $ is also cartesian. To prove this, we must show that for each edge $e: x \rightarrow y$ of $K$, the left side of the diagram

\[ \xymatrix { \mathscr {F}(x) \ar [r]^{\mathscr {F}(x)} \ar [d]^{ \gamma _{x} } & \mathscr {F}(y) \ar [r] \ar [d]^{ \gamma _{y} } & \mathscr {F}'(y) \ar [d]^{ \gamma '_{y} } \\ \mathscr {G}(x) \ar [r]^{ \mathscr {G}(e) } & \mathscr {G}(y) \ar [r] & \mathscr {G}'(y) } \]

is a pullback square. Since the right side is a pullback square by virtue of our hypothesis on $\sigma $, this is equivalent to the requirement that the outer rectangle is a pullback square (Proposition 7.6.2.28). This also appears as the outer rectangle in a commutative diagram

\[ \xymatrix { \mathscr {F}(x) \ar [r] \ar [d]^{ \gamma _{x} } & \mathscr {F}'(x) \ar [r]^{ \mathscr {F}'(e)} \ar [d]^{ \gamma '_{x} } & \mathscr {F}'(y) \ar [d]^{ \gamma '_{y} } \\ \mathscr {G}(x) \ar [r] & \mathscr {G}'(x) \ar [r]^{ \mathscr {G}'(e) } & \mathscr {G}'(y) } \]

where our hypothesis on $\sigma $ guarantees that the left side is a pullback diagram. Applying Proposition 7.6.2.28, we are reduced to showing that the right side is also a pullback diagram, which follows from our assumption that $\gamma '$ is cartesian.