open import Cat.Instances.Comma.Limits
open import Cat.Diagram.Initial.Weak
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
open import Cat.Instances.Comma
open import Cat.Prelude

import Cat.Reasoning as Cat

module Cat.Functor.Adjoint.AFT where

The adjoint functor theorem🔗

The adjoint functor theorem states a sufficient condition for a continuous functor $F : C \to 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 \to 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 \to F (X_{i}),$ which commute in the sense that, for every $X^{'}$ and $h : Y \to X^{'},$ there exists a $j : I$ and $t : X_{i} \to 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))

  open Solution-set

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))