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.

:  d  Corepresentation (Hom-from D d F∘ R)
right-adjoint→objectwise-rep d .corep = L .F₀ d

:  c  Corepresentation (Hom-into C c F∘ Functor.op L)
left-adjoint→objectwise-rep c .corep = R .F₀ 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 free objects, 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

private
↙≡∫ :  d  d  R   (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) ( (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 = ext refl
F .F-∘ f g = ext 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 = ext refl
is .is-iso.linv h = ↓Hom-path _ _ refl refl
objectwise-rep→universal-maps :  d  Universal-morphism R d
objectwise-rep→universal-maps d = subst Initial (sym (↙≡∫ d))
(corepresentation→initial-element (corep d))

objectwise-rep→functor : Functor D C
objectwise-rep→functor =
universal-maps→functor 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 .corep = L .F₀ top
iso→isoⁿ  _  equiv→iso (Π-⊤-eqv e⁻¹))  _  refl)

Going the other way, if we assume that is copowered over (in other words, that it admits indexed coproducts), then any functor with representing object has a left adjoint given by taking copowers of for any set we have

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→functor : Functor (Sets ) C
corepresentable→functor = objectwise-rep→functor Hom[X,R-]-rep