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	⊢ Colimit = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( 𝑐 Δfunc 𝑑 ) ( 𝑐 UP ( 𝑑 FuncCat 𝑐 ) ) 𝑓 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmd	⊢ Colimit
1		vc	⊢ 𝑐
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		vf	⊢ 𝑓
5	3	cv	⊢ 𝑑
6		cfunc	⊢ Func
7	1	cv	⊢ 𝑐
8	5 7 6	co	⊢ ( 𝑑 Func 𝑐 )
9		cdiag	⊢ Δfunc
10	7 5 9	co	⊢ ( 𝑐 Δfunc 𝑑 )
11		cup	⊢ UP
12		cfuc	⊢ FuncCat
13	5 7 12	co	⊢ ( 𝑑 FuncCat 𝑐 )
14	7 13 11	co	⊢ ( 𝑐 UP ( 𝑑 FuncCat 𝑐 ) )
15	4	cv	⊢ 𝑓
16	10 15 14	co	⊢ ( ( 𝑐 Δfunc 𝑑 ) ( 𝑐 UP ( 𝑑 FuncCat 𝑐 ) ) 𝑓 )
17	4 8 16	cmpt	⊢ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( 𝑐 Δfunc 𝑑 ) ( 𝑐 UP ( 𝑑 FuncCat 𝑐 ) ) 𝑓 ) )
18	1 3 2 2 17	cmpo	⊢ ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( 𝑐 Δfunc 𝑑 ) ( 𝑐 UP ( 𝑑 FuncCat 𝑐 ) ) 𝑓 ) ) )
19	0 18	wceq	⊢ Colimit = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( 𝑐 Δfunc 𝑑 ) ( 𝑐 UP ( 𝑑 FuncCat 𝑐 ) ) 𝑓 ) ) )