Homotopy Type Theory
left adjoint (Rev #1)


Many naturally arising functors in mathematics have adjoints. This makes them a useful thing to study.


A functor F:ABF: A \to B is a left adjoint if there exists

  • A functor G:BAG : B \to A
  • A natural transformation η:1 AGF\eta:1_A \to G F (the unit).
  • A natural transformation ϵG1 B\epsilon G \to 1_B (the counit).
  • Which satisfy the triangle identities (a.k.a zig-zag identities)
    • (ϵF)(Fη)=1 F(\epsilon F)(F \eta) = 1_F
    • (Gϵ)(ηG)=1 G(G \epsilon)(\eta G) = 1_G


Lemma 9.3.2

If AA s a category and BB is a precategory then the type “FF is a left adjoint” is a mere proposition?.

Proof. Suppose we are given (G,η,ϵ)(G, \eta, \epsilon) with the triangle identities and also (G,η,ϵ)(G', \eta', \epsilon'). Define γ:GG\gamma: G \to G' to be (Gϵ)(ηG)(G' \epsilon )(\eta G'). Then

δγ =(Gϵ)(ηG)(Gϵ)(ηG) =(Gϵ)(GFGϵ ))ηGFG)(ηG) =(Gϵ)(GϵFG)(GFηG)(ηG) =(Gϵ)(ηG) =1 G \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 γδ=1 G\gamma \delta=1_{G'}, so γ\gamma is a natural isomorphism GGG \cong G'. By Theorem 9.2.5 (see functor precategory), we have an identity G=GG=G'.

See also

functor natural transformation


HoTT Book

Revision on September 5, 2018 at 17:26:30 by Ali Caglayan. See the history of this page for a list of all contributions to it.