module Cat.Functor.Kan.Adjoint where

Adjoints are Kan extensions🔗

One way to think about Kan extensions is that, when they exist, they allow us to “compose” two functors when one of them is going the wrong way: given a span

DFCHE D \xleftarrow{F} C \xrightarrow{H} E

we get a “composite” LanF(H):DE\operatorname{Lan}_F(H) : D \to E. With this perspective in mind, it’s reasonable to expect that, if FF has an inverse G:DCG : D \to C, the composite we get should be the actual composite HGH \circ G.

In fact, we can do better: if FF only has a right adjoint FGF \dashv G (which we can think of as a directed inverse), then the induced precomposite adjunction GF- \circ G \dashv - \circ F means that left (global) Kan extensions along FF are given by precomposition with GG (and, dually, right Kan extensions along GG are given by precomposition with FF).

module _ {F : Functor C D} {G : Functor D C} (F⊣G : F  G) where
  adjoint→is-lan
    : (H : Functor C E)
     is-lan F H (H F∘ G) (precomposite-adjunction F⊣G .unit .η H)
  adjoint→is-lan = adjoint-precompose→Lan F (precompose G) (precomposite-adjunction F⊣G)

A more common way to say this is that GG is the absolute left Kan extension of FF along the identity; this is essentially a reformulation of the above fact:

  adjoint→is-lan-id : is-lan F Id G (F⊣G .unit)
  adjoint→is-lan-id =
    transport  i  is-lan F Id (F∘-idl i) (fixNT i))
      (adjoint→is-lan Id)
    where
      fixNT : PathP  i  Id => F∘-idl {F = G} i F∘ F) _ _
      fixNT = Nat-pathp refl  i  F∘-idl i F∘ F)  _  refl)

  adjoint→is-absolute-lan : is-absolute-lan adjoint→is-lan-id
  adjoint→is-absolute-lan H =
    transport  i  is-lan F (F∘-idr (~ i)) (H F∘ G) (fixNT (~ i)))
      (adjoint→is-lan H)
    where
      fixNT : PathP  i  F∘-idr {F = H} i => (H F∘ G) F∘ F) _ _
      fixNT = Nat-pathp F∘-idr refl  _  refl)

The dual statement is obtained by… duality, this time using the counit of the precomposite adjunction:

module _ {F : Functor C D} {G : Functor D C} (F⊣G : F  G) where
  adjoint→is-ran
    : (H : Functor D E)
     is-ran G H (H F∘ F) (precomposite-adjunction F⊣G .counit .η H)
  adjoint→is-ran H =
    transport  i  is-ran G H (fixF i) (fixNT i))
      (is-co-lan'→is-ran G H
        (adjoint→is-lan (opposite-adjunction F⊣G) (Functor.op H)))
    where
      fixF : Functor.op (Functor.op H F∘ Functor.op F)  H F∘ F
      fixF = Functor-path  _  refl)  _  refl)
      fixNT : PathP  i  fixF i F∘ G => H) _ _
      fixNT = Nat-pathp  i  fixF i F∘ G) refl  _  refl)

Even more dually, we can flip the span above to get a cospan of functors, giving rise to the theory of Kan lifts. We then get analogous statements: left (resp. right) adjoints are absolute left (resp. right) Kan lifts along the identity.