Definition df-cmd 49468

Description: A co-cone (or cocone) to a diagram (see df-lmd 49467 for definition), or a natural sink for a diagram in a category 𝐶 is a pair of an object 𝑋 in 𝐶 and a natural transformation from the diagram to the constant functor (or constant diagram) of the object 𝑋. The second component associates each object in the index category with a morphism in 𝐶 whose codomain is 𝑋 (coccl 49480). The naturality guarantees that the combination of the diagram with the co-cone must commute (coccom 49482). Definition 11.27(1) of [Adamek] p. 202.

A colimit of a diagram 𝐹:𝐷⟶𝐶 of type 𝐷 in category 𝐶 is a universal pair from the diagram to the diagonal functor (𝐶Δ_func𝐷). 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 49484). 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 49432).

"cmd" is short for "colimit of a diagram". See df-lmd 49467 for the dual concept. (Contributed by Zhi Wang, 12-Nov-2025.)

Assertion

Ref	Expression
df-cmd	⊢ Colimit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)))

Distinct variable group:   𝑐,𝑑,𝑓

Detailed syntax breakdown of Definition df-cmd

Step	Hyp	Ref	Expression
1		ccmd 49466	. 2 class Colimit
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		cvv 3459	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	3	cv 1539	. . . . 5 class 𝑑
7	2	cv 1539	. . . . 5 class 𝑐
8		cfunc 17865	. . . . 5 class Func
9	6, 7, 8	co 7403	. . . 4 class (𝑑 Func 𝑐)
10		cdiag 18222	. . . . . 6 class Δfunc
11	7, 6, 10	co 7403	. . . . 5 class (𝑐Δfunc𝑑)
12	5	cv 1539	. . . . 5 class 𝑓
13		cfuc 17956	. . . . . . 7 class FuncCat
14	6, 7, 13	co 7403	. . . . . 6 class (𝑑 FuncCat 𝑐)
15		cup 49056	. . . . . 6 class UP
16	7, 14, 15	co 7403	. . . . 5 class (𝑐 UP (𝑑 FuncCat 𝑐))
17	11, 12, 16	co 7403	. . . 4 class ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)
18	5, 9, 17	cmpt 5201	. . 3 class (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓))
19	2, 3, 4, 4, 18	cmpo 7405	. 2 class (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)))
20	1, 19	wceq 1540	1 wff Colimit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)))

This definition is referenced by:  reldmcmd  49470  cmdfval  49472