Let $J$ be a Grothendieck topology on a category $\mathcal{C}$ . If $R \mathbin{⪧}_J U$ and $S \mathbin{⪧} U$ is a sieve on $U$ containing $R$ , then $S \mathbin{⪧}_J U$ .

Proof [local-0]

The key is this: By definition of sieve, for any element $f \in R$ , the set $f^*(R)$ is a maximal sieve of $\text{dom}(f)$ ! Because let's see

f^*(R) = \{ g \mid f \circ g \in R \}

because elements of $R$ are closed under composition, $f^*(R)$ is the maximal sieve of $\text{dom}(f)$ :

f^*(R) = \{g \mid \text{cod}(g) = \text{dom}(f) \} = M_{\text{dom}(f)}

Because all elements of $R$ also belongs to $S$ , we have $f^*(R) \subseteq f^*(S)$ ; but $f^*(R)$ is the maximal sieve of $\text{dom}(f)$ , hence $f^*(R) = f^*(S)$ .

Recall that maximal sieve of $U$ belongs to $J(U)$ , implies that for any $f \in R$ , we have $f^*(S) \mathbin{⪧}_J \text{dom}(f)$ . We apply property (iii), conclude that $S \mathbin{⪧}_J U$ .

Proposition. For any sieve RRR in JJJ, bigger sieve S⊇RS \supseteq RS⊇R also in JJJ [7R33]

Proof [local-0]

Proposition. For any sieve $R$ in $J$ , bigger sieve $S \supseteq R$ also in $J$ [7R33]