TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Chosen limits and colimits of a fixed small shape assemble into limit and colimit functors

Statement

Let $J$ be small. If a particular limiting cone is chosen for every $D : J \to C$ , these choices define a functor

$\lim_{J} : [J, C] \to C .$

Chosen colimiting cocones similarly define ${colim}_{J} : [J, C] \to C$ .

Facts & Assumptions

Given: A small $J$ and, for every $D$ , a chosen limit $(L_{D}, λ^{D})$ .

[F1]

Objects and arrows of a functor category are functors and natural transformations (Functor category $[C, D]$ , Natural transformation and its components).

[F2]

A chosen limit supplies a unique factor from every cone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F3]

Smallness is cardinality of the indexing category (Assuming Choice, cardinality of a small category and κ-small diagrams).

[L1]

Limit legs are jointly monic (The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic).

[L2]

The colimit construction is the formal dual (A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category).

Proof

technique · universal property

1.1

For $α : D \Rightarrow E$ , the family $α_{j} λ_{j}^{D} : L_{D} \to E (j)$ is a cone: for $u : j \to k$ , naturality of $α$ and the cone equation give $E (u) α_{j} λ_{j}^{D} = α_{k} D (u) λ_{j}^{D} = α_{k} λ_{k}^{D}$ .

F1F2

2.1

By [F2], there is a unique morphism $\lim α : L_{D} \to L_{E}$ satisfying $λ_{j}^{E} \lim α = α_{j} λ_{j}^{D}$ for every $j$ .

F2step 1.1

3.1

For $1_{D}$ , both $\lim (1_{D})$ and $1_{L_{D}}$ have the same composites with all $λ_{j}^{D}$ ; [L1] gives $\lim (1_{D}) = 1_{L_{D}}$ .

L1step 2.1

3.2

For $D \overset{α}{\Rightarrow} E \overset{β}{\Rightarrow} H$ , the maps $\lim (β α)$ and $(\lim β) (\lim α)$ have composite $β_{j} α_{j} λ_{j}^{D}$ with every $λ_{j}^{H}$ . By [L1] they are equal. Thus the assignments satisfy the functor laws.

L1step 2.1

4.1

The smallness in [F3] ensures that the functor category is used under the library's set-based indexing convention. Reversing every arrow in steps 1.1, 2.1, 3.1, and 3.2 by [L2] gives the chosen-colimit functor.

F3L2step 1.1step 2.1step 3.1step 3.2∎

Depends on

Used by

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, Lemma 3.4.6 (standard reference, not scraped)