The left part of a pair of adjoint functors is one of two best approximations to a weak inverse of the other functor of the pair. (The other best approximation is the functorβs right adjoint, if it exists.) Note that a weak inverse itself, if it exists, must be a left adjoint, forming an adjoint equivalence.
A left adjoint to a forgetful functor is called a free functor. Many left adjoints can be constructed as quotients of free functors.
The concept generalises immediately to enriched categories and in 2-categories.
Given categories and and a functor , a left adjoint of is a functor together with natural transformations and such that the following diagrams (known as the triangle identities) commute, where denotes whiskering of a functor with a natural transformation.
Definition is equivalent to requiring that there is a natural isomorphism between the Hom functors
Depending upon oneβs interpretation of , the category of sets, one may strictly speaking need to restrict to locally small categories for this equivalence to parse.
The equivalent formulation of Definition given in Remark generalises immediately to the setting of enriched categories.
Given -enriched categories and and a -enriched functor , a left adjoint of is a -enriched functor together with a -enriched natural isomorphism between the Hom functors
Definition generalises immediately from CAT, the 2-category of (large) categories, to any 2-category.
Let be a 2-category. Given objects and and a 1-arrow of , a left adjoint of is a 1-arrow together with 2-arrows and such that the following diagrams commute, where denotes whiskering in .
If one assumes that oneβs ambient 2-category has more structure, bringing it closer to being a 2-topos, for example a Yoneda structure, one should be able to give an equivalent formulation of Definition akin to that of Remark .
Restricted to preorders or posets, Definition in its equivalent formulation of Remark can be expressed in the following terminology.
Given posets or preorders and and a monotone function , a left adjoint of is a monotone function such that, for all in and in , we have that holds if and only if holds.
left adjoints preserve epimorphisms.
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.
(Lemma 9.3.2 in the HoTT book)
If is an univalent category and is a category then the type β is a left adjointβ is a mere proposition.
Suppose we are given with the triangle identities and also . Define to be . Then
using Lemma 9.2.8 (see natural transformation) and the triangle identities. Similarly, we show , so is a natural isomorphism . By Theorem 9.2.5 (see functor category), we have an identity .
Now we need to know that when and are transported? along this identity, they become equal to and . By Lemma 9.1.9,
Lemma 9.1.9 needs to be included. For now as transports are not yet written up I didnβt bother including a reference to the page category. -Ali
this transport is given by composing with or as appropriate. For , this yields
using Lemma 9.2.8 (see natural transformation) and the traingle identity. The case of is similar. FInally, the triangle identities transport correctly automatically, since hom-sets are sets.
Last revised on June 9, 2022 at 08:21:49. See the history of this page for a list of all contributions to it.