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.
Set-weighted limits and colimits
Definition
Let be a small category, let be locally small (Small, locally small, and large categories) and let be a diagram. Because is small and is locally small, the functor category is locally small (Functor category , If is small and is locally small then is locally small; if both are small it is small, Sets and functions form the large locally small category ), so each collection of natural transformations named below is a set (Natural transformation and its components).
A weight for a limit is a functor . A weighted limit is an object of that represents the functor sending an object to the set of natural transformations from the weight (Presheaves, covariantly and contravariantly representable functors, and representations), namely
where is the covariant hom-functor composed with (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category). Written out, the isomorphism is a bijection natural in between morphisms and families of functions satisfying for every and .
A weight for a colimit is a presheaf (Opposite category ). A weighted colimit is an object of with
naturally in the second variable, where sends to and is obtained by composing the contravariant hom-functor with .
The natural transformation corresponding to the identity of is the counit cylinder of the weighted limit, with components ; dually for a weighted colimit. Neither object need exist.
Remarks
The variances are the ones that read correctly against the presheaf convention in force in this library: a weight for a limit is covariant, matching the covariant hom-functor , and a weight for a colimit is contravariant, matching . Writing a colimit weight covariantly would ask for a natural transformation between functors of opposite variance, which is not a well-formed condition.
Nothing here mentions cones. A cone over is recovered by taking the weight that is constantly a one-element set, and that this reproduces the ordinary limit is a theorem rather than a convention: Weighting by the constant singleton gives exactly the ordinary limit.
Depends on
- Functor category $[\mathcal C,\mathcal D]$
- If $\mathcal C$ is small and $\mathcal D$ is locally small then $[\mathcal C,\mathcal D]$ is locally small; if both are small it is small
- Presheaves, covariantly and contravariantly representable functors, and representations
- The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category
- Natural transformation and its components
- Small, locally small, and large categories
- Sets and functions form the large locally small category $\mathbf{Set}$
- Opposite category $\mathcal C^{\mathrm{op}}$
Used by
- A limit weighted by a Set-valued weight on a small index category exists in a complete target, and the weighted colimit in a cocomplete one Corollary
- The power and the copower of an object by a set Definition
- A weighted limit computing a kernel pair Example
- FALSE: every weighted limit is the ordinary limit of the diagram it weights False statement
- A weighted limit of a set-valued diagram is the set of natural transformations from the weight Proposition
- Why weights are needed once the base of enrichment is not Set Remark
- A coend is a colimit weighted by the hom-bifunctor, and an end a limit weighted by it Theorem
- A representable functor carries a weighted limit to the weighted limit of the composed diagram Theorem
- A weighted limit and a weighted colimit are unique up to a unique compatible isomorphism Theorem
- A weighted limit is an end of powers and a weighted colimit a coend of copowers Theorem
- A weighted limit is an ordinary limit over the category of elements of the weight, and a weighted colimit an ordinary colimit over it Theorem
- Weighting by a representable evaluates the diagram Theorem
- Weighting by the constant singleton gives exactly the ordinary limit Theorem
Dependency tree · two levels
19 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, Definitions 7.1.1 and 7.2.1 (standard reference, not scraped)
- G. M. Kelly, Basic Concepts of Enriched Category Theory (TAC Reprints 10), (3.1)-(3.6) (standard reference, not scraped)