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.
Small, locally small, and large categories
Definition
Let be a category (Category, object, morphism, domain, codomain, identity, composition, and hom-collection) under the class convention of Category, object, morphism, domain, codomain, identity, composition, and hom-collection.
- is small when both and are sets.
- is locally small when every is a set.
- is large when it is not small.
A small category is locally small because each hom-collection is a subclass of the set of all morphisms. A large category may or may not be locally small.
Remarks
Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why is not formed gives contextual discussion of the convention used here.