Locality and descent
A matching family of elements is an explicit component-wise characterizaton of a morphism from a sieve into a general presheaf.
Since such morphisms govern the sheaf property and the operation of sheafification, these can be discussed in terms of matching families.
Let be a site and a presheaf on . Let be a covering sieve on object (in particular a subobject of the representable presheaf ).
A matching family for of elements in is a rule assigning to each in an element such that for all
Notice that because is a sieve, so that the condition makes sense; furthermore the order of composition and the contravariant nature of agree. If we view the sieve as a subobject of the representable , then a matching family is precisely a natural transformation , .
An amalgamation of the matching family for is an element such that for all .
Characterization of sheaves
is a sheaf for the Grothendieck topology iff for all , for all and every matching family for , there is a unique amalgamation. Equivalently is a sheaf if any natural transformation has a unique extension to (along inclusion ); or to phrase it differently, is a sheaf (resp. separated presheaf) iff the precomposition with the inclusion is an isomorphism (resp. monomorphism) .
Suppose now that has all pullbacks. Let be any cover of (i.e., the smallest sieve containing is a covering sieve in ) and let , be the two projections of the pullback of along . A matching family for of elements in a presheaf is by definition a family of elements , such that for all , .
Let be the set of matching families for of elements in . Sieves over form a filtered category, where partial ordering is by reverse inclusion (refinement of sieves). There is an endofunctor given by
In other words, elements in are matching families for all covering sieves modulo the equivalence given by agreement , for all , where is a common refinement of and . This is called the plus construction.
Endofunctor extends to a presheaf on by where (recall that by the stability axiom of Grothendieck topologies, is a covering sieve over ).
The presheaf comes equipped with a canonical natural transformation which to an element assigns the equivalence class of the matching family where the maximal sieve is the class of objects of the slice category .
is a monomorphism (resp. isomorphism) of presheaves iff the presheaf is a separated presheaf (resp. sheaf); moreover any morphism of presheaves, where is a sheaf, factors uniquely through . For any presheaf , is separated presheaf and if is already separated then is a sheaf. In particular, for any presheaf is a sheaf. A fortiori, realizes sheafification.
A standard reference is