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.
Assuming Choice, cardinality of a small category and κ-small diagrams
Definition
Assume the Axiom of Choice (The Axiom of Choice), so every set has a cardinality (A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used, Cardinal sum , product and exponentiation , and why they are written apart from the ordinal operations). For a small category (Small, locally small, and large categories), define
Every object contributes an identity morphism, so this convention also bounds the number of objects. The cardinality of a small diagram (Diagram as a functor from an indexing category) is . For a cardinal , the diagram is -small when .
Depends on
- Small, locally small, and large categories
- A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used
- Cardinal sum $\kappa \oplus \lambda$, product $\kappa \otimes \lambda$ and exponentiation $\kappa^{\lambda}$, and why they are written apart from the ordinal operations
- The Axiom of Choice
- Diagram as a functor from an indexing category
Used by
- Finite, small, and large limits and colimits; complete and cocomplete categories Definition
- Assuming Choice, a small category with products or coproducts indexed by the cardinality of its morphism set is a preorder Theorem
- Chosen limits and colimits of a fixed small shape assemble into limit and colimit functors Theorem
- Iterated small limits commute: either order is canonically isomorphic to the limit over the product category Theorem
Dependency tree · two levels
25 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, Category Theory in Context, Definition 3.7.2 (standard reference, not scraped)