Descent identities for the atomic finite-surjection site (source code)

= Descent identities for the atomic finite-surjection site

For any sheaf $F$ and surjection $q:n\to k$, $F(k)\to F(n)\rightrightarrows F(n\times_kn)$ is an equalizer. In particular every $F(q)$ is injective. These follow from the sheaf condition on the sieve generated by the covering arrow $q$ and control primitive elements.