Any map of sets $A \xrightarrow{f} B$ induces a functor of posets $Sub(B) \xrightarrow{f^{-1}} Sub(A)$. It is known to have left and right adjoints $\exists_f$ and $\forall_f$ (defined as $\exists_f: X \mapsto f(X)$ and $\forall_f: X \mapsto \{y: f(x) = y \implies x \in X\}).$ I've noticed that for the first adjunction,
- $f$ is injective iff the unit is an isomorphism (i.e. $f^{-1}f(X)=X)$,
- $f$ is surjective iff the counit is an isomorphism.
Similar two statements hold for the second adjunction. It's easily seen from the definitions or from the well-known connection between (co)unit and (faith)fulness of adjunct functors.
I feel that this has to be more than a random observation, but it does not find a place in my head. So I may try to ask this way: is there some generalization of those facts? For example, $\exists_f$ and $\forall_f$ exist in any locally cartesian closed category with pullbacks, in particular all topoi have such adjunctions. What if we try to define injections/surjections this way?
Or is this just a simple manifestation of some well-known general fact I somehow fail to see?
The generalisation is as follows:
Consider a regular category $C$(a category with finite limits which has regular-epi mono image factorizations stable under pullback, allowing one to define $\exists_f m$ as the image of $f \circ m$). Note that the slice of any regular category is regular. Suppose $f : X \to Y$. Then
Proof: if $f$ is regular epic, then consider some monic $m : M \to Y$. Then the pullback of $m$ gives us an object $f^{-1}M$ and two arrows $h : f^{-1}M \to M$, $f^{-1}m : f^{-1}M \to X$. Now since $h$ is the pullback of a regular epi $f$, $h$ must be a regular epi. So $m \circ h$ is the image factorization of $f \circ f^{-1}m$. Therefore, $m$ is the image of $f^{-1}m$.
Conversely, suppose that $\exists_f \circ f^{-1} = 1$. Then the pullback of $1_Y : Y \to Y$ is $1_X : X \to X$. So $\exists_f 1_X = 1_Y$. But this means that the image of $f \circ 1_X = f$ is $1_Y$. Since the image of $f$ is the whole of $Y$, $f$ must be regular epi.
Forward proof: If $f$ is mono, then any pullback of $f$ is mono. So in particular, $A \times f$ is mono, as it is the pullback of $f$ along $A \to 1$. So it suffices to show for one direction that if $f$ is mono, $f^{-1} \circ \exists_f = 1$.
To show this, we note that $\exists_f m = f \circ m$, since $f$ is mono. Note that $f^{-1}(f) = 1$, so $f^{-1}(f \circ m) = 1^{-1}(m) = m$. So $f^{-1} \circ \exists_f = 1$.
To show the converse, consider two maps $g, h : K \to X$. Then the maps $(1_K, g) : K \to K \times X$ and $(1_K, h) : K \to K \times X$ are both mono. Suppose that $f \circ g = f \circ h$. Then $(K \times f) \circ (1_K, g) = (K \times f) \circ (1_K, h)$. Therefore, $\exists_{K \times f}(1_K, g) = \exists_{K \times f}(1_K, h)$. Then $(1_K, g) = (1_K, h)$. Then $g = h$. Thus, $f$ is mono.
I am not sure whether we can strengthen 3 to only have the requirement $f^{-1} \circ \exists_f = 1$. I have played around a bit to try to find a counterexample or a proof that we can do this, and haven't had any luck so far.