Plus construction on presheaf iff isomorphism

54 Views Asked by At

This is from Sheaves in Geometry and Logic, III5. Lemma 2, Moerdijk and Mac Lane.

On a site $(\mathcal C, J)$, and given a prehseaf $P$

Define the plus construction by$$P^+(U) = \underrightarrow{\mathrm{lim}}_{R \in J(U)} Match(R, P)$$

The claim is

If $\eta: P \rightarrow P^+$ is an isomoprhism then $P$ is a sheaf.

$\eta$ sends $x \in P(C)$ to the matching fmaily $\{x \cdot f \, : \, f \in t_C \}$ where $t_C$ is maximal sieve.

I see how being mono shows $P$ is separated.

But how does surjectivity imply the existence ?

Concern: given a matching family for a sieve $S$, $$\{x_f \, : \, f \in S \} $$ to say that $\eta$ is surjective, implies there exists a refinement $T \subseteq S$ $$ \{x_f \,:\, f \in T \} $$ is restriction fo $x \in P(C)$. This is weaker than what we need.