mathlib documentation


Constructing colimits from finite colimits and filtered colimits #

We construct colimits of size w from finite colimits and filtered colimits of size w. Since w-sized colimits are constructured from coequalizers and w-sized coproducts, it suffices to construct 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ᵒᵖ.

If C has finite coproducts, a functor discrete α ⥤ C lifts to a functor finset (discrete α) ⥤ C by taking coproducts.