How 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.
Every category is locally small
Statement
FALSE. Every category is locally small.
Facts & Assumptions
Given: The definable class of all ordinals, interpreted under the category-size convention in Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why is not formed.
A category is locally small exactly when every hom-collection is a set (Small, locally small, and large categories).
Ordinals are linearly ordered by membership, so any two have a maximum (Ordinal (von Neumann), Trichotomy and well-ordering of the ordinals).
There is no set of all ordinals (Burali-Forti: there is no set of all ordinals).
Refutation
Define a one-object category with object and . Take as the identity and define .
Maximum is associative, and for every ordinal . Thus the data in step 1.1 satisfy the category axioms under the given convention.
Its sole hom-collection is , which is not a set by [L3]. Hence is not locally small by [L1].
The category of step 2.1 refutes the assertion that every category is locally small.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 26 results over 14 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
- Emily Riehl, Category Theory in Context, sections 1.1 and 1.2 (standard reference, not scraped)