Surjectivity detected by the subobject classifier (source code)

= Surjectivity detected by the subobject classifier
{title2=$\lambda:\Omega_{\mathcal E}\hookrightarrow f_*\Omega_{\mathcal F}$}

For a <geometric morphism>, the characteristic map of $f^*\top$ induces a comparison $f^*\Omega_{\mathcal E}\to\Omega_{\mathcal F}$ whose adjoint transpose is $\lambda$. Composing with a characteristic map classifies the inverse-image subobject. Thus monicity of $\lambda$ is equivalent to reflection of equality of subobjects under $f^*$, and hence to faithfulness of the inverse image: apply reflection to equalizers of parallel arrows. Conversely faithfulness reflects when a pulled-back monomorphism is an isomorphism, by comparing its characteristic map with truth; intersections then reflect equality of arbitrary subobjects.