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.
Sets and functions form the large locally small category
Statement
Sets as objects and functions as morphisms form a large locally small category .
Facts & Assumptions
Given: Sets and functions , .
A category has associative composition and an identity at every object, and when it is presented by its hom-collections a morphism is the triple , so that and are the projections (Category, object, morphism, domain, codomain, identity, composition, and hom-collection); a function is a set of ordered pairs with a set domain and a uniquely determined value at each point of it, and does not itself determine a codomain (A function is a relation with and implying ; , the value , domain and codomain); the functions form the set (The set of all functions ).
Small, locally small, and large have the meanings in Small, locally small, and large categories, and the ordinals do not form a set (Burali-Forti: there is no set of all ordinals).
Proof
Identity functions are functions, composites of functions are functions, function composition is associative, and .
Hence sets and functions satisfy every axiom of a category.
For fixed , the hom-collection is , a set in bijection with the set from [L1]; the tagging is what gives each morphism a unique codomain, since the empty function alone would be a morphism into every set. The object class contains every ordinal and therefore is not a set, so is locally small and large.
Depends on
- Category, object, morphism, domain, codomain, identity, composition, and hom-collection
- Small, locally small, and large categories
- A function is a relation $f$ with $(a,b) \in f$ and $(a,c) \in f$ implying $b = c$; $f : A \to B$, the value $f(a)$, domain and codomain
- The set $B^{A}$ of all functions $A \to B$
- Burali-Forti: there is no set of all ordinals
Used by
- A componentwise family between functors need not be a natural transformation Counterexample
- A functor need not preserve monomorphisms Counterexample
- Actions of a group G on sets are functors BG toSet Example
- Pointed sets are equivalent to sets and partial functions but not isomorphic as categories Example
- Quivers and quiver homomorphisms form a functor category of set-valued diagrams Example
- Singletons define a natural transformation from the identity functor on sets to the covariant power-set functor Example
- The arrow category Set^→: functions as objects and commuting squares as morphisms Example
- The distributive and exponential laws of sets are natural isomorphisms Example
- The free-group functor F:Set toGrp and free-module functor R⁽⁻⁾:Set→ R-Mod Example
- Underlying-set and structure-forgetting functors among Grp, Ring, Vect_F, R-Mod, Top, and Set Example
- A natural transformation is determined by its component at one object False statement
- In Set, monomorphisms are exactly injections and epimorphisms are exactly surjections Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 33 results over 11 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, Chapter 1 (standard reference, not scraped)