Gluing Axiom - Sheafification

To turn a given presheaf P into a sheaf F, there is a standard device called sheafification or sheaving. The rough intuition of what one should do, at least for a presheaf of sets, is to introduce an equivalence relation, which makes equivalent data given by different covers on the overlaps by refining the covers. One approach is therefore to go to the stalks and recover the sheaf space of the best possible sheaf F produced from P.

This use of language strongly suggests that we are dealing here with adjoint functors. Therefore it makes sense to observe that the sheaves on X form a full subcategory of the presheaves on X. Implicit in that is the statement that a morphism of sheaves is nothing more than a natural transformation of the sheaves, considered as functors. Therefore we get an abstract characterisation of sheafification as left adjoint to the inclusion. In some applications, naturally, one does need a description.

In more abstract language, the sheaves on X form a reflective subcategory of the presheaves (Mac Lane-Moerdijk Sheaves in Geometry and Logic p. 86). In topos theory, for a Lawvere-Tierney topology and its sheaves, there is an analogous result (ibid. p. 227).