## Idea ## Many naturally arising functors in mathematics have adjoints. This makes them a useful thing to study. ## Definition ## A [[functor]] $F: A \to B$ is a **left adjoint** if there exists * A [[functor]] $G : B \to A$ * A [[natural transformation]] $\eta:1_A \to G F$ (the **unit**). * A [[natural transformation]] $\epsilon G \to 1_B$ (the **counit**). * Which satisfy the **triangle identities** (a.k.a zig-zag identities) * $(\epsilon F)(F \eta) = 1_F$ * $(G \epsilon)(\eta G) = 1_G$ ## Properties ## ### Lemma 9.3.2 ### If $A$ s a [[category]] and $B$ is a [[precategory]] then the type "$F$ is a left adjoint" is a [[mere proposition]]. **Proof.** Suppose we are given $(G, \eta, \epsilon)$ with the triangle identities and also $(G', \eta', \epsilon')$. Define $\gamma: G \to G'$ to be $(G' \epsilon )(\eta G')$. Then $$ \begin{aligned} \delta \gamma &= (G \epsilon')(\eta G')(G' \epsilon) (\eta' G)\\ &= (G \epsilon')(G F G' \epsilon_))\eta G' F G)(\eta' G)\\ &= (G \epsilon ')(G \epsilon' F G)(G F \eta' G)(\eta G)\\ &= (G \epsilon)(\eta G)\\ &= 1_G \end{aligned} $$ using Lemma 9.2.8 (see [[natural transformation]]) and the triangle identities. Similarly, we show $\gamma \delta=1_{G'}$, so $\gamma$ is a [[natural isomorphism]] $G \cong G'$. By Theorem 9.2.5 (see [[functor precategory]]), we have an [[identity]] $G=G'$. Now we need to know that when $\eta$ and $\epsilon$ are [transported]] along this [[identity]], they become equal to $\eta'$ and $\epsilon '$. By Lemma 9.1.9, +--{.query} 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 $\gamma$ or $\delta$ as appropriate. For $\eta$, this yields $$(G' \epsilon F)(\eta' G F)\eta = (G' \epsilon F)(G' F \eta)\eta'=\eta'$$ using Lemma 9.2.8 (see [[natural transformation]]) and the traingle identity. The case of $\epsilon$ is similar. FInally, the triangle identities transport correctly automatically, since hom-sets are sets. $\square$ ## See also ## [[Category theory]] [[functor]] [[natural transformation]] ## References ## [[HoTT Book]]