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

$DF CH E$we get a “composite” $Lan_{F}(H):D→E.$ With this perspective in mind, it’s reasonable to expect that, if $F$ has an inverse $G:D→C,$ the composite we get should be the actual composite $H∘G.$

In fact, we can do better: if
$F$
only has a right
adjoint
$F⊣G$
(which we can think of as a directed inverse), then the induced `precomposite adjunction`

$−∘G⊣−∘F$
means that *left* (global) Kan extensions along
$F$
are given by precomposition with
$G$
(and, dually, right Kan
extensions along
$G$
are given by precomposition with
$F).$

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
$G$
is the `absolute`

left Kan extension of
$F$
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.