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

we get a “composite” With this perspective in mind, it’s reasonable to expect that, if has an inverse the composite we get should be the actual composite

In fact, we can do better: if only has a right adjoint (which we can think of as a directed inverse), then the induced precomposite adjunction means that left (global) Kan extensions along are given by precomposition with (and, dually, right Kan extensions along are given by precomposition with

module _ {F : Functor C D} {G : Functor D C} (F⊣G : F  G) where
    : (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 is the absolute left Kan extension of 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)
      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)
      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
    : (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)))
      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.