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β†’DR : \mathcal{C} \to \mathcal{D} to be a right adjoint is equivalent to the functor HomD(d,Rβˆ’):Cβ†’Sets\mathbf{Hom}_\mathcal{D}(d, R-) : \mathcal{C} \to \mathbf{Sets} having a representing object for all d:Dd : \mathcal{D}.

The forward direction follows directly from the natural isomorphism HomC(Ld,βˆ’)β‰…HomD(d,Rβˆ’)\mathbf{Hom}_\mathcal{C}(Ld, -) \cong \mathbf{Hom}_\mathcal{D}(d, R-), which exhibits LdLd as a representing object.

    : βˆ€ 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⁻¹

    : βˆ€ 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 LdLd representing the functors HomD(d,Rβˆ’)\mathbf{Hom}_\mathcal{D}(d, R-), why should we expect them to assemble into a functor L:Dβ†’CL : \mathcal{D} \to \mathcal{C}?

We answer the question indirectly1: what is a sufficient condition for RR 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 d↙Rd \swarrow R. But we have also established that a (covariant) functor into Sets\mathbf{Sets} is representable if and only if its category of elements has an initial object.

Now we simply observe that the comma category d↙Rd \swarrow R and the category of elements of HomD(d,Rβˆ’)\mathbf{Hom}_\mathcal{D}(d, R-) are exactly the same: both are made out of pairs of an object c:Cc : \mathcal{C} and a map dβ†’Rcd \to Rc, with the morphisms between them obtained in the obvious way from morphisms in C\mathcal{C}.

    β†™β‰‘βˆ« : βˆ€ 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 .↓
      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 Setsβ„“\mathbf{Sets}_\ell, we can go one step further: under certain conditions, being a right adjoint is equivalent to being representable.

Indeed, if RR has a left adjoint L:Setsβ„“β†’CL : \mathbf{Sets}_\ell \to \mathcal{C}, then RR is automatically represented by L{βˆ—}L\{*\}, the image of the singleton set by LL, because we have HomC(L{βˆ—},c)β‰…({βˆ—}β†’Rc)β‰…Rc\mathbf{Hom}_\mathcal{C}(L\{*\}, c) \cong (\{*\} \to Rc) \cong Rc.

  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 C\mathcal{C} is copowered over Setsβ„“\mathbf{Sets}_\ell (in other words, that it admits β„“\ell-small indexed coproducts), then any functor RR with representing object cc has a left adjoint given by taking copowers of cc: for any set XX, we have HomC(XβŠ—c,βˆ’)β‰…(Xβ†’HomC(c,βˆ’))β‰…(Xβ†’Rβˆ’)\mathbf{Hom}_\mathcal{C}(X \otimes c, -) \cong (X \to \mathbf{Hom}_\mathcal{C}(c, -)) \cong (X \to R-).

    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

  1. for a more direct construction based on the Yoneda embedding, see the nLabβ†©οΈŽ