mathlib3 documentation


Constructing colimits from finite colimits and filtered colimits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.