hom-set, hom-object, internal hom, exponential object, derived hom-space
loop space object, free loop space object, derived loop space
Given categories and , the functor category – written or – is the category whose
morphisms are natural transformations between these functors.
Discussion in homotopy type theory.
Note: the HoTT book calls a internal category in HoTT a “precategory” and a univalent category a “category”, but here we shall refer to the standard terminology of “category” and “univalent category” respectively.
For categories , there is a category , called the functor category, defined by
Proof. We define . Naturality follows by the unit axioms of a category. For and , we define . Naturality follows by associativity. Similarly, the unit and associativity laws for follow from those for .
We define a natural isomorphism to be an isomorphism in .
Functor categories serve as the hom-categories in the strict 2-category Cat.
In the context of enriched category theory the functor category is generalized to the enriched functor category.
In the absence of the axiom of choice (including many internal situations), the appropriate notion to use is often instead the anafunctor category.
If has limits or colimits of a certain shape, then so does and they are computed pointwise. (However, if is not complete, then other limits in can exist “by accident” without being pointwise.)
If is small and is cartesian closed and complete, then is cartesian closed. See at cartesian closed category for a proof.
Functor categories enjoy the following accessibility and local presentability properties, as explained by Zhen Lin Low at nForum.
-accessible functors from a -accessible category to any accessible category form an accessible category. (It is not so easy to say what the accessibility rank is here.)
-accessible functors from a -accessible category to any locally -presentable category form a locally -presentable category.
Cocontinuous functors between locally presentable categories form a locally presentable category. More precisely, if and are locally -presentable, then so is .
Continuous accessible functors between locally presentable categories form the opposite of a locally presentable category. More precisely, if and are locally -presentable, then so is .
Indeed, the point is this: given a -accessible category ( essentially small), the category of -accessible functors (for arbitrary ; here by “-accessible” we mean simply “preserves -filtered colimits”) is naturally equivalent to the category of all . It should be well known that:
If is accessible, then so is .
If is small and is locally -presentable, then also the functor category is locally presentable.
Colimit-preserving functors out of a locally -presentable category are -accessible.
A right adjoint between locally -presentable categories is -accessible if and only if its left adjoint is strongly -accessible (i.e. preserves -presentable objects as well as -filtered colimits); and every limit-preserving accessible functor between locally presentable categories is a right adjoint.
Statement 2 is Adámek & Rosický (1994), Cor. 1.54. Statement 3 is obvious, and statement 4 is a straightforward exercise.
In general, accessible functors between accessible categories do not form an accessible category due to size issues. The best one can hope for is a class-accessible category. Let be an accessible category that is not essentially small. Consider the category of all accessible functors . This is the same as the smallest full replete subcategory of containing all representable functors and closed under small colimits. In particular, is accessible if and only if locally presentable. We claim is not accessible.
Indeed, suppose has a small generating family, say . Then for some regular cardinal , every member of is -accessible. So consider for some object that is not -presentable. (Such an exists because is not essentially small.) Since generates, there is a small diagram of -accessible functors whose colimit is . But then is a retract of a -accessible functor and hence -accessible: a contradiction. That said, is a class-locally presentable category.
A natural transformation is an isomorphism in if and only if each is an isomorphism in .
Proof. If is an isomorphism, then we have that is its inverse. By definition of composition in , . Thus, and imply that and , so is an isomorphism.
Conversely, suppose each is an isomorphism, with inverse called . We define a natural transformation with components ; for the naturality axiom we have
Now since composition and identity of natural transformations is determined on their components, we have and
If is a category and is a univalent category, then is a univalent category.
Proof. Let ; we must show that is an equivalence.
To give an inverse to it, suppose is a natural isomorphism. Then for any , we have an isomorphism , hence an identity . By function extensionality, we have an identity .
Now since the last two axioms of a functor are mere propositions, to show that it will suffice to show that for any , the functions
become equal when transported? along . By computation for function extensionality, when applied to , becomes equal to .
This reference needs to be included. For now as transports are not yet written up I didn’t bother including a reference to the page univalent category. -Ali
But by [INCLUDE ME], transporting along and is equal to the composite , which by naturality of is equal to .
This completes the definition of a function . Now consider the composite
Since hom-sets are sets, their identity types are mere propositions, so to show that two identities are equal, it suffices to show that . But in the definition of , if were of the form , then would be equal to (this can easily be proved by induction on ). Thus, would be equal to , and so by function extensionality we would have , which is what we need.
Finally, consider the composite
Since identity of natural transformations can be tested componentwise, it suffices to show that for each we have . But as observed above, we have , while by computation for function extensionality. Since and are inverses, we have as desired.
If and are small, then is also small.
If is small and is locally small, then is still locally small.
Even if and are locally small, if is not small, then will usually not be locally small.
As a partial converse to the above, if and are locally small, then must be essentially small; see Freyd & Street (1995).
See most references at category theory, such as
Discussion of local presentability:
Last revised on May 20, 2023 at 08:53:41. See the history of this page for a list of all contributions to it.