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.
Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why is not formed
The word class in this development is an abbreviation for a formula in the language of set theory, as described by The first-order language of set theory: , , formulas with parameters, and class abbreviations. It is not an additional set. A category may therefore have a definable class of objects and a definable class of morphisms. Quantification over such a category is a schema: each use expands to an ordinary formula of ZFC.
A category is small when its objects and morphisms form sets, and locally small when each hom-collection is a set. The category used below has small categories as objects; its hom-categories are sets or locally small categories as asserted in the relevant result. We do not form a category of all large categories. Doing so as though all classes were members of a larger set would conflict with the same size obstruction exhibited for the ordinals by Burali-Forti: there is no set of all ordinals. Class recursion, when used, is only the definable schema licensed by Transfinite recursion.
Depends on
Used by
- A complete locally small category with no small coseparating set Counterexample
- A locally small category that is not well-powered: one object admits no set of representative monomorphisms Counterexample
- Category, object, morphism, domain, codomain, identity, composition, and hom-collection Definition
- Functor category [C,D] Definition
- Multiplicative system in a category Definition
- Small, locally small, and large categories Definition
- Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms Definition
- Well-powered and co-well-powered categories, and supplied well-powerings Definition
- Every category is locally small False statement
- FALSE: A continuous functor on a complete category necessarily has a left adjoint False statement
- A functor is an isomorphism of categories exactly when its object and morphism maps are bijective Proposition
- Why completeness alone cannot replace a solution set or the SAFT smallness hypotheses Remark
- Small categories, functors, and natural transformations form the strict 2-category Cat Theorem
- Subobjects and quotient objects form oppositely oriented partially ordered collections Theorem
Dependency tree · two levels
9 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
- Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)