Kerodon

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

Remark 8.6.1.4 (Base Change). Let $F: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets. Suppose we are given pullback squares

\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}'^{\dagger } \ar [r]^-{ U'^{\dagger } } \ar [d] & \operatorname{\mathcal{C}}'^{\operatorname{op}} \ar [d]^{F^{\operatorname{op}}} & \operatorname{\mathcal{E}}' \ar [r]^-{ U' } \ar [d] & \operatorname{\mathcal{C}}' \ar [d]^{F} \\ \operatorname{\mathcal{E}}^{\dagger } \ar [r]^-{U^{\dagger }} & \operatorname{\mathcal{C}}^{\operatorname{op}} & \operatorname{\mathcal{E}}\ar [r]^-{ U} & \operatorname{\mathcal{C}}, } \]

where $U^{\dagger }$ is a cartesian fibration and $U$ is a cocartesian fibration. If $T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ is a morphism which exhibits $U^{\dagger }$ as a cartesian conjugate of $U$, then the induced map $T': \operatorname{\mathcal{E}}'^{\dagger } \times _{ \operatorname{\mathcal{C}}'^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}') \rightarrow \operatorname{\mathcal{E}}'$ exhibits $U'^{\dagger }$ as a cartesian conjugate of $U'$.