Kerodon

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

Construction 9.3.4.32 (Inverse Images). Let $\operatorname{\mathcal{C}}$ be an $\infty $-category which admits fiber products. Then every morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$ determines a pullback functor

\[ f^{\ast }: \operatorname{\mathcal{C}}_{/Y} \rightarrow \operatorname{\mathcal{C}}_{/X} \quad \quad Y' \mapsto X \times _{Y} Y' \]

(see Proposition 7.6.2.24). The functor $f^{\ast }$ has a left adjoint, and therefore carries subterminal objects of $\operatorname{\mathcal{C}}_{/X}$ to subterminal objects of $\operatorname{\mathcal{C}}_{/Y}$. Passing to isomorphism classes, we obtain a map of partially ordered sets $f^{-1}: \operatorname{Sub}(Y) \rightarrow \operatorname{Sub}(X)$, given concretely by the formula $f^{-1} [Y_0] = [ Y_0 \times _{Y} X ]$. Since the functor $f^{\ast }$ preserves products, $f^{-1}$ is a homomorphism of lower semilattices: that is, it satisfies the identities

\[ f^{-1}( [Y_0] \cap [Y_1] ) = f^{-1}([Y_0]) \cap f^{-1}( [Y_1] ) \quad \quad f^{-1}([Y]) = [X]. \]