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 functors 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 β
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 : natural-iso (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 natural-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 adjunct-hom-iso-from : β a β natural-iso (Hom-from C (L.β a)) (Hom-from D a Fβ R) adjunct-hom-iso-from a = to-natural-iso mi where open make-natural-iso mi : make-natural-iso (Hom-from C (L.β a)) (Hom-from D a Fβ R) mi .eta x = L-adjunct adj mi .inv x = R-adjunct adj mi .etaβinv _ = funext Ξ» _ β L-R-adjunct adj _ mi .invβeta _ = funext Ξ» _ β R-L-adjunct adj _ mi .natural _ _ f = funext Ξ» g β sym (L-adjunct-naturalr adj f g) adjunct-hom-iso-into : β b β natural-iso (Hom-into C b Fβ Functor.op L) (Hom-into D (R.β b)) adjunct-hom-iso-into b = to-natural-iso mi where open make-natural-iso mi : make-natural-iso (Hom-into C b Fβ Functor.op L) (Hom-into D (R.β b)) mi .eta x = L-adjunct adj mi .inv x = R-adjunct adj mi .etaβinv _ = funext Ξ» _ β L-R-adjunct adj _ mi .invβeta _ = funext Ξ» _ β R-L-adjunct adj _ mi .natural _ _ f = funext Ξ» g β sym $ L-adjunct-naturall adj g f adjunct-hom-iso : natural-iso (Hom[-,-] C Fβ (Functor.op L FΓ Id)) (Hom[-,-] D Fβ (Id FΓ R)) adjunct-hom-iso = to-natural-iso mi where open make-natural-iso mi : make-natural-iso (Hom[-,-] C Fβ (Functor.op L FΓ Id)) (Hom[-,-] D Fβ (Id FΓ R)) mi .eta x = L-adjunct adj mi .inv x = R-adjunct adj mi .etaβinv _ = funext Ξ» _ β L-R-adjunct adj _ mi .invβeta _ = funext Ξ» _ β R-L-adjunct adj _ mi .natural _ _ (f , h) = funext Ξ» g β sym $ L-adjunct-naturalβ adj h f g