Definition df-cmd 49639

Description: A co-cone (or cocone) to a diagram (see df-lmd 49638 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 49655). The naturality guarantees that the combination of the diagram with the co-cone must commute (coccom 49657). 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 49659). Definition 11.27(2) of [Adamek] p. 202.

Initial objects (initocmd 49662), coproducts, coequalizers, pushouts, and direct limits can be considered as colimits of some diagram; colimits can be further generalized as left Kan extensions (cmdlan 49665).

"cmd" is short for "colimit of a diagram". See df-lmd 49638 for the dual concept (lmddu 49660, cmddu 49661). (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 49637	. 2 class Colimit
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		cvv 3450	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	3	cv 1539	. . . . 5 class 𝑑
7	2	cv 1539	. . . . 5 class 𝑐
8		cfunc 17823	. . . . 5 class Func
9	6, 7, 8	co 7390	. . . 4 class (𝑑 Func 𝑐)
10		cdiag 18180	. . . . . 6 class Δfunc
11	7, 6, 10	co 7390	. . . . 5 class (𝑐Δfunc𝑑)
12	5	cv 1539	. . . . 5 class 𝑓
13		cfuc 17914	. . . . . . 7 class FuncCat
14	6, 7, 13	co 7390	. . . . . 6 class (𝑑 FuncCat 𝑐)
15		cup 49166	. . . . . 6 class UP
16	7, 14, 15	co 7390	. . . . 5 class (𝑐 UP (𝑑 FuncCat 𝑐))
17	11, 12, 16	co 7390	. . . 4 class ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓)
18	5, 9, 17	cmpt 5191	. . 3 class (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((𝑐Δfunc𝑑)(𝑐 UP (𝑑 FuncCat 𝑐))𝑓))
19	2, 3, 4, 4, 18	cmpo 7392	. 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  49641  cmdfval  49643