For precategories , there is a precategory , called the functor precategory, defined by
Proof. We define . Naturality follows by the unit axioms of a precategory. For and , we define . Naturality follows by associativity. Similarly, the unit and associativity laws for follow from those for .
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 precategory and is a category, then is a category.
Category theory functor category Rezk completion
Revision on September 5, 2018 at 12:25:11 by Ali Caglayan. See the history of this page for a list of all contributions to it.