Description: A co-cone (or cocone) to a diagram (see df-lmd for definition), or a natural sink for a diagram in a category C is a pair of an object X in C and a natural transformation from the diagram to the constant functor (or constant diagram) of the object X . The second component associates each object in the index category with a morphism in C whose codomain is X ( coccl ). The naturality guarantees that the combination of the diagram with the co-cone must commute ( coccom ). Definition 11.27(1) of Adamek p. 202.
A colimit of a diagram F : D --> C of type D in category C is a universal pair from the diagram to the diagonal functor ( C DiagFunc D ) . The universal pair is a co-cone to the diagram satisfying the universal property, that each co-cone to the diagram uniquely factors through the colimit. ( iscmd ). Definition 11.27(2) of Adamek p. 202.
Initial objects, coproducts, coequalizers, pushouts, and direct limits can be considered as colimits of some diagram; colimits can be further generalized as left Kan extensions ( df-lan ).
"cmd" is short for "colimit of a diagram". See df-lmd for the dual concept. (Contributed by Zhi Wang, 12-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-cmd | |- Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccmd | |- Colimit |
|
| 1 | vc | |- c |
|
| 2 | cvv | |- _V |
|
| 3 | vd | |- d |
|
| 4 | vf | |- f |
|
| 5 | 3 | cv | |- d |
| 6 | cfunc | |- Func |
|
| 7 | 1 | cv | |- c |
| 8 | 5 7 6 | co | |- ( d Func c ) |
| 9 | cdiag | |- DiagFunc |
|
| 10 | 7 5 9 | co | |- ( c DiagFunc d ) |
| 11 | cup | |- UP |
|
| 12 | cfuc | |- FuncCat |
|
| 13 | 5 7 12 | co | |- ( d FuncCat c ) |
| 14 | 7 13 11 | co | |- ( c UP ( d FuncCat c ) ) |
| 15 | 4 | cv | |- f |
| 16 | 10 15 14 | co | |- ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) |
| 17 | 4 8 16 | cmpt | |- ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) |
| 18 | 1 3 2 2 17 | cmpo | |- ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) |
| 19 | 0 18 | wceq | |- Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) |