Where can I find a reference for the following fact:


If $C$ is a small category with finite colimits, then $\text{Ind}(C)$ is a category with all colimits, and it is the universal one in the following sense: If $D$ is a category with all colimits, then there is an equivalence of categories between finitely cocontinuous functors $C \to D$ and cocontinuous functors $\text{Ind}(C) \to D$.


This is a consequence of a combination of facts which can be found in SGA 4 I.8 and Section 6 in "Category of Sheaves" by Kashiwara, Shapira. I wonder if this is written down somewhere so that I can reference it in my work without spelling out the proof.


EDIT: Actually I don't know exactly how to prove it. Take a finitely cocont. functor $C \to D$. This extends to a cocont. functor $\widehat{C} \to D$ and may be restricted to $\text{Ind}(C)$. The resulting functor $\text{Ind}(C) \to D$ commutes with coproducts and with filtered colimits. The problem are the cokernels (or rather coequalizer, if we do not deal with linear categories). Namely, we should prove that every cokernel diagram in $\text{Ind}(C)$ is a filtered colimit of cokernel diagrams in $C$. Now in the book by Kashiwara, Schapira it is shown that (almost) every finite diagram in $\text{Ind}(C)$ is a filtered colimit of diagrams of the same shape in $C$. But we need a refinement of this!



Indization as adjoint from finite colimits to all colimits
Every finite loopless diagram in Ind-$C$ can be represented as a levelwise diagram, i.e. as a diagram of functors $I \to C$ for some filtered $I$. (Artin-Mazur, App. of Etale Homotopy Theory, Prop. 3.3 for example.) In particular, this holds for coequalizer diagrams. Then the colimit can be computed levelwise (Prop. 4.1 in Artin-Mazur). See also D. Isaksen, "Calculating limits and colimits in pro-categorie", Fund. Math. 175 (2002).


