Constructing colimits from finite colimits and filtered colimits #
We construct colimits of size
w from finite colimits and filtered colimits of size
w-sized colimits are constructed from coequalizers and
w-sized coproducts, it suffices to
w-sized coproducts from finite coproducts and
w-sized filtered colimits.
The idea is simple: to construct coproducts of shape
α, we take the colimit of the filtered
diagram of all coproducts of finite subsets of
We also deduce the dual statement by invoking the original statement in
C has finite coproducts, a functor
Discrete α ⥤ C lifts to a functor
Finset (Discrete α) ⥤ C by taking coproducts.
C has finite coproducts and filtered colimits, we can construct arbitrary coproducts by
taking the colimit of the diagram formed by the coproducts of finite sets over the indexing