PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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 weighted limit of a set-valued diagram is the set of natural transformations from the weight

Statement

Let $J$ be a small category and let $W, D : J \to S e t$ be functors (Sets and functions form the large locally small category $S e t$ ). Then the weighted limit of $D$ by $W$ in $S e t$ exists, and a weighted limit of a set-valued diagram is the set of natural transformations from the weight (Set-weighted limits and colimits, Functor category $[C, D]$ ):

${W, D} = [J, S e t] (W, D) = Nat (W, D) .$

Its counit cylinder is $κ_{j} (w) (α) = α_{j} (w)$ , and its elements are exactly the natural transformations $W \Rightarrow D$ (Natural transformation and its components).

Facts & Assumptions

Given: A small category $J$ and two functors $W, D : J \to S e t$ .

[F2]

Sets as objects and functions as morphisms form a large locally small category $S e t$ (Sets and functions form the large locally small category $S e t$ ).

[F6]

The functor category $[C, D]$ has functors $C \to D$ as objects and natural transformations as morphisms (Functor category $[C, D]$ ).

[L1]

If $C$ is small and $D$ is locally small, then $[C, D]$ is locally small (If $C$ is small and $D$ is locally small then $[C, D]$ is locally small; if both are small it is small).

[F4]

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

[F1]

A weighted limit ${W, D}$ is an object that represents the functor sending an object to the set of natural transformations from the weight, that is $M (m, {W, D}) ≅ [J, S e t] (W, M (m, D -))$ naturally in $m$ , the counit cylinder corresponding to the identity (Set-weighted limits and colimits).

[F5]

A natural transformation $α : F \Rightarrow G$ is a family $α_{A} : F A \to G A$ such that every $f : A \to B$ satisfies the naturality equation $G f \circ α_{A} = α_{B} \circ F f$ (Natural transformation and its components).

[F3]

The singleton ${x}$ is the set whose only element is $x$ : $t \in {x} \leftrightarrow t = x$ (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ).

Proof

technique · direct

1.1F1F2F4F6L1

Since $J$ is small and $S e t$ is locally small, [L1] and [F6] make $N : = [J, S e t] (W, D)$ a set, and likewise $Φ (X) : = [J, S e t] (W, S e t (X, D -))$ a set for every set $X$ , the functor $S e t (X, D -)$ being the covariant hom-functor of [F4] composed with $D$ .

2.1F4F5step 1.1

For a set $X$ the assignments $h \mapsto α$ with $α_{j} (w) (x) = h (x)_{j} (w)$ , and $α \mapsto h$ with $h (x)_{j} (w) = α_{j} (w) (x)$ , are mutually inverse bijections between $S e t (X, N)$ and $Φ (X)$ : each is defined by the same formula read in the two directions, and each side of the correspondence satisfies its naturality condition exactly when the other does, since $D (u) (h (x)_{j} (w)) = h (x)_{k} (W (u) (w))$ for all $x$ is the same family of equations as $S e t (X, D (u)) \circ α_{j} = α_{k} \circ W (u)$ .

3.1F1F5step 2.1

The bijection of step 2.1 is natural in $X$ : for $g : X^{'} \to X$ the family attached to $h \circ g$ has components $w \mapsto (x^{'} \mapsto h (g (x^{'}))_{j} (w))$ , which is the family attached to $h$ postcomposed with $S e t (g, D j)$ . So $N$ represents $Φ$ in the sense of [F1] and is a weighted limit ${W, D}$ ; its counit cylinder is the family attached to the identity of $N$ , namely $κ_{j} (w) (α) = α_{j} (w)$ .

4.1F3F4step 3.1∎

Taking $X$ to be a one-element set ${*}$ reads off the elements: by [F3] a function ${*} \to Y$ is determined by its single value, so $S e t ({*}, N)$ is in bijection with $N$ and $Φ ({*})$ with $[J, S e t] (W, D)$ , and step 3.1 identifies the two. Hence an element of ${W, D}$ is exactly a natural transformation $W \Rightarrow D$ .

Remarks

Naturality in the test object is what makes this an identification of the represented functors rather than a bijection of two sets that happen to have the same size. Step 4.1 alone, evaluating at a one-element set, would compute the underlying set of a weighted limit already known to exist; it is step 3.1 that produces one.

The proposition is the reason the weighted limit is called a limit "weighted by $W$ ": in $S e t$ it is literally the set of $W$ -shaped families in $D$ , and every other target is compared to this case through a representable, which is A representable functor carries a weighted limit to the weighted limit of the composed diagram.

Depends on

Used by

Dependency tree · two levels

21 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.7) (standard reference, not scraped)