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 · next 3 levels
Direct dependencies and their dependencies through the next three levels: 67 results over 20 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, Definition 3.7.2 (standard reference, not scraped)