TheoremStatement: Literature-sourcedProof: AI-generatedSession-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 weighted limit is an ordinary limit over the category of elements of the weight, and a weighted colimit an ordinary colimit over it

Statement

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

Limit clause. Let $W : J \to S e t$ be a weight, let $\int W$ be its category of elements (The category of elements of a covariant functor or a presheaf) and let $π : \int W \to J$ be the projection $(c, x) \mapsto c$ . Then a weighted limit is an ordinary limit over the category of elements of the weight (Set-weighted limits and colimits, Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties): the cones over $F π$ with apex $m$ are exactly the natural transformations $W \Rightarrow M (m, F -)$ , so ${W, F}$ exists exactly when $\lim_{\int W} F π$ does and then ${W, F} = \lim_{\int W} F π$ .

Colimit clause. Let $W : J^{o p} \to S e t$ be a weight (Opposite category $C^{o p}$ ), let $\int W$ be its category of elements, whose morphisms $(c, x) \to (d, y)$ are the $f : c \to d$ of $J$ with $x = W (f) (y)$ , and let $π$ again be the projection. Then a weighted colimit is an ordinary colimit over it: the cocones under $F π$ with apex $m$ are exactly the natural transformations $W \Rightarrow M (F -, m)$ , so $W ⋆ F$ exists exactly when ${colim}_{\int W} F π$ does and then $W ⋆ F = {colim}_{\int W} F π$ .

Both clauses use the published category of elements as it stands, with no opposite inserted, and if $J$ is small then $\int W$ is small.

Facts & Assumptions

Given: A small $J$ , a locally small $M$ , a diagram $F : J \to M$ , and a weight $W$ of the variance named in each clause.

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

[F2]

The category of elements $\int G$ of a functor $G : C \to S e t$ has objects $(c, x)$ with $c \in C$ and $x \in G (c)$ ; its identities and composition are those of $C$ (The category of elements of a covariant functor or a presheaf).

[F3]

For a covariant $G$ , a morphism $(c, x) \to (d, y)$ of $\int G$ is a morphism $f : c \to d$ in $C$ satisfying $G (f) (x) = y$ (The category of elements of a covariant functor or a presheaf).

[F11]

For a presheaf $P$ , a morphism $(c, x) \to (d, y)$ of $\int P$ is a morphism $f : c \to d$ in $C$ satisfying $x = P (f) (y) .$ (The category of elements of a covariant functor or a presheaf).

[F4]

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$ , and a morphism of cones is $h$ with $λ_{j}^{'} h = λ_{j}$ (Constant diagrams, cones, cocones, and their morphisms).

[F9]

A cocone under $D$ with apex $c$ is a family $ρ_{j} : D (j) \to c$ satisfying $ρ_{k} D (u) = ρ_{j}$ for $u : j \to k$ (Constant diagrams, cones, cocones, and their morphisms).

[F5]

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

[F10]

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

[F6]

The covariant hom-assignment 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).

[F12]

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

[F7]

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

[F8]

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

[L1]

Two representing objects of one functor are joined by a unique compatible isomorphism: There is a unique isomorphism $i : R \to R^{'}$ satisfying the compatibility equation with the universal elements (Representing objects are unique up to a unique isomorphism compatible with their universal elements).

Proof

technique · direct

1.1

Fix $m$ . A natural transformation $α : W \Rightarrow M (m, F -)$ assigns to each object $c$ of $J$ a function $α_{c} : W (c) \to M (m, F c)$ . A cone over $F π$ with apex $m$ assigns to each object $(c, x)$ of $\int W$ a morphism $λ_{(c, x)} : m \to F (c)$ , since $F π (c, x) = F (c)$ . So both are families of morphisms $m \to F (c)$ indexed by the pairs $(c, x)$ with $x \in W (c)$ .

F1F2F6F7

1.2

If $J$ is small then $\int W$ is small. Its objects are the pairs $(c, x)$ with $c$ in the set $Ob (J)$ and $x$ in the set $W (c)$ , so they form a set; and a morphism of $\int W$ carries its domain, its codomain and the underlying morphism of $J$ , so the morphisms form a subclass of $Ob (\int W) \times Ob (\int W) \times Mor (J)$ and hence a set. No choice is used.

F2F3F8given

2.1

Setting $λ_{(c, x)} : = α_{c} (x)$ matches the two families of step 1.1 bijectively, and it matches the two conditions as well. Naturality of $α$ at $f : c \to d$ says $F (f) \circ α_{c} (x) = α_{d} (W (f) (x))$ for every $x \in W (c)$ . A morphism $(c, x) \to (d, y)$ of $\int W$ is an $f : c \to d$ with $W (f) (x) = y$ , and the cone condition at it says $F (f) \circ λ_{(c, x)} = λ_{(d, y)}$ . Substituting $y = W (f) (x)$ makes these the same equation, so the two conditions are one equation and not merely equivalent ones.

F2F3F4step 1.1

3.1

The bijection of step 2.1 is natural in $m$ : precomposing every $λ_{(c, x)}$ with $h : m^{'} \to m$ corresponds to postcomposing every $α_{c}$ with $M (h, F c)$ , and it carries a morphism of cones to a morphism of the transformations and back. So a terminal cone over $F π$ is exactly a representing object for $m \mapsto [J, S e t] (W, M (m, F -))$ ; by [F1] and [F5] the weighted limit exists exactly when the ordinary limit does and the two are the same object, unique by [L1].

F1F4F5L1step 2.1

3.2

For the colimit clause the same matching is made in the other variance. A cocone under $F π$ with apex $m$ assigns $λ_{(c, x)} : F (c) \to m$ to every object of $\int W$ and satisfies $λ_{(d, y)} \circ F (f) = λ_{(c, x)}$ for every morphism $(c, x) \to (d, y)$ , which by [F11] is an $f : c \to d$ of $J$ with $x = W (f) (y)$ . A natural transformation $α : W \Rightarrow M (F -, m)$ of presheaves on $J$ assigns $α_{c} : W (c) \to M (F c, m)$ and its naturality equation at $f$ reads $α_{c} (W (f) (y)) = α_{d} (y) \circ F (f)$ for $y \in W (d)$ . Setting $λ_{(c, x)} : = α_{c} (x)$ and substituting $x = W (f) (y)$ makes the two families and the two equations the same.

F7F9F11F12step 2.1

4.1

The bijection of step 3.2 is natural in $m$ by the same computation with postcomposition in place of precomposition, so an initial cocone under $F π$ is exactly a representing object for $m \mapsto [J^{o p}, S e t] (W, M (F -, m))$ : the weighted colimit exists exactly when the ordinary colimit over $\int W$ does, and then they agree.

F1F10L1step 3.2∎

Remarks

The published category of elements is used exactly as defined, with no opposite inserted. Its projection to $J$ is covariant in both the covariant and the presheaf case, and the colimit is taken over $\int W$ itself. A source that forms the category of elements of the weight viewed as a covariant functor on $J^{o p}$ will write "the opposite category of elements" for the same category read backwards; inserting an $o p$ here to match that phrase would reverse the variance and make the statement false.

No choice principle is used. What is matched at every step is a whole family against a whole family, and at no point is an element of any $W (c)$ selected. The smallness count of step 1.2 is recorded because the existence corollary for weighted limits spends exactly it.

Depends on

Used by

Dependency tree · two levels

22 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, (7.1.8) and (7.2.4) (standard reference, not scraped)
G. M. Kelly, Basic Concepts of Enriched Category Theory (TAC Reprints 10), (3.33)-(3.34) (standard reference, not scraped)