Definition df-lmd 49467

Description: A diagram of type 𝐷 or a 𝐷-shaped diagram in a category 𝐶, is a functor 𝐹:𝐷⟶𝐶 where the source category 𝐷, usually small or even finite, is called the index category or the scheme of the diagram. The actual objects and morphisms in 𝐷 are largely irrelevant; only the way in which they are interrelated matters. The diagram is thought of as indexing a collection of objects and morphisms in 𝐶 patterned on 𝐷. Definition 11.1(1) of [Adamek] p. 193.

A cone to a diagram, or a natural source for a diagram in a category 𝐶 is a pair of an object 𝑋 in 𝐶 and a natural transformation from the constant functor (or constant diagram) of the object 𝑋 to the diagram. The second component associates each object in the index category with a morphism in 𝐶 whose domain is 𝑋 (concl 49479). The naturality guarantees that the combination of the diagram with the cone must commute (concom 49481). Definition 11.3(1) of [Adamek] p. 193.

A limit of a diagram 𝐹:𝐷⟶𝐶 of type 𝐷 in category 𝐶 is a universal pair from the diagonal functor (𝐶Δ_func𝐷) to the diagram. The universal pair is a cone to the diagram satisfying the universal property, that each cone to the diagram uniquely factors through the limit (islmd 49483). Definition 11.3(2) of [Adamek] p. 194.

Terminal objects, products, equalizers, pullbacks, and inverse limits can be considered as limits of some diagram; limits can be further generalized as right Kan extensions (df-ran 49433).

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

Assertion

Ref	Expression
df-lmd	⊢ Limit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((oppFunc‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓)))

Distinct variable group:   𝑐,𝑑,𝑓

Detailed syntax breakdown of Definition df-lmd

Step	Hyp	Ref	Expression
1		clmd 49465	. 2 class Limit
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	. . . . . . 7 class Δfunc
11	7, 6, 10	co 7403	. . . . . 6 class (𝑐Δfunc𝑑)
12		coppf 49019	. . . . . 6 class oppFunc
13	11, 12	cfv 6530	. . . . 5 class (oppFunc‘(𝑐Δfunc𝑑))
14	5	cv 1539	. . . . 5 class 𝑓
15		coppc 17721	. . . . . . 7 class oppCat
16	7, 15	cfv 6530	. . . . . 6 class (oppCat‘𝑐)
17		cfuc 17956	. . . . . . . 8 class FuncCat
18	6, 7, 17	co 7403	. . . . . . 7 class (𝑑 FuncCat 𝑐)
19	18, 15	cfv 6530	. . . . . 6 class (oppCat‘(𝑑 FuncCat 𝑐))
20		cup 49056	. . . . . 6 class UP
21	16, 19, 20	co 7403	. . . . 5 class ((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))
22	13, 14, 21	co 7403	. . . 4 class ((oppFunc‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓)
23	5, 9, 22	cmpt 5201	. . 3 class (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((oppFunc‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓))
24	2, 3, 4, 4, 23	cmpo 7405	. 2 class (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((oppFunc‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓)))
25	1, 24	wceq 1540	1 wff Limit = (𝑐 ∈ V, 𝑑 ∈ V ↦ (𝑓 ∈ (𝑑 Func 𝑐) ↦ ((oppFunc‘(𝑐Δfunc𝑑))((oppCat‘𝑐) UP (oppCat‘(𝑑 FuncCat 𝑐)))𝑓)))

This definition is referenced by:  reldmlmd  49469  lmdfval  49471