Kerodon

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

Proposition 10.3.1.34 (Transitivity). Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $Y$ be an object of $\operatorname{\mathcal{C}}$, and let $\operatorname{\mathcal{C}}^{0}_{/Y}, \operatorname{\mathcal{C}}^{1}_{/Y} \subseteq \operatorname{\mathcal{C}}_{/Y}$ be sieves on $Y$. Assume that:

$(1)$

The sieve $\operatorname{\mathcal{C}}^{0}_{/Y}$ is dense.

$(2)$

For each morphism $f: X \rightarrow Y$ which belongs to $\operatorname{\mathcal{C}}^{0}_{/Y}$, the pullback sieve $f^{\ast }( \operatorname{\mathcal{C}}^{1}_{/Y} ) \subseteq \operatorname{\mathcal{C}}_{/X}$ is dense.

Then $\operatorname{\mathcal{C}}^{1}_{/Y}$ is also a dense sieve.

Proof. Let $U: \operatorname{\mathcal{C}}_{/Y} \rightarrow \operatorname{\mathcal{C}}$ denote the projection map; we wish to show that $U$ is left Kan extended from $\operatorname{\mathcal{C}}^{1}_{/Y}$. Assumption $(1)$ guarantees that $U$ is left Kan extended from $\operatorname{\mathcal{C}}^{0}_{/Y}$. By virtue of Corollary 7.3.8.8, it will suffice to show that $U|_{ \operatorname{\mathcal{C}}^{0}_{/Y} }$ is left Kan extended from the intersection $\operatorname{\mathcal{C}}^{01}_{/Y} = \operatorname{\mathcal{C}}^{0}_{/Y} \cap \operatorname{\mathcal{C}}^{1}_{/Y}$. Fix a morphism $f: X \rightarrow Y$ which belongs to the sieve $\operatorname{\mathcal{C}}^{0}_{/Y}$; we wish to show that $U$ is left Kan extended from $\operatorname{\mathcal{C}}^{01}_{/Y}$ at $f$. This follows from our assumption that $f^{\ast } \operatorname{\mathcal{C}}^{01}_{/Y} = f^{\ast } \operatorname{\mathcal{C}}^{1}_{/Y}$ is a dense sieve on $X$. $\square$