Fppf sheaves of sets and sheafification

Throughout, $S$ is a fixed base scheme and $(Sch\mathrm{/}S{)}_{fppf}$ is the fppf site of Fppf coverings and the fppf site.

A presheaf of sets on $(Sch\mathrm{/}S{)}_{fppf}$ is a contravariant functor from the category of $S$-schemes to the category of sets (Presheaves, covariantly and contravariantly representable functors, and representations, Covariant functor, identity functor, composite functor, and contravariant functor); the associated representable presheaf of a scheme is the contravariant functor it represents. It is an fppf sheaf when for every fppf covering $\{T_i\to T{\}}_{i\in I}$ the diagram $F(T)⟶{\prod }_{i}F(T_i)\rightrightarrows {\prod }_{i,j}F(T_i{\times }_T{T}_j)$ is an equalizer of sets (Fibre product of schemes), the two maps being the pullbacks along the two projections $T_i{\times }_T{T}_j\to T_i,T_j$. Equivalently, restriction identifies $F(T)$ with the set of families $(s_i{)}_{i\in I}$, $s_i\in F(T_i)$, whose two pullbacks to every $T_i{\times }_T{T}_j$ agree (Equivalence relation, equivalence class, and the quotient set $A\mathrm{/}\sim$ for the underlying set-theoretic relation); the two descriptions agree because an equalizer in sets consists of the elements on which the two maps coincide.

A morphism of presheaves is a natural transformation (Natural transformation and its components); the presheaves on $(Sch\mathrm{/}S{)}_{fppf}$ thus form a category. The sheafification of a presheaf $F$ is an fppf sheaf $F^{\mathrm{a}}$ together with a morphism $F\to F^{\mathrm{a}}$ such that every morphism $F\to G$ with $G$ an fppf sheaf factors uniquely through $F\to F^{\mathrm{a}}$. When it exists it is unique up to unique isomorphism, by the usual universal property; in this library its existence is established separately for the presheaves used below. A representable presheaf is an fppf sheaf (Scheme morphisms satisfy fppf descent), under the Axiom of Choice recorded there, since fppf descent for morphisms of schemes is effective.

All sheaves below are set-valued unless stated otherwise. The empty family is an fppf covering of the empty scheme, so for a sheaf the sheaf condition on that covering forces $F(\mathrm{\varnothing })$ to be a one-point set; this holds in particular for every representable presheaf, since ${\mathrm{Hom}}_S(\mathrm{\varnothing },X)$ is a one-point set for every $S$-scheme $X$, because the empty scheme is initial in the category of $S$-schemes.