False statementConstruction: AI-adaptedVerification: AI-generatedSession-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.

FALSE: every weighted limit is the ordinary limit of the diagram it weights

Statement

False claim: for every weight $W$ and every diagram $F$ , the weighted limit ${W, F}$ is the ordinary limit of $F$ (Set-weighted limits and colimits, Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

Facts & Assumptions

Given: The walking arrow $J$ , with objects $0$ and $1$ and one non-identity morphism $u : 0 \to 1$ ; the diagram $F : J \to S e t$ with $F (0)$ a two-element set and $F (1)$ a one-element set; and the weight $W : J \to S e t$ with $W (0)$ a two-element set and $W (1)$ a one-element set.

[F5]

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]

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

[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 (Set-weighted limits and colimits).

[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$ (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties).

[F3]

For a cospan $X \overset{f}{\to} Z \overset{g}{\leftarrow} Y$ , a pullback is its limit, consisting of $X \times_{Z} Y$ with two projections whose composites with $f$ and $g$ agree and through which every compatible pair factors uniquely (Pullbacks and pushouts as limits and colimits of cospans and spans).

[F4]

A set $A$ is finite when $A \approx n$ for some $n \in N$ , and then $∣ A ∣$ is that unique $n$ ; equal cardinalities mean equinumerosity (The cardinality $∣ A ∣$ of a finite set).

[L2]

For a small $J$ and set-valued $W$ and $D$ , 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).

[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).

[L3]

A weighted limit with the constant singleton weight is exactly the ordinary limit: ${Δ {*}, F} = \lim F$ (Weighting by the constant singleton gives exactly the ordinary limit).

Refutation

technique · direct

1.1

Fix the witness. Let $J$ be the walking arrow, let $F (0) = {a, b}$ and $F (1) = {*}$ with $F (u)$ the only function between them, and let $W (0) = {p, q}$ and $W (1) = {*}$ with $W (u)$ the only function between them. Both are functors, since the only equations to check involve identities.

F5F6givenconstruct

2.1

The ordinary limit of $F$ has two elements. A cone over $F$ with apex $X$ is a pair of functions $λ_{0} : X \to F (0)$ and $λ_{1} : X \to F (1)$ with $F (u) λ_{0} = λ_{1}$ , so $λ_{1}$ is determined by $λ_{0}$ and a cone is exactly a function $X \to F (0)$ ; by [F2] the limit is $F (0)$ , a set with two elements.

F2F4step 1.1

2.2

The weighted limit has four elements. By [L2] it is the set of natural transformations $W \Rightarrow F$ ; such a transformation is a pair of functions $α_{0} : {p, q} \to {a, b}$ and $α_{1} : {*} \to {*}$ , and its naturality equation at $u$ is an equation between two functions into the one-element set $F (1)$ , hence automatic. So there are exactly as many as there are functions ${p, q} \to {a, b}$ , namely four.

F1F4F6L2step 1.1

3.1

Four is not two, so ${W, F}$ is not the ordinary limit of $F$ and the claim is false. The same count follows from [L1] and [F3]: the category of elements of $W$ has the objects $(0, p)$ , $(0, q)$ and $(1, *)$ and one morphism from each of the first two to the third, so it is a cospan, and the limit of the composed diagram is the pullback of $F (u)$ along itself, which for a map from a two-element set to a one-element set has four elements.

F3L1step 2.1step 2.2

4.1

What is true is [L3]: the ordinary limit is the weighted limit at the constant singleton weight, and the witness above differs from that case exactly by having a two-element value at the object $0$ . By [L1] a larger value of the weight at an object puts more copies of that object into the category of elements, which is what changes the limit.

L1L3step 3.1∎

Remarks

The weight is doing something visible here: it duplicates the object $0$ of the index category, so the limit is taken over a diagram with two copies of $F (0)$ mapping into $F (1)$ rather than one. That is why the answer is a pullback rather than the domain of the map.

Nothing about the witness needs the sets to be small or the target to be $S e t$ in any essential way; it is stated with three finite sets so that both sides can be counted by hand and the counts compared.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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, Categorical Homotopy Theory, Example 7.1.16 (standard reference, not scraped)