TheoremStatement: AI-adaptedProof: 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.

A weighted limit and a weighted colimit are unique up to a unique compatible isomorphism

Statement

Let $J$ be small, $M$ locally small, $D : J \to M$ a diagram and $W : J \to S e t$ a weight (Set-weighted limits and colimits).

If $L$ and $L^{'}$ are weighted limits ${W, D}$ , with counit cylinders $κ$ and $κ^{'}$ , there is exactly one isomorphism $i : L \to L^{'}$ satisfying $κ_{j}^{'} (w) \circ i = κ_{j} (w)$ for every object $j$ of $J$ and every $w \in W (j)$ .

Dually, for a weight $W : J^{o p} \to S e t$ , any two weighted colimits $W ⋆ D$ are joined by exactly one isomorphism commuting with the components of their counit cylinders.

Facts & Assumptions

Given: A small $J$ , a locally small $M$ , a diagram $D$ , a weight $W$ , and two weighted limits, respectively two weighted colimits, of that data.

[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, the counit cylinder being the natural transformation corresponding to the identity; dually for a weighted colimit (Set-weighted limits and colimits).

[F3]

A presheaf $P$ is contravariantly representable when there is an object $R$ and a natural isomorphism $θ : C (-, R) \Rightarrow P$ ; The pair $(R, θ)$ is a representation of $F$ , and $R$ is a representing object, with the covariant case using $C (R, -)$ (Presheaves, covariantly and contravariantly representable functors, and representations).

[F2]

A universal element of a presheaf $P$ is a pair $(R, u)$ with $u \in P (R)$ such that the maps $θ_{c}^{u} : C (c, R) ⟶ P (c), θ_{c}^{u} (f) = P (f) (u)$ are the components of a natural isomorphism; for a covariant $F$ the maps are $θ_{c}^{u} (f) = F (f) (u)$ on $C (R, c)$ . A universal element is therefore a representation whose isomorphism is named by a distinguished element (Universal elements of covariant functors and presheaves).

[L1]

If a presheaf $P$ has universal elements $(R, u)$ and $(R^{'}, u^{'})$ , There is a unique isomorphism $i : R \to R^{'}$ satisfying $P (i) (u^{'}) = u$ ; the covariant clause is the same statement with $F (i) (u) = u^{'}$ (Representing objects are unique up to a unique isomorphism compatible with their universal elements).

Proof

technique · direct

1.1

Write $Φ (m) : = [J, S e t] (W, M (m, D -))$ , a presheaf on $M$ . By [F1] a weighted limit is exactly a representing object for $Φ$ in the contravariant sense of [F3], so the data " $L$ is a weighted limit" and " $L$ represents $Φ$ " are the same data.

F1F3

2.1

The counit cylinder is the universal element of that representation: under the representing isomorphism $θ : M (-, L) \Rightarrow Φ$ , the element $κ : = θ_{L} (1_{L})$ lies in $Φ (L)$ and satisfies $θ_{m} (h) = Φ (h) (κ)$ for every $h : m \to L$ , which is the display of [F2]; conversely a universal element determines the representing isomorphism by that same formula. Componentwise $Φ (h) (κ)_{j} (w) = κ_{j} (w) \circ h$ , so the equation of the Statement, $κ_{j}^{'} (w) \circ i = κ_{j} (w)$ , is exactly $Φ (i) (κ^{'}) = κ$ . This identification is the whole content of the theorem.

F1F2F3step 1.1

3.1

By [L1] applied to $Φ$ with the two universal elements $κ$ and $κ^{'}$ , there is exactly one isomorphism $i : L \to L^{'}$ with $Φ (i) (κ^{'}) = κ$ ; by step 2.1 that is exactly one isomorphism with $κ_{j}^{'} (w) \circ i = κ_{j} (w)$ for every $j$ and every $w$ .

L1step 2.1

4.1

For weighted colimits the represented functor $m \mapsto [J^{o p}, S e t] (W, M (D -, m))$ is covariant in $m$ , so steps 1.1 to 3.1 run with the covariant halves of [F2], [F3] and [L1] in place of the contravariant ones, and give exactly one isomorphism between two weighted colimits commuting with every component of the counit cylinders.

L1step 3.1∎

Remarks

A weighted limit is not merely like a representing object; by the definition in force here it is one, and every property of representations transfers without a separate argument. What has to be said explicitly is only which element of the represented set is the universal one, and that is the counit cylinder.

Uniqueness is up to a unique compatible isomorphism. Two weighted limits of the same data are isomorphic in many ways in general; exactly one of those isomorphisms respects the counit cylinders, and it is that one the statement produces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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