TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

A representable functor carries a weighted limit to the weighted limit of the composed diagram

Statement

Let $J$ be small, let $M$ be locally small (Small, locally small, and large categories), let $F : J \to M$ be a diagram and let $m$ be an object of $M$ .

Limit clause. Let $W : J \to S e t$ be a weight and suppose ${W, F}$ exists (Set-weighted limits and colimits). Then the weighted limit of the composed diagram $M (m, F -) : J \to S e t$ by the same weight exists and

$M (m, {W, F}) ≅ {W, M (m, F -)}$

(The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor).

Colimit clause. Let $W : J^{o p} \to S e t$ be a weight (Opposite category $C^{o p}$ ) and suppose $W ⋆ F$ exists. Then

$M (W ⋆ F, m) ≅ {W, M (F -, m)},$

a weighted limit in $S e t$ of the presheaf $M (F -, m) : J^{o p} \to S e t$ , not a weighted colimit: the contravariant representable turns the weighted colimit into a weighted limit over the opposite index category.

Facts & Assumptions

Given: A small $J$ , a locally small $M$ , a diagram $F$ , an object $m$ , and a weight of the variance named in each clause whose weighted limit or colimit is assumed to exist.

[F5]

A category is small when both $Ob (C)$ and $Mor (C)$ are sets; a small category is locally small (Small, locally small, and large categories).

[F2]

The covariant hom-assignment $C (a, -)$ sends $u : b \to c$ to $u_{*} : C (a, b) ⟶ C (a, c), f ⟼ u \circ f$ , and the contravariant hom-assignment sends $u$ to precomposition (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[L2]

For every locally small category the hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a functor, and its restrictions in the two variables are the contravariant and covariant hom-functors (The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor).

[F6]

The opposite category has the same objects and reverses every morphism: $C^{o p} (A, B) = C (B, A)$ (Opposite category $C^{o p}$ ).

[F1]

A weighted limit ${W, F}$ is an object that represents the functor sending an object to the set of natural transformations from the weight, that is $M (m, {W, F}) ≅ [J, S e t] (W, M (m, F -))$ naturally in $m$ ; the weighted colimit is characterised by $M (W ⋆ F, m) ≅ [J^{o p}, S e t] (W, M (F -, m))$ (Set-weighted limits and colimits).

[F3]

A representation of a functor is an object with a natural isomorphism from the corresponding hom-functor; The pair $(R, θ)$ is a representation of $F$ , and $R$ is a representing object (Presheaves, covariantly and contravariantly representable functors, and representations).

[L3]

Two representing objects of one functor are joined by a unique compatible isomorphism (Representing objects are unique up to a unique isomorphism compatible with their universal elements).

[L1]

For a small $J$ and functors $W, D : J \to S e t$ , a weighted limit of a set-valued diagram is the set of natural transformations from the weight: ${W, D} = [J, S e t] (W, D)$ (A weighted limit of a set-valued diagram is the set of natural transformations from the weight).

Proof

technique · direct

1.1

By [L2] and [F2] the assignment $M (m, F -)$ is a functor $J \to S e t$ , its values being sets because $M$ is locally small, and $J$ is small by hypothesis. So [L1] applies to the pair $W$ and $M (m, F -)$ and gives ${W, M (m, F -)} = [J, S e t] (W, M (m, F -))$ , in particular the right-hand side of the limit clause exists.

F2F5L1L2

2.1

By [F1] and [F3] the defining property of ${W, F}$ is a bijection $M (m, {W, F}) ≅ [J, S e t] (W, M (m, F -))$ natural in $m$ . Composing it with the identification of step 1.1 gives the limit clause: the hom-set of the weighted limit is canonically bijective to the weighted limit of the hom-sets, with the bijection determined by the counit cylinder and unique by [L3].

F1F3L3step 1.1

3.1

For the colimit clause, [F6] makes $M (F -, m)$ a presheaf on $J$ , that is a functor on $J^{o p}$ , which is small with $J$ ; so [L1] applied with source $J^{o p}$ identifies ${W, M (F -, m)}$ with $[J^{o p}, S e t] (W, M (F -, m))$ , and [F1] gives a canonical bijection from that set to $M (W ⋆ F, m)$ . The object produced is a weighted limit in $S e t$ over $J^{o p}$ , and calling it a weighted colimit would reverse the variance of the weight.

F1F2F6L1L3step 2.1∎

Remarks

This is the seam between the general definition and the case that can be computed. A weighted limit in an arbitrary locally small target is defined by a representation, and the theorem says that applying a representable functor turns it into the weighted limit in $S e t$ , which A weighted limit of a set-valued diagram is the set of natural transformations from the weight identifies outright. Everything that can be checked about ${W, F}$ by testing against objects of $M$ is therefore a statement about sets of natural transformations.

The colimit clause is not the dual read carelessly. Both clauses produce a weighted limit in $S e t$ , because the covariant representable preserves the shape of the universal property while the contravariant one reverses the direction of every morphism it is applied to, and the weight stays where it is.

Depends on

Used by

Nothing in the library uses this result yet.

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

G. M. Kelly, Basic Concepts of Enriched Category Theory (TAC Reprints 10), (3.8) (standard reference, not scraped)