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.
Functor category
Definition
Within the definable-class convention of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why is not formed, the construction below is formed when the source category is small. Then a functor out of and a natural transformation between two such functors are set-coded data, so they can be objects and morphisms of a category in ZFC.
For categories , the functor category has functors as objects and natural transformations as morphisms (Natural transformation and its components). Its identities and composition are the identity transformations and vertical composition. These are the operations of Identity natural transformation and vertical composition.
Closure under composition is Vertical composites of natural transformations satisfy naturality. Associativity and the identity laws hold at each component because they hold in . Further smallness and local-smallness properties of this category are stated separately.
For an arbitrary large source , the same notation may be used only as metatheoretic shorthand for functors and natural transformations; this definition does not form those proper-class-sized data into a category.
Depends on
Used by
- The end of the hom-bifunctor is the commutative monoid of natural endomorphisms of the identity functor Corollary
- Global Kan extensions as adjoints to restriction Definition
- Natural isomorphism Definition
- Set-weighted limits and colimits Definition
- The arrow category of an abelian category Definition
- The Yoneda assignment and the small-source Yoneda functor, traditionally called the Yoneda embedding Definition
- Quivers and quiver homomorphisms form a functor category of set-valued diagrams Example
- The arrow category Set^→: functions as objects and commuting squares as morphisms Example
- FALSE: A monad is a monoid object in the endofunctor category for every category False statement
- A weighted limit of a set-valued diagram is the set of natural transformations from the weight Proposition
- Additive functors and natural transformations form a preadditive category Proposition
- An adjunction induces postcomposition and precomposition adjunctions on legitimate functor categories Proposition
- If C is small and D is locally small then [C,D] is locally small; if both are small it is small Proposition
- Local smallness does not make every natural-transformation collection a set, but the Yoneda construction proves sethood in the representable-source case Remark
- The Kleisli and Eilenberg–Moore universal properties are schematic Remark
- The monoid description of a monad requires an endofunctor category Remark
- The particular Yoneda end and the enriched functor category have different size requirements Remark
- Chosen limits and colimits are adjoint to the diagonal functor Theorem
- Chosen limits and colimits of a fixed small shape assemble into limit and colimit functors Theorem
- For a small source category, the set of natural transformations is an end of the hom-bifunctor of the values Theorem
- For small source and index categories, chosen target limits and colimits compute the corresponding functor-category limits and colimits pointwise Theorem
- Small categories, functors, and natural transformations form the strict 2-category Cat Theorem
- The category of small categories is cartesian closed Theorem
- The endofunctor category of a small category is strict monoidal under composition Theorem
- Whenever the endofunctor category exists, monads on a fixed category and their morphisms form a category Theorem
Dependency tree · two levels
8 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)