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 | |- Limit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | clmd | |- Limit |
|
| 1 | vc | |- c |
|
| 2 | cvv | |- _V |
|
| 3 | vd | |- d |
|
| 4 | vf | |- f |
|
| 5 | 3 | cv | |- d |
| 6 | cfunc | |- Func |
|
| 7 | 1 | cv | |- c |
| 8 | 5 7 6 | co | |- ( d Func c ) |
| 9 | coppf | |- oppFunc |
|
| 10 | cdiag | |- DiagFunc |
|
| 11 | 7 5 10 | co | |- ( c DiagFunc d ) |
| 12 | 11 9 | cfv | |- ( oppFunc ` ( c DiagFunc d ) ) |
| 13 | coppc | |- oppCat |
|
| 14 | 7 13 | cfv | |- ( oppCat ` c ) |
| 15 | cup | |- UP |
|
| 16 | cfuc | |- FuncCat |
|
| 17 | 5 7 16 | co | |- ( d FuncCat c ) |
| 18 | 17 13 | cfv | |- ( oppCat ` ( d FuncCat c ) ) |
| 19 | 14 18 15 | co | |- ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) |
| 20 | 4 | cv | |- f |
| 21 | 12 20 19 | co | |- ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) |
| 22 | 4 8 21 | cmpt | |- ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) |
| 23 | 1 3 2 2 22 | cmpo | |- ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) |
| 24 | 0 23 | wceq | |- Limit = ( c e. _V , d e. _V |-> ( f e. ( d Func c ) |-> ( ( oppFunc ` ( c DiagFunc d ) ) ( ( oppCat ` c ) UP ( oppCat ` ( d FuncCat c ) ) ) f ) ) ) |