Homotopy Type Theory
left adjoint > history (Rev #6, changes)
Showing changes from revision #5 to #6:
Added | Removed | Changed
Idea
< left adjoint
Many naturally arising functors in mathematics have adjoints. This makes them a useful thing to study.
Definition
A functor F : A → B F: A \to B is a left adjoint if there exists
A functor G : B → A G : B \to A
A natural transformation η : 1 A → G F \eta:1_A \to G F (the unit ).
A natural transformation ϵ G → 1 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
Properties
Lemma 9.3.2
If A A s a category and B B is a precategory then the type “F F 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 γ : G → G ′ \gamma: G \to G' to be ( G ′ ϵ ) ( η G ′ ) (G' \epsilon )(\eta G') . Then
δ γ = ( G ϵ ′ ) ( η G ′ ) ( G ′ ϵ ) ( η ′ G ) = ( G ϵ ′ ) ( G F G ′ ϵ ) ) η G ′ F G ) ( η ′ G ) = ( G ϵ ′ ) ( G ϵ ′ F G ) ( G F η ′ 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 G ≅ G ′ G \cong G' . By Theorem 9.2.5 (see functor precategory ), we have an identity G = G ′ 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,
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 ′ ϵ F ) ( η ′ G F ) η = ( G ′ ϵ F ) ( G ′ F η ) η ′ = η ′ (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
Revision on June 7, 2022 at 16:09:52 by
Anonymous? .
See the history of this page for a list of all contributions to it.