TheoremStatement: Literature-sourcedProof: 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.

A weighted limit is an end of powers and a weighted colimit a coend of copowers

Statement

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

Limit clause. Suppose given a functorial choice of powers: a functor $T : J^{o p} \times J \to M$ together with bijections

$η : M (m, T (c_{1}, c_{2})) ≅ S e t (W c_{1}, M (m, D c_{2}))$

natural in $m$ , in $c_{1}$ and in $c_{2}$ , so that each $T (c_{1}, c_{2})$ is a power $(D c_{2})^{W c_{1}}$ (The power and the copower of an object by a set, The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category). Then the wedges over $T$ with vertex $m$ correspond bijectively and naturally in $m$ to the natural transformations $W \Rightarrow M (m, D -)$ (Wedges and cowedges, and the categories they form, Natural transformation and its components). Consequently $T$ has an end exactly when ${W, D}$ exists (The end and the coend of a functor $C^{o p} \times C \to D$ ), and then

${W, D} = \int_{c} (D c)^{W c} .$

Colimit clause. For a weight $W : J^{o p} \to S e t$ (Opposite category $C^{o p}$ ) and a functorial choice of copowers $T^{'} (c_{1}, c_{2}) = W c_{1} \cdot D c_{2}$ , with bijections $M (T^{'} (c_{1}, c_{2}), m) ≅ S e t (W c_{1}, M (D c_{2}, m))$ natural in all three variables, the cowedges under $T^{'}$ with vertex $m$ correspond to the natural transformations $W \Rightarrow M (D -, m)$ , so $T^{'}$ has a coend exactly when $W ⋆ D$ exists, and then $W ⋆ D = \int^{c} W c \cdot D c$ .

The hypothesis is the functorial choice of the displayed powers. Existence of the displayed end and existence of the weighted limit are equivalent conclusions; neither is assumed. Completeness of $M$ is not assumed.

Facts & Assumptions

Given: A small $J$ , a locally small $M$ , a diagram $D$ , a weight $W$ , and a functorial choice of powers, respectively of copowers, as displayed.

[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$ ; a weighted colimit is characterised dually by $M (W ⋆ D, m) ≅ [J^{o p}, S e t] (W, M (D -, m))$ (Set-weighted limits and colimits).

[F2]

The power $(D c_{2})^{W c_{1}}$ is the weighted limit of the one-object diagram at the constant weight $S$ with $S = W c_{1}$ , characterised by a bijection $M (m, (D c_{2})^{W c_{1}}) ≅ S e t (W c_{1}, M (m, D c_{2}))$ natural in $m$ ; the copower is characterised dually (The power and the copower of an object by a set).

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

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

[F6]

A representation of a functor is an object together with a natural isomorphism from the corresponding hom-functor; The pair $(R, θ)$ is a representation of $F$ , and $R$ is a representing object (Presheaves, covariantly and contravariantly representable functors, and representations).

[F7]

A wedge from $d$ to $T$ is a dinatural transformation from a constant functor to $T$ : a family $ω_{c} : d \to T (c, c)$ with $T (1_{c}, f) \circ ω_{c} = T (f, 1_{c^{'}}) \circ ω_{c^{'}}$ ; a cowedge satisfies $ρ_{c} \circ T (f, 1_{c}) = ρ_{c^{'}} \circ T (1_{c^{'}}, f)$ ; a morphism of either is a morphism of the vertices commuting with every component (Wedges and cowedges, and the categories they form).

[F3]

An end of $T$ is a terminal object of the category of wedges over $T$ and a coend an initial object of the category of cowedges under $T$ ; in short, an end is a terminal wedge and a coend an initial cowedge (The end and the coend of a functor $C^{o p} \times C \to D$ ).

[F8]

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

Proof

technique · direct

1.1

A family $ω_{c} : m \to T (c, c)$ corresponds, componentwise under $η$ , to a family of functions ${\hat{ω}}_{c} : W c \to M (m, D c)$ , and the correspondence is a bijection because each $η$ is.

F1F2F4

2.1

The family $ω$ satisfies the wedge equation at $f : c \to c^{'}$ exactly when $\hat{ω}$ satisfies the naturality equation at $f$ . Both sides of the wedge equation are morphisms $m \to T (c, c^{'})$ , and applying $η$ at $(c, c^{'})$ turns them into functions $W c \to M (m, D c^{'})$ : naturality of $η$ in the covariant slot at $f$ sends $T (1_{c}, f) \circ ω_{c}$ to $x \mapsto D (f) \circ {\hat{ω}}_{c} (x)$ , and naturality of $η$ in the contravariant slot at $f$ sends $T (f, 1_{c^{'}}) \circ ω_{c^{'}}$ to $x \mapsto {\hat{ω}}_{c^{'}} (W (f) (x))$ . Their equality for every $x \in W c$ is the equation $M (m, D f) \circ {\hat{ω}}_{c} = {\hat{ω}}_{c^{'}} \circ W (f)$ , which by [F5] is naturality of $\hat{ω}$ as a transformation $W \Rightarrow M (m, D -)$ ; and since $η$ is a bijection the implication runs in both directions.

F4F5F7step 1.1

3.1

The correspondence of steps 1.1 and 2.1 is natural in $m$ , because $η$ is, so a morphism $h : m^{'} \to m$ carries the wedge $ω$ to the wedge $ω h$ and the transformation $\hat{ω}$ to $\hat{ω}$ postcomposed with $M (h, D -)$ . Hence a terminal wedge over $T$ is exactly a representing object for $m \mapsto [J, S e t] (W, M (m, D -))$ in the sense of [F6], so by [F1] and [F3] the end of $T$ exists exactly when ${W, D}$ does, and the two are the same object.

F1F3F6step 2.1

4.1

For the colimit clause, a family $ρ_{c} : T^{'} (c, c) \to m$ corresponds under the copower bijections to functions ${\hat{ρ}}_{c} : W c \to M (D c, m)$ , and applying the bijection at $(c^{'}, c)$ to the two sides of the cowedge equation at $f : c \to c^{'}$ gives $y \mapsto {\hat{ρ}}_{c} (W (f) (y))$ and $y \mapsto {\hat{ρ}}_{c^{'}} (y) \circ D (f)$ for $y \in W c^{'}$ ; their equality is the naturality equation of $\hat{ρ}$ as a transformation of presheaves on $J$ , using [F8] to read $W$ and $M (D -, m)$ on $J^{o p}$ . The correspondence is natural in $m$ , so an initial cowedge under $T^{'}$ is exactly a representing object for $m \mapsto [J^{o p}, S e t] (W, M (D -, m))$ , and the coend of $T^{'}$ exists exactly when $W ⋆ D$ does.

F1F3F5F6F7F8step 3.1∎

Remarks

The functorial choice of powers is genuine extra data and is stated as a hypothesis rather than derived. A power is determined only up to isomorphism by its universal property, so a choice of one power for each pair $(c_{1}, c_{2})$ is not by itself a functor on $J^{o p} \times J$ ; what makes the displayed end meaningful is that the choice carries a functor structure whose bijections are natural in both index variables.

Nothing in the argument assumes $M$ complete, or the weight or the diagram to be of any particular kind. What it assumes is exactly that the objects written down exist, and the conclusion is an equivalence of existence in both directions, not only a formula valid when everything is available.

Depends on

Used by

Nothing in the library uses this result yet.

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

E. Riehl, Categorical Homotopy Theory, (7.1.3) (standard reference, not scraped)