# Monomorphism into separated presheaf

Let $$X, Y : \mathbb{C}^\text{op} \to \mathbf{Set}$$, where $$\mathbb{C}$$ is a small category, and assume the natural transformation $$\alpha : X \to Y$$ is a monomorphism. If $$Y$$ is separated with respect to a coverage on $$\mathbb{C}$$, then is $$X$$ necessarily separated (w.r.t. the same coverage)?

The natural transformation $$\alpha$$ is a monomorphism precisely when all of its components are injections. That way we may see $$X$$ as just a subpresheaf of $$Y$$. That is, for each object $$C$$ in $$\mathbb{C}$$ we have $$X(C) \subseteq Y(C)$$ and $$\alpha_C$$ is just this inclusion.
A presheaf $$X$$ is separated (with respect to a fixed Grothendieck topology) if the following holds: for every object $$C$$ in $$\mathbb{C}$$ and all $$x, y \in X(C)$$, if the sieve $$\{f: C' \to C \mid X(f)(x) = X(f)(y)\}$$ is covering, then $$x = y$$.
Now assume $$Y$$ is separated. Let $$x, y \in X(C)$$ such that $$S = \{f: C' \to C \mid X(f)(x) = X(f)(y)\}$$ is covering. Then because $$X(C) \subseteq Y(C)$$ we have that $$x,y \in Y(C)$$. Since $$S$$ is covering for $$C$$ and $$Y$$ is separated we conclude that $$x = y$$, and so we see that indeed $$X$$ is separated.
Another way of defining sheaves that I find elegant is the following: $$Y$$ is a sheaf (with respect to a given covering) if and only if for every covering sieve $$S$$ on $$U$$ represented as a subfunctor of $$\mathsf{Hom}(-,U)$$ we have $$y\mapsto(f\mapsto Y(f)(y)):Y(U)\to\mathsf{Nat}(S,Y)$$ is an isomorphism. Here, $$\mathsf{Nat}(S,Y)$$ is the set of natural transformations from $$S$$ to $$Y$$. $$Y$$ is a separated presheaf if this is only a monomorphism.
Given that $$Y$$ is separated and $$\alpha$$ is a mono, then so is $$x\mapsto(f\mapsto Y(f)(\alpha_U(x))):X(U)\to\mathsf{Nat}(S,Y)$$ for every $$U$$ and $$S$$ covering $$U$$ because it's a composition of monomorphisms. Naturality of $$\alpha$$ states that $$Y(f)\circ\alpha_U=\alpha_V\circ X(f)$$, in other words $$x\mapsto(f\mapsto Y(f)(\alpha_U(x))) = x\mapsto(f\mapsto \alpha(X(f)(x)))$$ This means $$x\mapsto(f\mapsto X(f)(x))$$ is a mono since it factors through a mono via post-composition by a mono.