module Cat.Functor.Adjoint.Hom where module _ {o β o' β'} {C : Precategory o β} {D : Precategory o' β'} {L : Functor D C} {R : Functor C D} where
Adjoints as hom-isomorphismsπ
Recall from the page on adjoint functors that an adjoint pair induces an isomorphism
of -sets, sending each morphism to its left and right adjuncts, respectively. What that page does not mention is that any functors with such a correspondence β as long as the isomorphism is natural β actually generates an adjunction , with the unit and counit given by the adjuncts of each identity morphism.
More precisely, the data we require is an equivalence (of sets) such that the equation
holds. While this may seem un-motivated, itβs really a naturality square for a transformation between the bifunctors and whose data has been βunfoldedβ into elementary terms.
hom-iso-natural : (β {x y} β C.Hom (L.β x) y β D.Hom x (R.β y)) β Type _ hom-iso-natural f = β {a b c d} (g : C.Hom a b) (h : D.Hom c d) x β f (g C.β x C.β L.β h) β‘ R.β g D.β f x D.β h hom-isoβadjoints : (f : β {x y} β C.Hom (L.β x) y β D.Hom x (R.β y)) β (eqv : β {x y} β is-equiv (f {x} {y})) β hom-iso-natural f β L β£ R hom-isoβadjoints f f-equiv natural = adj' where fβ»ΒΉ : β {x y} β D.Hom x (R.β y) β C.Hom (L.β x) y fβ»ΒΉ = equivβinverse f-equiv inv-natural : β {a b c d} (g : C.Hom a b) (h : D.Hom c d) x β fβ»ΒΉ (R.β g D.β x D.β h) β‘ g C.β fβ»ΒΉ x C.β L.β h inv-natural g h x = ap fst $ is-contrβis-prop (f-equiv .is-eqv _) (fβ»ΒΉ (R.β g D.β x D.β h) , refl) ( g C.β fβ»ΒΉ x C.β L.β h , natural _ _ _ β sym (equivβcounit f-equiv _) β ap (f β fβ»ΒΉ) (D.extendl (ap (R.β g D.β_) (equivβcounit f-equiv _))))
We do not require an explicit naturality witness for the inverse of , since if a natural transformation is componentwise invertible, then its inverse is natural as well. It remains to use our βbinaturalityβ to compute that and do indeed give a system of adjunction units and co-units.
adj' : L β£ R adj' .unit .Ξ· x = f C.id adj' .unit .is-natural x y h = f C.id D.β h β‘β¨ D.introl R.F-id β©β‘ R.β C.id D.β f C.id D.β h β‘Λβ¨ natural _ _ _ β©β‘Λ f (C.id C.β C.id C.β L.β h) β‘β¨ ap f (C.cancell (C.idl _) β C.intror (C.idl _ β L.F-id)) β©β‘ f (L.β h C.β C.id C.β L.β D.id) β‘β¨ natural _ _ C.id β©β‘ R.β (L.β h) D.β f C.id D.β D.id β‘β¨ D.reflβ©ββ¨ D.idr _ β©β‘ R.β (L.β h) D.β f C.id β adj' .counit .Ξ· x = fβ»ΒΉ D.id adj' .counit .is-natural x y f = fβ»ΒΉ D.id C.β L.β (R.β f) β‘β¨ C.introl refl β©β‘ C.id C.β fβ»ΒΉ D.id C.β L.β (R.β f) β‘Λβ¨ inv-natural _ _ _ β©β‘Λ fβ»ΒΉ (R.β C.id D.β D.id D.β R.β f) β‘β¨ ap fβ»ΒΉ (D.cancell (D.idr _ β R.F-id) β D.intror (D.idl _)) β©β‘ fβ»ΒΉ (R.β f D.β D.id D.β D.id) β‘β¨ inv-natural _ _ _ β©β‘ f C.β fβ»ΒΉ D.id C.β L.β D.id β‘β¨ C.reflβ©ββ¨ C.elimr L.F-id β©β‘ f C.β fβ»ΒΉ D.id β adj' .zig = fβ»ΒΉ D.id C.β L.β (f C.id) β‘β¨ C.introl refl β©β‘ C.id C.β fβ»ΒΉ D.id C.β L.β (f C.id) β‘Λβ¨ inv-natural _ _ _ β©β‘Λ fβ»ΒΉ (R.β C.id D.β D.id D.β f C.id) β‘β¨ ap fβ»ΒΉ (D.cancell (D.idr _ β R.F-id)) β©β‘ fβ»ΒΉ (f C.id) β‘β¨ equivβunit f-equiv _ β©β‘ C.id β adj' .zag = R.β (fβ»ΒΉ D.id) D.β f C.id β‘β¨ D.reflβ©ββ¨ D.intror refl β©β‘ R.β (fβ»ΒΉ D.id) D.β f C.id D.β D.id β‘Λβ¨ natural _ _ _ β©β‘Λ f (fβ»ΒΉ D.id C.β C.id C.β L.β D.id) β‘β¨ ap f (C.elimr (C.idl _ β L.F-id)) β©β‘ f (fβ»ΒΉ D.id) β‘β¨ equivβcounit f-equiv _ β©β‘ D.id β
hom-iso-inv-natural : (f : β {x y} β D.Hom x (R.β y) β C.Hom (L.β x) y) β Type _ hom-iso-inv-natural f = β {a b c d} (g : C.Hom a b) (h : D.Hom c d) x β f (R.β g D.β x D.β h) β‘ g C.β f x C.β L.β h hom-iso-invβadjoints : (f : β {x y} β D.Hom x (R.β y) β C.Hom (L.β x) y) β (eqv : β {x y} β is-equiv (f {x} {y})) β hom-iso-inv-natural f β L β£ R hom-iso-invβadjoints f f-equiv natural = hom-isoβadjoints f.from (f.inverse .snd) nat where module f {x} {y} = Equiv (_ , f-equiv {x} {y}) abstract nat : hom-iso-natural f.from nat g h x = f.injective (f.Ξ΅ _ β sym (natural _ _ _ β ap (g C.β_) (ap (C._β L.β h) (f.Ξ΅ _)))) module _ {o β o'} {C : Precategory o β} {D : Precategory o' β} {L : Functor D C} {R : Functor C D} where private module C = Cat C module D = Cat D module L = Func L module R = Func R hom-natural-isoβadjoints : (Hom[-,-] C Fβ (Functor.op L FΓ Id)) β βΏ (Hom[-,-] D Fβ (Id FΓ R)) β L β£ R hom-natural-isoβadjoints eta = hom-isoβadjoints (to .Ξ· _) (natural-iso-to-is-equiv eta (_ , _)) Ξ» g h x β happly (to .is-natural _ _ (h , g)) x where open IsoβΏ eta open _=>_ module _ {o β o'} {C : Precategory o β} {D : Precategory o' β} {L : Functor D C} {R : Functor C D} (adj : L β£ R) where private module C = Cat C module D = Cat D module L = Func L module R = Func R hom-equiv : β {a b} β C.Hom (L.β a) b β D.Hom a (R.β b) hom-equiv = _ , L-adjunct-is-equiv adj adjunct-hom-iso-from : β a β Hom-from C (L.β a) β βΏ Hom-from D a Fβ R adjunct-hom-iso-from a = isoβisoβΏ (Ξ» _ β equivβiso hom-equiv) Ξ» f β funext Ξ» g β sym (L-adjunct-naturalr adj _ _) adjunct-hom-iso-into : β b β Hom-into C b Fβ Functor.op L β βΏ Hom-into D (R.β b) adjunct-hom-iso-into b = isoβisoβΏ (Ξ» _ β equivβiso hom-equiv) Ξ» f β funext Ξ» g β sym (L-adjunct-naturall adj _ _) adjunct-hom-iso : Hom[-,-] C Fβ (Functor.op L FΓ Id) β βΏ Hom[-,-] D Fβ (Id FΓ R) adjunct-hom-iso = isoβisoβΏ (Ξ» _ β equivβiso hom-equiv) Ξ» (f , h) β funext Ξ» g β sym (L-adjunct-naturalβ adj _ _ _)