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 constructed 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.
Instances For
If 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
type.