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 = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | clmd | ⊢ Limit | |
| 1 | vc | ⊢ 𝑐 | |
| 2 | cvv | ⊢ V | |
| 3 | vd | ⊢ 𝑑 | |
| 4 | vf | ⊢ 𝑓 | |
| 5 | 3 | cv | ⊢ 𝑑 |
| 6 | cfunc | ⊢ Func | |
| 7 | 1 | cv | ⊢ 𝑐 |
| 8 | 5 7 6 | co | ⊢ ( 𝑑 Func 𝑐 ) |
| 9 | coppf | ⊢ oppFunc | |
| 10 | cdiag | ⊢ Δfunc | |
| 11 | 7 5 10 | co | ⊢ ( 𝑐 Δfunc 𝑑 ) |
| 12 | 11 9 | cfv | ⊢ ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) |
| 13 | coppc | ⊢ oppCat | |
| 14 | 7 13 | cfv | ⊢ ( oppCat ‘ 𝑐 ) |
| 15 | cup | ⊢ UP | |
| 16 | cfuc | ⊢ FuncCat | |
| 17 | 5 7 16 | co | ⊢ ( 𝑑 FuncCat 𝑐 ) |
| 18 | 17 13 | cfv | ⊢ ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) |
| 19 | 14 18 15 | co | ⊢ ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) |
| 20 | 4 | cv | ⊢ 𝑓 |
| 21 | 12 20 19 | co | ⊢ ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) |
| 22 | 4 8 21 | cmpt | ⊢ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) ) |
| 23 | 1 3 2 2 22 | cmpo | ⊢ ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) ) ) |
| 24 | 0 23 | wceq | ⊢ Limit = ( 𝑐 ∈ V , 𝑑 ∈ V ↦ ( 𝑓 ∈ ( 𝑑 Func 𝑐 ) ↦ ( ( oppFunc ‘ ( 𝑐 Δfunc 𝑑 ) ) ( ( oppCat ‘ 𝑐 ) UP ( oppCat ‘ ( 𝑑 FuncCat 𝑐 ) ) ) 𝑓 ) ) ) |