10 ANDREJ gfiEDROV
the category Mod(F,S ) and the category of F-internal flat functors on
C (as a constant object in F) and F-internal natural transformations.
Moreover, this equivalence is natural in F •
Remark. A few comments on the statement of the theorem are in order.
If F is the category of S , it just says that "the category
is equivalent to the full subcategory of S whose objects are flat
functors on CC" . The statement of the theorem means that the above
sentence in quotation marks is true when interpreted in F . In practice,
it often suffices to look at the case f - S , and check that the
facts about the situation are proved intuitionistically.
Corollary (Diaconescu). Under the hypotheses of the theorem, let J be
a Grothendieck topology on C C . Then there is an equivalence between the
category Mod(F,Shj (CC ) ) and the category of F-internal flat continuous
functors on C C (i.e. F-internal flat functors on ( C taking J-covers to
epimorphic families in F).
In practice, J is the Grothendieck topology generated by a family
of sieves on C C closed w.r.t. pullbacks:
Lemma (folklore) . Let K be a family of sieves in a category C C , and
assume that K is closed w.r.t. pullbacks. Then for the Grothendieck
topology J generated by K , a flat functor from C C to a Grothendieck
topos F is continuous for J iff it sends every sieve in K to an
epimorphic family in F .