module Cat.Functor.Adjoint.Representable {o β} {C : Precategory o β} where
Adjoints in terms of representabilityπ
Building upon our characterisation of adjoints as Hom isomorphisms, we now investigate the relationship between adjoint functors and representable functors.
In this section, we show that for a functor to be a right adjoint is equivalent to the functor having a representing object for all .
The forward direction follows directly from the natural isomorphism , which exhibits as a representing object.
right-adjointβobjectwise-rep : β d β Corepresentation (Hom-from D d Fβ R) right-adjointβobjectwise-rep d .corep = L .Fβ d right-adjointβobjectwise-rep d .corepresents = adjunct-hom-iso-from Lβ£R d niβ»ΒΉ left-adjointβobjectwise-rep : β c β Corepresentation (Hom-into C c Fβ Functor.op L) left-adjointβobjectwise-rep c .corep = R .Fβ c left-adjointβobjectwise-rep c .corepresents = adjunct-hom-iso-into Lβ£R c βni pathβiso (sym (Hom-from-op _))
The other direction should be more surprising: if we only have a family of objects representing the functors , why should we expect them to assemble into a functor ?
We answer the question indirectly1: what is a sufficient
condition for
to have a left adjoint? Well, by our characterisation in terms of universal
morphisms, it should be enough to have initial objects for
each comma
category
.
But we have also established
that a (covariant)
functor into
is representable if and only if its category
of elements has an initial object.
Now we simply observe that the comma category and the category of elements of are exactly the same: both are made out of pairs of an object and a map , with the morphisms between them obtained in the obvious way from morphisms in .
module _ {o'} {D : Precategory o' β} {R : Functor C D} (corep : β d β Corepresentation (Hom-from D d Fβ R)) where private module D = Cat.Reasoning D
private ββ‘β« : β d β d β R β‘ β« C (Hom-from D d Fβ R)
The proof is by obnoxious data repackaging, so we hide it away.
ββ‘β« d = Precategory-path F F-is-precat-iso where open is-precat-iso F : Functor (d β R) (β« C (Hom-from D d Fβ R)) F .Fβ m = elem (m .βObj.y) (m .βObj.map) F .Fβ f = elem-hom (f .βHom.Ξ²) (sym (f .βHom.sq) β D.idr _) F .F-id = Element-hom-path _ _ refl F .F-β f g = Element-hom-path _ _ refl F-is-precat-iso : is-precat-iso F F-is-precat-iso .has-is-iso = is-isoβis-equiv is where is : is-iso (F .Fβ) is .is-iso.inv e = βobj (e .Element.section) is .is-iso.rinv e = refl is .is-iso.linv o = βObj-path _ _ refl refl refl F-is-precat-iso .has-is-ff = is-isoβis-equiv is where is : is-iso (F .Fβ) is .is-iso.inv h = βhom (D.idr _ β sym (h .Element-hom.commute)) is .is-iso.rinv h = Element-hom-path _ _ refl is .is-iso.linv h = βHom-path _ _ refl refl
objectwise-repβuniversal-maps : β d β Universal-morphism d R objectwise-repβuniversal-maps d = subst Initial (sym (ββ‘β« d)) (corepresentationβinitial-element (corep d)) objectwise-repβL : Functor D C objectwise-repβL = universal-mapsβL R objectwise-repβuniversal-maps objectwise-repβLβ£R : objectwise-repβL β£ R objectwise-repβLβ£R = universal-mapsβLβ£R R objectwise-repβuniversal-maps
Right adjoints into Sets are representableπ
For functors into , we can go one step further: under certain conditions, being a right adjoint is equivalent to being representable.
Indeed, if has a left adjoint , then is automatically represented by , the image of the singleton set by , because we have .
open Terminal (Sets-terminal {β}) right-adjointβcorepresentable : Corepresentation R right-adjointβcorepresentable .corep = L .Fβ top right-adjointβcorepresentable .corepresents = isoβisoβΏ (Ξ» _ β equivβiso (Ξ -β€-eqv eβ»ΒΉ)) (Ξ» _ β refl) βni adjunct-hom-iso-from Lβ£R top niβ»ΒΉ
Going the other way, if we assume that is copowered over (in other words, that it admits -small indexed coproducts), then any functor with representing object has a left adjoint given by taking copowers of : for any set , we have .
module _ (copowered : has-indexed-coproducts C β) {R : Functor C (Sets β)} (R-corep : Corepresentation R) where
private open Copowers (Ξ» _ β copowered) Hom[X,R-]-rep : β X β Corepresentation (Hom-from (Sets β) X Fβ R) Hom[X,R-]-rep X .corep = X β R-corep .corep Hom[X,R-]-rep X .corepresents = Fβ-iso-r (R-corep .corepresents) βni copower-hom-iso niβ»ΒΉ corepresentableβL : Functor (Sets β) C corepresentableβL = objectwise-repβL Hom[X,R-]-rep corepresentableβLβ£R : corepresentableβL β£ R corepresentableβLβ£R = objectwise-repβLβ£R Hom[X,R-]-rep