TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Weighting by the constant singleton gives exactly the ordinary limit

Statement

Let $J$ be small, let $M$ be locally small and let $F : J \to M$ be a diagram. Write $Δ {*}$ for the weight that is constantly a one-element set (The unordered pair ${x, y}$ and the singleton ${x} = {x, x}$ ).

Then a weighted limit with the constant singleton weight is exactly the ordinary limit (Set-weighted limits and colimits, Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties): the natural transformations $Δ {*} \Rightarrow M (m, F -)$ are exactly the cones over $F$ with apex $m$ (Constant diagrams, cones, cocones, and their morphisms), so ${Δ {*}, F}$ exists exactly when $\lim F$ does and then

${Δ {*}, F} = \lim_{j \in J} F (j) .$

Dually, for the constant singleton weight on $J^{o p}$ , the weighted colimit $Δ {*} ⋆ F$ exists exactly when $colim F$ does and then the two agree.

Facts & Assumptions

Given: A small $J$ , a locally small $M$ , a diagram $F : J \to M$ , and the constant singleton weight.

[F6]

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}$ ).

[F4]

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

[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, and a weighted colimit is characterised dually (Set-weighted limits and colimits).

[F3]

A cone over $D : J \to C$ with apex $c$ is a family $λ_{j} : c \to D (j)$ satisfying $D (u) λ_{j} = λ_{k}$ for $u : j \to k$ ; a cocone satisfies $ρ_{k} D (u) = ρ_{j}$ , and a morphism of cones is $h$ with $λ_{j}^{'} h = λ_{j}$ (Constant diagrams, cones, cocones, and their morphisms).

[F2]

A limit of $D$ is a terminal cone: explicitly, for every cone $(X, ξ)$ there exists a unique morphism $u : X \to L$ such that $λ_{j} u = ξ_{j}$ for every $j$ ; a colimit is an initial cocone (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F5]

The category of elements $\int G$ has objects $(c, x)$ with $c \in C$ and $x \in G (c)$ ; a morphism $(c, x) \to (d, y)$ is a morphism $f : c \to d$ in $C$ satisfying $G (f) (x) = y$ ; and its identities and composition are those of $C$ (The category of elements of a covariant functor or a presheaf).

[L1]

A weighted limit is an ordinary limit over the category of elements of the weight, and a weighted colimit an ordinary colimit over it (A weighted limit is an ordinary limit over the category of elements of the weight, and a weighted colimit an ordinary colimit over it).

Proof

technique · direct

1.1

A natural transformation $α : Δ {*} \Rightarrow M (m, F -)$ has components $α_{j} : {*} \to M (m, F j)$ , and by [F6] each is determined by the single morphism $λ_{j} : = α_{j} (*)$ , every function out of a one-element set being determined by its value. Naturality at $u : j \to k$ reads $F (u) \circ α_{j} (*) = α_{k} (Δ {*} (u) (*)) = α_{k} (*)$ , that is $F (u) λ_{j} = λ_{k}$ , which is the cone condition of [F3]. The correspondence $α \leftrightarrow λ$ is a bijection in both directions.

F1F3F4F6

2.1

The bijection of step 1.1 is natural in $m$ , since precomposing every $λ_{j}$ with $h : m^{'} \to m$ corresponds to postcomposing every $α_{j}$ with $M (h, F j)$ . So an object represents $m \mapsto [J, S e t] (Δ {*}, M (m, F -))$ exactly when it is a terminal cone over $F$ ; by [F1] and [F2] the weighted limit exists exactly when the ordinary limit does, and they are the same object with the same components.

F1F2F3step 1.1

2.2

For the colimit clause, a natural transformation $Δ {*} \Rightarrow M (F -, m)$ of presheaves on $J$ has components determined by morphisms $ρ_{j} : F (j) \to m$ , and its naturality equation at $u : j \to k$ reads $ρ_{k} \circ F (u) = ρ_{j}$ , the cocone condition of [F3]; the correspondence is natural in $m$ , so $Δ {*} ⋆ F$ exists exactly when $colim F$ does and the two agree.

F1F2F3step 1.1

3.1

The same conclusion follows from [L1] by a second route: the category of elements of the constant singleton weight has, by [F5], one object $(j, *)$ for each object $j$ of $J$ and one morphism for each morphism of $J$ , the defining equation being vacuous because the weight's values are one-element sets; so the projection $π$ is an isomorphism onto $J$ and $\lim_{\int W} F π$ is $\lim F$ . This is a comparison, not a redefinition: the ordinary limit is the published one and is restated nowhere.

F5L1step 2.1step 2.2∎

Remarks

The theorem is what makes "weighted" a genuine generalisation rather than a replacement: ordinary limits are the weighted limits at one particular weight, and every statement about weighted limits specialises to a statement already in the library. The specialisation is by a theorem and not by fiat, and the two routes in the proof agree.

The second route also explains the shape of the general comparison. Weighting by $W$ replaces the index category $J$ by $\int W$ , which has one copy of $j$ for each element of $W (j)$ ; the constant singleton weight leaves exactly one copy of each, and larger weights make more.

Depends on

Used by

FALSE: every weighted limit is the ordinary limit of the diagram it weights False statement
Why weights are needed once the base of enrichment is not Set Remark

Dependency tree · two levels

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