Alphabeta MathHow 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.
Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties
Definition
Let be a diagram. A limit of is a terminal object of (Constant diagrams, cones, cocones, and their morphisms, Initial object, terminal object, and zero object). It is written
Explicitly, for every cone there exists a unique morphism such that for every . The diagram has a limit when such a cone exists. A colimit of is an initial object of , written
Explicitly, for every cocone there exists a unique morphism such that for every . The diagram has a colimit when such a cocone exists.
Depends on
Used by
- Equalizers and coequalizers as limits and colimits of a parallel pair Definition
- Filtered categories and filtered colimits Definition
- Finite, small, and large limits and colimits; complete and cocomplete categories Definition
- Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors Definition
- Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations Definition
- Pullbacks and pushouts as limits and colimits of cospans and spans Definition
- The colimit of an increasing chain of sets is its union Example
- The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic Lemma
- A limiting cone for a diagram is exactly a colimiting cocone for the formally dual diagram in the opposite category Proposition
- Limits of empty diagrams are terminal objects, and colimits of empty diagrams are initial objects Proposition
- Any two limits, or any two colimits, of one diagram are uniquely isomorphic compatibly with their structure maps Theorem
- Assuming Choice, precomposition with a final functor does not change colimits, and precomposition with an initial functor does not change limits Theorem
- Chosen limits and colimits of a fixed small shape assemble into limit and colimit functors Theorem
- Every covariantly representable functor to Set preserves all existing small limits Theorem
- Every small limit can be constructed as an equalizer between products over the objects and arrows of the index category Theorem
- For small source and index categories, chosen target limits and colimits compute the corresponding functor-category limits and colimits pointwise Theorem
- Iterated small limits commute: either order is canonically isomorphic to the limit over the product 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: 10 results over 6 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.1.6 and 3.1.11 (standard reference, not scraped)