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.
Finite, small, and large limits and colimits; complete and cocomplete categories
Definition
A diagram is finite when its indexing category has finitely many morphisms, small when its indexing category is small, and large otherwise (Assuming Choice, cardinality of a small category and κ-small diagrams, Small, locally small, and large categories).
A category has finite limits, small limits, or a specified class of limits when every diagram of the corresponding class has a limit in the sense of Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties. It is complete when it has all small limits. The dual terms are finite colimits, small colimits, and cocomplete. Completeness and cocompleteness do not assert the existence of limits or colimits of large diagrams.
Depends on
Used by
- A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers Corollary
- Assuming Choice, every small complete category and every small cocomplete category is a preorder Corollary
- If A is small, then [A,C] is complete or cocomplete whenever C is respectively complete or cocomplete Corollary
- Filtered categories and filtered colimits Definition
- Under the definable-class diagram convention, the empty set is the product of the large family of all sets Example
- FALSE: every category has all small limits False statement
- A cone over an identity diagram is weakly initial, and the identity diagram has a limit exactly when the category has an initial object Lemma
- Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category Theorem
- Set has all small colimits, realized as a quotient of a set-indexed disjoint union Theorem
- Set has all small limits, realized as compatible tuples in a set-indexed product Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 35 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- E. Riehl, Category Theory in Context, Definitions 3.2.1 and 3.2.3 (standard reference, not scraped)