module Cat.Functor.Adjoint.AFT where

# The adjoint functor theoremπ

The **adjoint functor theorem** states a sufficient
condition for a continuous functor
$F:CβD$
from a locally small, complete category to
have a left
adjoint.

In an ideal world, this would always be the case: we want to compute an initial object $Lx$ in the comma category $xβF,$ for each $x:D.$ Generalising from the case of partial orders, where a bottom element is the intersection of everything in the poset, we might try to find $Lx$ as the limit of the identity functor on $xβF.$ Furthermore, each of these comma categories are complete, by completeness of $C$ and continuity of $F,$ so this functor should have a limit!

Unfortunately, the only categories which can be shown to admit
arbitrary limits indexed by themselves are the preorders; The existence
of a large-complete *non*-preorder would contradict excluded
middle, which we neither assume nor reject. Therefore, weβre left with
the task of finding a condition on the functor
$F$
which ensures that we can compute the limit of
$Id:xβFβxβF$
using only small data. The result is a technical device called a
**solution set**.

module _ {o β o'} {C : Precategory o β} {D : Precategory o' β} (F : Functor C D) where open βObj private module C = Cat C module D = Cat D module F = Functor F

A solution set (for $F$ with respect to $Y:D)$ is a set $I,$ together with an $I-indexed$ family of objects $X_{i}$ and morphisms $m_{i}:YβF(X_{i}),$ which commute in the sense that, for every $X_{β²}$ and $h:YβX_{β²},$ there exists a $j:I$ and $t:X_{i}βX_{β²}$ which satisfy $h=F(t)m_{i}.$

record Solution-set (Y : β D β) : Type (o β lsuc β) where field {index} : Type β has-is-set : is-set index dom : index β β C β map : β i β D.Hom Y (F.β (dom i)) factor : β {X'} (h : D.Hom Y (F.β X')) β β[ i β index ] (Ξ£[ t β C.Hom (dom i) X' ] (h β‘ F.β t D.β map i))

Put another way, $F$ has a solution set with respect to $X$ if the comma category $XβF$ has a weakly initial family of objects, given by the $m_{i}$ and their domains, with the complicated factoring condition corresponding to weak initiality.

module _ {X} (S : Solution-set X) where solution-setβfamily : S .index β β X β F β solution-setβfamily i .x = tt solution-setβfamily i .y = S .dom i solution-setβfamily i .map = S .map i solution-setβfamily-is-weak-initial : is-weak-initial-fam (X β F) solution-setβfamily solution-setβfamily-is-weak-initial Y = do (i , t , p) β S .factor (Y .map) pure (i , βhom (D.elimr refl β p))

Then, we can put together the adjoint functor theorem, by showing that the sea has risen above it:

- Since
$C$
is small-complete and
$F$
is small-continuous, then each comma category
$xβF$
is small-complete, by
`limits in comma categories`

; - Each $xβF$ has a weakly initial family, and all small equalisers, so they all have initial objects;
- An initial object for $xβF$ is exactly a universal morphism into $F,$ and if $F$ admits all universal maps, then it has a left adjoint.

solution-setβleft-adjoint : is-complete β β C β is-continuous β β F β (β y β Solution-set y) β Ξ£[ G β Functor D C ] G β£ F solution-setβleft-adjoint c-compl F-cont ss = _ , universal-mapsβleft-adjoint init where module _ x where instance H-Level-ix : β {n} β H-Level (ss x .index) (2 + n) H-Level-ix = basic-instance 2 (ss x .has-is-set) init : Initial (x β F) init = is-complete-weak-initialβinitial (x β F) (solution-setβfamily (ss x)) (comma-is-complete F c-compl F-cont) (solution-setβfamily-is-weak-initial (ss x))