Notice that in terms of n-truncated morphisms, a presheaf is
In the context of (n,1)-topos theory, therefore, the plus-construction is applied -times in a row. The second but last step makes an (n,1)-presheaf into a separated infinity-stack and then the last step into an actual (n,1)-sheaf. (See Lurie, section 6.5.3.)
Let be a small site equipped with a Grothendieck topology , let be a functor. Then the plus construction (functor) , resp. the plus construction of is defined by one of following equivalent descriptions:
where denotes the poset of -covering sieves on .
Let be a functor. Then for we define to be an equivalence class of pairs where and is a compatible family of elements of relative to , and iff there is a -covering sieve on which the restrictions of and agree.
where denotes the class of those morphisms in which are sent to isomorphisms by the sheafification functor and the colimit is taken over all dense monomorphisms only.
is a functor.
is a functor.
is a separated presheaf.
If is separated then is a sheaf.
Note that is not left adjoint to the inclusion of the full subcategory of separated presheaves. If it were, it would be a reflector and therefore satisfy . But this is false, since the plus construction applied to separated presheaves yields their sheafification. See this MathOverflow question for details.
The plus construction can be described in the internal language of the presheaf topos . For a presheaf , seen as a set from the internal point of view, the separated presheaf is given by the internal expression
where is the equivalence relation given by if and only if and is the Lawvere–Tierney topology describing the subtopos .
With this internal description, the verification of the properties of the plus construction becomes an exercise with sets and subsets (instead of colimits).
Related entries: sheafification
A standard textbook reference in the context of 1-topos theory is:
Remarks on the plus-construction in (infinity,1)-topos theory is in section 6.5.3 of
Plus construction for presheaves in values in abelian categories is also called Heller-Rowe construction: