open import Cat.Functor.Kan.Duality
open import Cat.Functor.Coherence
open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Functor.Adjoint
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cr

module Cat.Functor.Adjoint.Kan where

Adjoints preserve Kan extensions🔗

Let $L\rightleftarrows R$ be a pair of adjoint functors. It’s well-known that right adjoints preserve limits¹, and dually that left adjoints preserve colimits, but it turns out that this theorem can be made a bit more general: If $G$ is a left (resp. right) extension of $F$ along $p\text{,}$ then $LG$ is a left extension of $LF$ along $p\text{:}$ left adjoints preserve left extensions. This dualises to right adjoints preserving right extensions.

The proof could be given in bicategorical generality: If the triangle below is a left extension diagram, then the overall pasted diagram is also a left extension. This is essentially because the $L⊣R$ adjunction provides a bunch of isomorphisms between natural transformations, e.g. $(LF\to Mp)\cong (F\to RMp)\text{,}$ which we can use to “grow” the original extension diagram.

module
  _ {oc ℓc oc' ℓc' od ℓd oa ℓa}
    {C : Precategory oc ℓc} {C' : Precategory oc' ℓc'} {D : Precategory od ℓd}
    {A : Precategory oa ℓa}
    {p : Functor C C'}
    {F : Functor C D}
    {G : Functor C' D}
    {eta : F => G F∘ p}
    (lan : is-lan p F G eta)
    {L : Functor D A} {R : Functor A D}
    (adj : L ⊣ R)
  where
  private
    open _⊣_ adj
    module l = is-lan lan
    open is-lan
    open _=>_
    module A = Cr A
    module D = Cr D
    module L = Fr L
    module R = Fr R
    module F = Functor F
    module G = Functor G
    module p = Functor p

    LF = L F∘ F
    LG = L F∘ G
    RL = R F∘ L
    module RL = Functor RL
    module LF = Functor LF
    module LG = Functor LG

  left-adjoint→left-extension : preserves-lan L lan
  left-adjoint→left-extension = pres where

    fixup : ∀ {M : Functor C' A} → (LF => M F∘ p) → F => (R F∘ M) F∘ p
    fixup α .η x = L-adjunct adj (α .η x)
    fixup {M = M} α .is-natural x y f =
      (R.₁ (α .η y) D.∘ unit.η _) D.∘ F.₁ f            ≡⟨ D.pullr (unit.is-natural _ _ _) ⟩≡
      (R.₁ (α .η y) D.∘ (RL.₁ (F.₁ f)) D.∘ unit.η _)   ≡⟨ D.extendl (R.weave (α .is-natural _ _ _)) ⟩≡
      R.₁ (M.₁ (p.₁ f)) D.∘ R.₁ (α .η x) D.∘ unit.η _  ∎
      where module M = Functor M

It wouldn’t fit in the diagram above, but the 2-cell of the larger diagram is simply the whiskering $L\eta \text{.}$ Unfortunately, proof assistants; Our existing definition of whiskering lands in $L(Gp)\text{,}$ but we need a natural transformation onto $(LG)p\text{.}$

    pres : is-lan p (L F∘ F) (L F∘ G) (nat-assoc-to (L ▸ eta))

Given a 2-cell $\alpha :LF\to Mp\text{,}$ how do we factor it through $\eta$ as a 2-cell $\sigma :LG\to M\text{?}$ Well, since the original diagram was an extension, if we can get our hands on a 2-cell $F\to M^{\prime }p\text{,}$ that’ll give us a cell $G\to M^{\prime }\text{.}$ Hm: choose $M^{\prime }=RM\text{,}$ let ${\alpha }^{\prime }:F\to (RM)p$ be the adjunct of $\alpha \text{,}$ factor it through the original $\eta$ into a cell ${\sigma }^{\prime }:G\to RM\text{,}$ and let $\sigma :LG\to M$ be its adjunct.

    pres .σ α .η x = R-adjunct adj (l.σ (fixup α) .η x)
    pres .σ {M = M} α .is-natural x y f =
      (ε _ A.∘ L.₁ (l.σ (fixup α) .η y)) A.∘ LG.₁ f        ≡⟨ A.pullr (L.weave (l.σ (fixup α) .is-natural x y f)) ⟩≡
      ε _ A.∘ (L.₁ (RM.₁ f) A.∘ L.₁ (l.σ (fixup α) .η x))  ≡⟨ A.extendl (counit.is-natural _ _ _) ⟩≡
      M.₁ f A.∘ pres .σ α .η x                             ∎
      where module M = Functor M
            module RM = Functor (R F∘ M)

And since every part of the process in the preceeding paragraph is an isomorphism, this is indeed a factorisation, and it’s unique to boot: we’ve shown that $LG$ is the extension of $LF$ along $p\text{!}$

    pres .σ-comm {α = α} = ext λ x →
      (R-adjunct adj (l.σ (fixup α) .η _)) A.∘ L.₁ (eta .η _) ≡⟨ L.pullr (l.σ-comm {α = fixup α} ηₚ _) ⟩≡
      R-adjunct adj (L-adjunct adj (α .η x))                  ≡⟨ equiv→unit (L-adjunct-is-equiv adj) (α .η x) ⟩≡
      α .η x                                                  ∎

    pres .σ-uniq {M = M} {α = α} {σ' = σ'} wit = ext λ x →
      R-adjunct adj (l.σ (fixup α) .η x)      ≡⟨ A.refl⟩∘⟨ ap L.₁ (l.σ-uniq lemma ηₚ x) ⟩≡
      R-adjunct adj (L-adjunct adj (σ' .η x)) ≡⟨ equiv→unit (L-adjunct-is-equiv adj) (σ' .η x) ⟩≡
      σ' .η x                                 ∎
      where
        module M = Functor M

        σ'' : G => R F∘ M
        σ'' .η x = L-adjunct adj (σ' .η x)
        σ'' .is-natural x y f =
          (R.₁ (σ' .η _) D.∘ unit.η _) D.∘ G.₁ f          ≡⟨ D.pullr (unit.is-natural _ _ _) ⟩≡
          (R.₁ (σ' .η _) D.∘ (RL.₁ (G.₁ f)) D.∘ unit.η _) ≡⟨ D.extendl (R.weave (σ' .is-natural _ _ _)) ⟩≡
          R.₁ (M.₁ f) D.∘ R.₁ (σ' .η x) D.∘ unit.η _      ∎

        lemma : fixup α ≡ ((σ'' ◂ p) ∘nt eta)
        lemma = ext λ x →
          R.₁ (α .η x) D.∘ unit.η _                     ≡⟨ ap R.₁ (wit ηₚ _) D.⟩∘⟨refl ⟩≡
          R.₁ (σ' .η _ A.∘ L.₁ (eta .η _)) D.∘ unit.η _ ≡⟨ ap (D._∘ unit.η _) (R.F-∘ _ _) ∙ D.extendr (sym (unit.is-natural _ _ _)) ⟩≡
          (R.₁ (σ' .η _) D.∘ unit.η _) D.∘ eta .η x     ∎

Dually🔗

By duality, right adjoints preserve right extensions.

module
  _ {oc ℓc oc' ℓc' od ℓd oa ℓa}
    {C : Precategory oc ℓc} {C' : Precategory oc' ℓc'} {D : Precategory od ℓd}
    {A : Precategory oa ℓa} {p : Functor C C'} {F : Functor C D} {G : Functor C' D}
    {eps : G F∘ p => F} (ran : is-ran p F G eps) {L : Functor A D} {R : Functor D A}
    (adj : L ⊣ R)
  where

  right-adjoint→right-extension : preserves-ran R ran
  right-adjoint→right-extension = fixed where
    pres-lan = left-adjoint→left-extension
      (is-ran→is-co-lan _ _ ran)
      (opposite-adjunction adj)

    module p = is-lan pres-lan
    open is-ran
    open _=>_

    fixed : is-ran p (R F∘ F) (R F∘ G) (nat-assoc-from (R ▸ eps))
    fixed .is-ran.σ {M = M} α = σ' where
      unquoteDecl α' = dualise-into α'
        (Functor.op R F∘ Functor.op F => Functor.op M F∘ Functor.op p)
        α
      unquoteDecl σ' = dualise-into σ' (M => R F∘ G) (p.σ α')

    fixed .is-ran.σ-comm = ext λ x → p.σ-comm ηₚ _
    fixed .is-ran.σ-uniq {M = M} {σ' = σ'} p =
      ext λ x → p.σ-uniq {σ' = dualise! σ'} (reext! p) ηₚ x