# Equivalence of two definitions of sheaves on a site

I'd like to prove that two definitions of sheaves on a site are equivalent, but I'm having trouble proving one direction.

Let $C$ be a category with pullbacks. Let $(C,T)$ be a site defined through a collection $\Phi$ of covering families. (So that a subfunctor of $Hom(-,U)$ is a covering sieve in $T$ if and only if it contains a covering family in $\Phi$).

Let $F$ be a presheaf on $C$, taking values in some complete category.

Then it should be the case that the following are equivalent characterisations of $F$ being a sheaf.

1) For each $U\in C$, and each covering sieve $R \subset Hom(-,U)$, the map $F(U) \to {{\lim \atop \leftarrow} \atop {V\to U \in R}} F(V)$ is an isomorphism.

2) The following diagram is an equalizer for each $U$ in $C$, and covering family {$U_\alpha \to U$} in $\Phi$: $$F(U) \to \prod_\gamma F(U_\gamma) {\rightarrow \atop \rightarrow} \prod_{(\alpha,\beta)} F(U_\alpha \times_U U_\beta)$$

Question: How do you prove $2) \implies 1)$?. (I've proved $1) \implies 2)$)

Here's my proof attempt of $2) \implies 1)$ so far:

$\bullet$ Suppose we have a covering family {$U_\alpha \to U$} in $\Phi$,and that it generates a sieve $S$. I proved that the following is an equalizer:

$${{\lim \atop \leftarrow} \atop {V\to U \in S}} F(V) \to \prod_\gamma F(U_\gamma) {\rightarrow \atop \rightarrow} \prod_{(\alpha,\beta)} F(U_\alpha \times_U U_\beta)$$

(This is also what I used to prove $1) \implies 2)$).

$\bullet$ Let $R$ be an arbitrary covering sieve, which is a subfunctor of $Hom(-,U)$. Then it contains a covering family {$U_\alpha \to U$}, and the diagram of $2)$ is an equalizer by assumption. If $S$ is the covering sieve generated by the covering family (so $S \subset R$), the diagram above is also an equalizer. By an isomorphism of equalizers, the map $F(U) \to {{\lim \atop \leftarrow} \atop {V\to U \in S}} F(V)$ is an isomorphism.

Because of the commutative diagram

$F(U) \to {{\lim \atop \leftarrow} \atop {V\to U \in R}} F(V)$

$\ \ \ \ \ \ \cong \searrow \ \ \ \ \ \downarrow$

$\ \ \ \ \ \ \ \ \ \ \ \ \ \ {{\lim \atop \leftarrow} \atop {V\to U \in S}} F(V)$

we get that the map $F(U) \to {{\lim \atop \leftarrow} \atop {V\to U \in R}} F(V)$ is a split monic. From here, I'm not sure how to show that it's also epi.

So the crux of my issue is that I can prove the isomorphism in $1)$ only for covering sieves generated by covering families, but not for arbitrary covering sieves.

-
And you have looked in the Elephant and/or MacLane & Moerdijk? –  Andrej Bauer Oct 28 '10 at 6:03
Thanks, it was in MacLane (p.124). For some reason, I missed it before. –  user9109 Oct 29 '10 at 5:46

In (1) we have the limit ${\underleftarrow{lim}}(R^{ op } \subset (\mathscr{C} \downarrow X) ^{ op } \xrightarrow{\pi^{op} } \mathscr{C} ^{ op }\xrightarrow{F} Set )$.
Any covering sieve $R$ is genated by the covering familes $\Phi$: $R=${$f\circ r | f\in \Phi,\ r\in |\mathscr{C}\downarrow d_0(f)|_0)$} (sorry for the brace brackets) . Then considering $\Phi$ and all pullback’s of its element’s we get final diagram $\Phi^\star \subset R$ (this means that the comma category $r \downarrow \Phi^\star$ is connected for any $r\in \Phi$). Then $(\Phi^\star)^{ op } \subset R^{ op }$ is initial, and any limits on $R^{ op }$ is isomorphic (is the some) to its restriction to $(\Phi^*)^{ op }$ and latter limit is the Ker diagram in $(2)$ (canonical form of limits in terms of Ker and products).