open import Cat.Instances.Elements.Covariant
open import Cat.Diagram.Coproduct.Copower
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Functor.Hom.Representable
open import Cat.Functor.Equivalence.Path
open import Cat.Instances.Sets.Complete
open import Cat.Functor.Equivalence
open import Cat.Functor.Hom.Duality
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial
open import Cat.Instances.Comma
open import Cat.Instances.Sets
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Reasoning

open Corepresentation
open Representation
open Functor

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.

module _ {o'} {D : Precategory o' β}
{L : Functor D C} {R : Functor C D} (Lβ£R : L β£ R)
where

  right-adjointβobjectwise-rep
: β 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 $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 indirectly1: 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}$.

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 $\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$.

module _
{R : Functor C (Sets β)} {L : Functor (Sets β) C} (Lβ£R : L β£ R)
where

  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 $\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-)$.

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


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