Could not include topos theory - contents
The condition that a presheaf be a sheaf may be seen as a condition of unique existence. A presheaf is separated if it satisfies the uniqueness part.
Let $S$ be a site.
Recall that a sheaf on $S$ is a presheaf $A \in PSh_S$ such that for all local isomorphisms $Y \to X$ the induced morphism $PSh_S(X,A) \to PSh_S(Y,A)$ (under the hom-functor $PSh_S(-,A)$) is an isomorphism. (For an arbitrary class of morphisms $V$, the corresponding condition is called being a local object.)
It is sufficient to check this on the dense monomorphisms instead of all local isomorphisms. This is equivalent to checking covering sieves.
A presheaf $A \in PSh(S)$ is called separated (or a monopresheaf) if for all local isomorphisms $Y \to X$ the induced morphism $Hom(X,A) \to Hom(Y,A)$ is a monomorphism.
More generally, for a class $V$ of arrows in a category $C$, an object $A\in C$ is $V$-separated if for all morphisms $Y\to X$ in $V$, the induced morphism $Hom(X,A)\to Hom(Y,A)$ is a monomorphism.
As for sheaves, it is sufficient to check the separation condition on the dense monomorphisms, hence on the sieves.
For $\{p_i : U_i \to U\}$ a covering family of an object $U \in S$, the condition is that if $a,b \in A(U)$ are such that for all $i$ we have $A(p_i)(a) = A(p_i)(b)$ then already $a = b$.
The definition generalizes to any system of local isomorphisms on any topos, such as that obtained from any Lawvere-Tierney topology, or equivalently any subtopos.
Let $(S,J)$ be a site for which every $J$-covering family is inhabited. Then for any set $X$, the constant presheaf $S\ni a \mapsto X$ is separated.
See also at locally connected site.
The full subcategory
of separated presheaves in a presheaf category is
Being a reflective subcategory means that there is a left adjoint functor to the inclusion
For $A \in PSh_S$ the separafication $L_{sep}A$ of $A$ is the presheaf that assigns equivalence classes
where $\sim_U$ is the equivalence relation that relates two elements $a \sim b$ iff there exists a covering $\{p_i : U_i \to U\}$ such that $A(p_i)(a) = A(p_i)(b)$ for all $i$.
This construction extends in the evident way to a functor
This functor $L_{sep}$ is indeed a left adjoint to the inclusion $i : Sep(S) \hookrightarrow PSh(S)$.
Let $A \in PSh(S)$ and $B \in Sep(S) \hookrightarrow PSh(S)$. We need to show that morphisms $f : A \to B$ in $PSh_C$ are in natural bijection with morphisms $L_{sep} A \to B$ in $Sep(S)$.
For $f$ such a morphism and $f_U : A(U) \to B(U)$ its component over any object $U \in S$, consider any covering $\{U_i \to U\}$, let $S(U_i) \to U$ be the corresponding sieve and consider the commuting diagram
obtained from the naturality of $PSh_S(S(U_i) \to U, A \stackrel{f}{\to} B)$.
If for $a,a' \in A(U)$ two elements that are not equal their restrictions to the cover become equal in that $\forall i : a|_{U_i} = a'|_{U_i}$, then also $f(a|_{U_i}) = f(a'|_{U_i})$ and since the right vertical morphism is monic there is a unique $b \in B(U)$ mapping to the latter. The commutativity of the diagram then demands that $f(a) = f(a') = b$.
Since this argument applies to all covers of $U$, we have that $f_U$ factors uniquely through the projection map $A(U) \to A(U)/\sim_U =: L_{sep}(U)$ onto the quotient. Since this is true for every object $U$ we have that $f$ factors uniquely through $A \to L_{sep}A$.
Often one is interested in separated presheaves with respect to one coverage that are sheaves with respect to another coverage. These are called biseparated presheaves .
This typically arises if a reflective subcategory
of a sheaf topos is given. This is the localization at a set $W$ of morphisms in $Sh(S)$, with $C$ the full subcategory of all local objects $c$: objects such that $Sh_(S)(w,c)$ is an isomorphism for all $w \in W$. A $W$-separated object is then called a biseparated presheaf on $S$ and their collection $BiSep(S)$ factors the reflective inclusion as
A bisite is a small category $S$ equipped with two coverages: $J$ and $K$ such that $J \subset K$.
A presheaf $A \in PSh_S$ is called $(J,K)$-biseparated if it is
a sheaf with respect to $J$;
a separated presheaf with respect to $K$.
Write
for the full subcategory on biseparated presheaves.
Biseparated presheaves form a reflective subcategory of all sheaves
See quasitopos for the proof.
separated presheaf
The general theory of biseparated presheaves and Grothendieck quasitoposes is in section C.2.2 of
A concrete description of separafication appears on page 43 of