Definition df-lmd

Description: A diagram of type D or a D -shaped diagram in a category C , is a functor F : D --> C where the source category D , usually small or even finite, is called the index category or the scheme of the diagram. The actual objects and morphisms in D 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 C patterned on D . Definition 11.1(1) of Adamek p. 193.

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

A limit of a diagram F : D --> C of type D in category C is a universal pair from the diagonal functor ( C DiagFunc D ) 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 ). 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 ).

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

	Ref	Expression
Assertion	df-lmd	Could not format assertion : No typesetting found for |- Limit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmd	Could not format Limit : No typesetting found for class Limit 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		coppf	Could not format oppFunc : No typesetting found for class oppFunc with typecode class
10		cdiag	$$class{\Delta }_{\mathrm{func}}$$
11	7 5 10	co	$$class\left(c{\Delta }_{\mathrm{func}}d\right)$$
12	11 9	cfv	Could not format ( oppFunc ` ( c DiagFunc d ) ) : No typesetting found for class ( oppFunc ` ( c DiagFunc d ) ) with typecode class
13		coppc	$$class\mathrm{oppCat}$$
14	7 13	cfv	$$class\mathrm{oppCat}\left(c\right)$$
15		cup	Could not format UP : No typesetting found for class UP with typecode class
16		cfuc	$$class\mathrm{FuncCat}$$
17	5 7 16	co	$$class\left(d\mathrm{FuncCat}c\right)$$
18	17 13	cfv	$$class\mathrm{oppCat}\left(d\mathrm{FuncCat}c\right)$$
19	14 18 15	co	Could not format ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) : No typesetting found for class ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) with typecode class
20	4	cv	$$setvarf$$
21	12 20 19	co	Could not format ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) : No typesetting found for class ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) with typecode class
22	4 8 21	cmpt	Could not format ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) : No typesetting found for class ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) with typecode class
23	1 3 2 2 22	cmpo	Could not format ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) : No typesetting found for class ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) with typecode class
24	0 23	wceq	Could not format Limit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) : No typesetting found for wff Limit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) with typecode wff