I'm reading Chapter 2 of Mac Lane and Moerdijk's Sheaves in Geometry and Logic.
At some point our guys claim that given a topological space $ X $ and a sheaf $ F $ on $ X $, a subsheaf $ S $ of $ F $ is itself a sheaf if and only if for every open set $ U\subset X $ and every open cover $ U = \bigcup_{i\in I}U_i $ of $ U $, chosen a $ s\in FU $ we have $ s\in SU $ if and only if $ s{\restriction_{U_i}}\in S(U_i) $ for every $ i\in I $.
In the proof it is light-heartedly claimed that the condition $ s\in S(U) $ if and only if $ s{\restriction_{U_i}}\in S(U_i) $ for every $ i\in I $ is equivalent to the diagram $$ \require{AMScd} \begin{CD} SU @>>> \prod_\nolimits{i\in I}S(U_i)\\ @VVV @VVV\\ FU @>>> \prod_\nolimits{i\in I}F(U_i) \end{CD} $$ being a pullback square, where the horizontal arrows maps $ s\mapsto (s{\restriction}_{U_i})_{i\in I} $ and the vertical arrows are the inclusions.
Is there a "slick" way to prove this fact?
I can show that the condition mentioned above is equivalent to the obvious map $$ SU\to FU\times_{\prod_{i\in I}F(U_i)}\prod_{i\in I}S(U_i) = \left\{(s,(s_i)_{i\in I})\in FU\times \prod_{i\in I}S(U_i) : \text{$ s{\restriction_{U_i}} = s_i $ for every $ i\in I $}\right\},\quad s\mapsto (s,(s{\restriction_{U_i}})_{i\in I}) $$ being a bijection, and that this fact is equivalent to the diagram above being a pullback. But I was wondering if there was a smarter way to prove this fact than exhibiting the bijection above (maybe a trick usign generalized elements, or some other categorical wizardry).
Indeed I'm always at unease when someone asks me to show that a diagram [of sets] is a pullback, and I usually resort to the bijection trick described above, but I find it a little clumsy.
I mean there is nothing wrong or clumsy about using the explicit formula of pullbacks of sets, but if you insist on having a more abstract proof, the following might work.
Recall that $F$ respectively $S$ is a sheaf iff the diagram $$S(U) \rightarrow \prod_i S(U_i) \overset{\rightarrow}{\underset{\rightarrow}{}} \prod_{i,j} S(U_i \cap U_j)$$ is an equalizer diagram. A monomorphism of functors $S \rightarrow F$ gives rise to a diagram of (wannabe) equalizers $$\begin{array}{ccccc} S(U) & \rightarrow & \prod_i S(U_i) & \overset{\rightarrow}{\underset{\rightarrow}{}} & \prod_{i,j} S(U_i\cap U_j)\\ \downarrow &&\downarrow&&\downarrow\\ F(U) & \rightarrow & \prod_i F(U_i) & \overset{\rightarrow}{\underset{\rightarrow}{}} & \prod_{i,j} F(U_i\cap U_j) \end{array}$$ with all vertical morphisms being monic. You can now show explicitly that giving a cone over the left square is the same as giving a cone over the upper equalizer diagram. Thus being universal for one type of these amounts to being universal for the other.