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 $R:C→D$ to be a right adjoint is equivalent to the functor $Hom_{D}(d,R−):C→Sets$ having a representing object for all $d:D.$

The forward direction follows directly from the natural isomorphism $Hom_{C}(Ld,−)≅Hom_{D}(d,R−),$ which exhibits $Ld$ 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 = path→iso (sym (Hom-from-op _)) ∘ni adjunct-hom-iso-into L⊣R c

The other direction should be more surprising: if we only have a
family of objects
$Ld$
representing the functors
$Hom_{D}(d,R−),$
why should we expect them to assemble into a *functor*
$L:D→C?$

We answer the question indirectly^{1}: what is a sufficient
condition for
$R$
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
$d↙R.$
But we have also `established`

that a (covariant)
functor into
$Sets$
is representable if and only if its category
of elements has an initial object.

Now we simply observe that the comma category $d↙R$ and the category of elements of $Hom_{D}(d,R−)$ are exactly the same: both are made out of pairs of an object $c:C$ and a map $d→Rc,$ with the morphisms between them obtained in the obvious way from morphisms in $C.$

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 ≡ ∫ (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 objectwise-rep→left-adjoint : objectwise-rep→functor ⊣ R objectwise-rep→left-adjoint = universal-maps→left-adjoint objectwise-rep→universal-maps

## Right adjoints into Sets are representable🔗

For functors into $Sets_{ℓ},$ we can go one step further: under certain conditions, being a right adjoint is equivalent to being representable.

Indeed, if $R$ has a left adjoint $L:Sets_{ℓ}→C,$ then $R$ is automatically represented by $L{∗},$ the image of the singleton set by $L,$ because we have $Hom_{C}(L{∗},c)≅({∗}→Rc)≅Rc.$

open Terminal (Sets-terminal {ℓ}) right-adjoint→corepresentable : Corepresentation R right-adjoint→corepresentable .corep = L .F₀ top right-adjoint→corepresentable .corepresents = adjunct-hom-iso-from L⊣R top ni⁻¹ ∘ni iso→isoⁿ (λ _ → equiv→iso (Π-⊤-eqv e⁻¹)) (λ _ → refl)

Going the other way, if we assume that $C$ is copowered over $Sets_{ℓ}$ (in other words, that it admits $ℓ-small$ indexed coproducts), then any functor $R$ with representing object $c$ has a left adjoint given by taking copowers of $c:$ for any set $X,$ we have $Hom_{C}(X⊗c,−)≅(X→Hom_{C}(c,−))≅(X→R−).$

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 = copower-hom-iso ni⁻¹ ∘ni F∘-iso-r (R-corep .corepresents) corepresentable→functor : Functor (Sets ℓ) C corepresentable→functor = objectwise-rep→functor Hom[X,R-]-rep corepresentable→left-adjoint : corepresentable→functor ⊣ R corepresentable→left-adjoint = objectwise-rep→left-adjoint Hom[X,R-]-rep