Definition df-cmd

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	Could not format assertion : No typesetting found for |- Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmd	Could not format Colimit : No typesetting found for class Colimit with typecode class
1		vc	$$setvarc$$
2		cvv	$$class\mathrm{V}$$
3		vd	$$setvard$$
4		vf	$$setvarf$$
5	3	cv	$$setvard$$
6		cfunc	$$class\mathrm{Func}$$
7	1	cv	$$setvarc$$
8	5 7 6	co	$$class\left(d\mathrm{Func}c\right)$$
9		cdiag	$$class{\Delta }_{\mathrm{func}}$$
10	7 5 9	co	$$class\left(c{\Delta }_{\mathrm{func}}d\right)$$
11		cup	Could not format UP : No typesetting found for class UP with typecode class
12		cfuc	$$class\mathrm{FuncCat}$$
13	5 7 12	co	$$class\left(d\mathrm{FuncCat}c\right)$$
14	7 13 11	co	Could not format ( c UP ( d FuncCat c ) ) : No typesetting found for class ( c UP ( d FuncCat c ) ) with typecode class
15	4	cv	$$setvarf$$
16	10 15 14	co	Could not format ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) : No typesetting found for class ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) with typecode class
17	4 8 16	cmpt	Could not format ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) : No typesetting found for class ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) with typecode class
18	1 3 2 2 17	cmpo	Could not format ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) : No typesetting found for class ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) with typecode class
19	0 18	wceq	Could not format Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) : No typesetting found for wff Colimit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( c DiagFunc d ) ( c UP ( d FuncCat c ) ) f ) ) ) with typecode wff