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

The forward direction follows directly from the natural isomorphism $\mathbf{Hom}_\mathcal{C}(Ld, -) \cong \mathbf{Hom}_\mathcal{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 =
    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 $Ld$ representing the functors $\mathbf{Hom}_\mathcal{D}(d, R-)$, why should we expect them to assemble into a functor $L : \mathcal{D} \to \mathcal{C}$?

We answer the question indirectly¹: what is a sufficient condition for $R$ 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 \swarrow R$. But we have also established that a (covariant) functor into $\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 \swarrow R$ and the category of elements of $\mathbf{Hom}_\mathcal{D}(d, R-)$ are exactly the same: both are made out of pairs of an object $c : \mathcal{C}$ and a map $d \to Rc$, with the morphisms between them obtained in the obvious way from morphisms in $\mathcal{C}$.

  private
    ↙≡∫ : ∀ d → d ↙ R ≡ ∫ C (Hom-from D d F∘ R)

    ↙≡∫ 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 $\mathbf{Sets}_\ell$, 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 : \mathbf{Sets}_\ell \to \mathcal{C}$, then $R$ is automatically represented by $L\{*\}$, the image of the singleton set by $L$, because we have $\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 $\mathcal{C}$ is copowered over $\mathbf{Sets}_\ell$ (in other words, that it admits $\ell$-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 $\mathbf{Hom}_\mathcal{C}(X \otimes c, -) \cong (X \to \mathbf{Hom}_\mathcal{C}(c, -)) \cong (X \to R-)$.

  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